ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  poxp Structured version   GIF version

Theorem poxp 5794
Description: A lexicographical ordering of two posets. (Contributed by Scott Fenton, 16-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.)
Hypothesis
Ref Expression
poxp.1 𝑇 = {⟨x, y⟩ ∣ ((x (A × B) y (A × B)) ((1stx)𝑅(1sty) ((1stx) = (1sty) (2ndx)𝑆(2ndy))))}
Assertion
Ref Expression
poxp ((𝑅 Po A 𝑆 Po B) → 𝑇 Po (A × B))
Distinct variable groups:   x,A,y   x,B,y   x,𝑅,y   x,𝑆,y
Allowed substitution hints:   𝑇(x,y)

Proof of Theorem poxp
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 f 𝑡 u v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elxp 4305 . . . . . . . 8 (𝑡 (A × B) ↔ 𝑎𝑏(𝑡 = ⟨𝑎, 𝑏 (𝑎 A 𝑏 B)))
2 elxp 4305 . . . . . . . 8 (u (A × B) ↔ 𝑐𝑑(u = ⟨𝑐, 𝑑 (𝑐 A 𝑑 B)))
3 elxp 4305 . . . . . . . 8 (v (A × B) ↔ 𝑒f(v = ⟨𝑒, f (𝑒 A f B)))
4 3an6 1216 . . . . . . . . . . . . . . . . 17 (((𝑡 = ⟨𝑎, 𝑏 (𝑎 A 𝑏 B)) (u = ⟨𝑐, 𝑑 (𝑐 A 𝑑 B)) (v = ⟨𝑒, f (𝑒 A f B))) ↔ ((𝑡 = ⟨𝑎, 𝑏 u = ⟨𝑐, 𝑑 v = ⟨𝑒, f⟩) ((𝑎 A 𝑏 B) (𝑐 A 𝑑 B) (𝑒 A f B))))
5 poirr 4035 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 Po A 𝑎 A) → ¬ 𝑎𝑅𝑎)
65ex 108 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑅 Po A → (𝑎 A → ¬ 𝑎𝑅𝑎))
7 poirr 4035 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑆 Po B 𝑏 B) → ¬ 𝑏𝑆𝑏)
87intnand 839 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑆 Po B 𝑏 B) → ¬ (𝑎 = 𝑎 𝑏𝑆𝑏))
98ex 108 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑆 Po B → (𝑏 B → ¬ (𝑎 = 𝑎 𝑏𝑆𝑏)))
106, 9im2anan9 530 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 Po A 𝑆 Po B) → ((𝑎 A 𝑏 B) → (¬ 𝑎𝑅𝑎 ¬ (𝑎 = 𝑎 𝑏𝑆𝑏))))
11 ioran 668 . . . . . . . . . . . . . . . . . . . . . . . . 25 (¬ (𝑎𝑅𝑎 (𝑎 = 𝑎 𝑏𝑆𝑏)) ↔ (¬ 𝑎𝑅𝑎 ¬ (𝑎 = 𝑎 𝑏𝑆𝑏)))
1210, 11syl6ibr 151 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Po A 𝑆 Po B) → ((𝑎 A 𝑏 B) → ¬ (𝑎𝑅𝑎 (𝑎 = 𝑎 𝑏𝑆𝑏))))
1312imp 115 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 Po A 𝑆 Po B) (𝑎 A 𝑏 B)) → ¬ (𝑎𝑅𝑎 (𝑎 = 𝑎 𝑏𝑆𝑏)))
1413intnand 839 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 Po A 𝑆 Po B) (𝑎 A 𝑏 B)) → ¬ (((𝑎 A 𝑎 A) (𝑏 B 𝑏 B)) (𝑎𝑅𝑎 (𝑎 = 𝑎 𝑏𝑆𝑏))))
15143ad2antr1 1068 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po A 𝑆 Po B) ((𝑎 A 𝑏 B) (𝑐 A 𝑑 B) (𝑒 A f B))) → ¬ (((𝑎 A 𝑎 A) (𝑏 B 𝑏 B)) (𝑎𝑅𝑎 (𝑎 = 𝑎 𝑏𝑆𝑏))))
16 an4 520 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑎 A 𝑐 A) (𝑏 B 𝑑 B)) (𝑎𝑅𝑐 (𝑎 = 𝑐 𝑏𝑆𝑑))) (((𝑐 A 𝑒 A) (𝑑 B f B)) (𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f)))) ↔ ((((𝑎 A 𝑐 A) (𝑏 B 𝑑 B)) ((𝑐 A 𝑒 A) (𝑑 B f B))) ((𝑎𝑅𝑐 (𝑎 = 𝑐 𝑏𝑆𝑑)) (𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f)))))
17 3an6 1216 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑎 A 𝑏 B) (𝑐 A 𝑑 B) (𝑒 A f B)) ↔ ((𝑎 A 𝑐 A 𝑒 A) (𝑏 B 𝑑 B f B)))
18 potr 4036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑅 Po A (𝑎 A 𝑐 A 𝑒 A)) → ((𝑎𝑅𝑐 𝑐𝑅𝑒) → 𝑎𝑅𝑒))
19183impia 1100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑅 Po A (𝑎 A 𝑐 A 𝑒 A) (𝑎𝑅𝑐 𝑐𝑅𝑒)) → 𝑎𝑅𝑒)
2019orcd 651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑅 Po A (𝑎 A 𝑐 A 𝑒 A) (𝑎𝑅𝑐 𝑐𝑅𝑒)) → (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f)))
21203expia 1105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 Po A (𝑎 A 𝑐 A 𝑒 A)) → ((𝑎𝑅𝑐 𝑐𝑅𝑒) → (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f))))
2221expdimp 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑅 Po A (𝑎 A 𝑐 A 𝑒 A)) 𝑎𝑅𝑐) → (𝑐𝑅𝑒 → (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f))))
23 breq2 3759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑒 → (𝑎𝑅𝑐𝑎𝑅𝑒))
2423biimpa 280 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 = 𝑒 𝑎𝑅𝑐) → 𝑎𝑅𝑒)
2524orcd 651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 = 𝑒 𝑎𝑅𝑐) → (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f)))
2625expcom 109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎𝑅𝑐 → (𝑐 = 𝑒 → (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f))))
2726adantrd 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎𝑅𝑐 → ((𝑐 = 𝑒 𝑑𝑆f) → (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f))))
2827adantl 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑅 Po A (𝑎 A 𝑐 A 𝑒 A)) 𝑎𝑅𝑐) → ((𝑐 = 𝑒 𝑑𝑆f) → (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f))))
2922, 28jaod 636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑅 Po A (𝑎 A 𝑐 A 𝑒 A)) 𝑎𝑅𝑐) → ((𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f)) → (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f))))
3029ex 108 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 Po A (𝑎 A 𝑐 A 𝑒 A)) → (𝑎𝑅𝑐 → ((𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f)) → (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f)))))
31 potr 4036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑆 Po B (𝑏 B 𝑑 B f B)) → ((𝑏𝑆𝑑 𝑑𝑆f) → 𝑏𝑆f))
3231expdimp 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑆 Po B (𝑏 B 𝑑 B f B)) 𝑏𝑆𝑑) → (𝑑𝑆f𝑏𝑆f))
3332anim2d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑆 Po B (𝑏 B 𝑑 B f B)) 𝑏𝑆𝑑) → ((𝑐 = 𝑒 𝑑𝑆f) → (𝑐 = 𝑒 𝑏𝑆f)))
3433orim2d 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑆 Po B (𝑏 B 𝑑 B f B)) 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f)) → (𝑐𝑅𝑒 (𝑐 = 𝑒 𝑏𝑆f))))
35 breq1 3758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑎 = 𝑐 → (𝑎𝑅𝑒𝑐𝑅𝑒))
36 equequ1 1595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑎 = 𝑐 → (𝑎 = 𝑒𝑐 = 𝑒))
3736anbi1d 438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑎 = 𝑐 → ((𝑎 = 𝑒 𝑏𝑆f) ↔ (𝑐 = 𝑒 𝑏𝑆f)))
3835, 37orbi12d 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎 = 𝑐 → ((𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f)) ↔ (𝑐𝑅𝑒 (𝑐 = 𝑒 𝑏𝑆f))))
3938imbi2d 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 = 𝑐 → (((𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f)) → (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f))) ↔ ((𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f)) → (𝑐𝑅𝑒 (𝑐 = 𝑒 𝑏𝑆f)))))
4034, 39syl5ibr 145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 = 𝑐 → (((𝑆 Po B (𝑏 B 𝑑 B f B)) 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f)) → (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f)))))
4140expd 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 = 𝑐 → ((𝑆 Po B (𝑏 B 𝑑 B f B)) → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f)) → (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f))))))
4241com12 27 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑆 Po B (𝑏 B 𝑑 B f B)) → (𝑎 = 𝑐 → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f)) → (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f))))))
4342impd 242 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑆 Po B (𝑏 B 𝑑 B f B)) → ((𝑎 = 𝑐 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f)) → (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f)))))
4430, 43jaao 638 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑅 Po A (𝑎 A 𝑐 A 𝑒 A)) (𝑆 Po B (𝑏 B 𝑑 B f B))) → ((𝑎𝑅𝑐 (𝑎 = 𝑐 𝑏𝑆𝑑)) → ((𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f)) → (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f)))))
4544impd 242 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑅 Po A (𝑎 A 𝑐 A 𝑒 A)) (𝑆 Po B (𝑏 B 𝑑 B f B))) → (((𝑎𝑅𝑐 (𝑎 = 𝑐 𝑏𝑆𝑑)) (𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f))) → (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f))))
4645an4s 522 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po A 𝑆 Po B) ((𝑎 A 𝑐 A 𝑒 A) (𝑏 B 𝑑 B f B))) → (((𝑎𝑅𝑐 (𝑎 = 𝑐 𝑏𝑆𝑑)) (𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f))) → (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f))))
4717, 46sylan2b 271 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 Po A 𝑆 Po B) ((𝑎 A 𝑏 B) (𝑐 A 𝑑 B) (𝑒 A f B))) → (((𝑎𝑅𝑐 (𝑎 = 𝑐 𝑏𝑆𝑑)) (𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f))) → (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f))))
48 an4 520 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎 A 𝑏 B) (𝑒 A f B)) ↔ ((𝑎 A 𝑒 A) (𝑏 B f B)))
4948biimpi 113 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑎 A 𝑏 B) (𝑒 A f B)) → ((𝑎 A 𝑒 A) (𝑏 B f B)))
50493adant2 922 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑎 A 𝑏 B) (𝑐 A 𝑑 B) (𝑒 A f B)) → ((𝑎 A 𝑒 A) (𝑏 B f B)))
5150adantl 262 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 Po A 𝑆 Po B) ((𝑎 A 𝑏 B) (𝑐 A 𝑑 B) (𝑒 A f B))) → ((𝑎 A 𝑒 A) (𝑏 B f B)))
5247, 51jctild 299 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 Po A 𝑆 Po B) ((𝑎 A 𝑏 B) (𝑐 A 𝑑 B) (𝑒 A f B))) → (((𝑎𝑅𝑐 (𝑎 = 𝑐 𝑏𝑆𝑑)) (𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f))) → (((𝑎 A 𝑒 A) (𝑏 B f B)) (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f)))))
5352adantld 263 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 Po A 𝑆 Po B) ((𝑎 A 𝑏 B) (𝑐 A 𝑑 B) (𝑒 A f B))) → (((((𝑎 A 𝑐 A) (𝑏 B 𝑑 B)) ((𝑐 A 𝑒 A) (𝑑 B f B))) ((𝑎𝑅𝑐 (𝑎 = 𝑐 𝑏𝑆𝑑)) (𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f)))) → (((𝑎 A 𝑒 A) (𝑏 B f B)) (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f)))))
5416, 53syl5bi 141 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po A 𝑆 Po B) ((𝑎 A 𝑏 B) (𝑐 A 𝑑 B) (𝑒 A f B))) → (((((𝑎 A 𝑐 A) (𝑏 B 𝑑 B)) (𝑎𝑅𝑐 (𝑎 = 𝑐 𝑏𝑆𝑑))) (((𝑐 A 𝑒 A) (𝑑 B f B)) (𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f)))) → (((𝑎 A 𝑒 A) (𝑏 B f B)) (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f)))))
5515, 54jca 290 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 Po A 𝑆 Po B) ((𝑎 A 𝑏 B) (𝑐 A 𝑑 B) (𝑒 A f B))) → (¬ (((𝑎 A 𝑎 A) (𝑏 B 𝑏 B)) (𝑎𝑅𝑎 (𝑎 = 𝑎 𝑏𝑆𝑏))) (((((𝑎 A 𝑐 A) (𝑏 B 𝑑 B)) (𝑎𝑅𝑐 (𝑎 = 𝑐 𝑏𝑆𝑑))) (((𝑐 A 𝑒 A) (𝑑 B f B)) (𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f)))) → (((𝑎 A 𝑒 A) (𝑏 B f B)) (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f))))))
56 breq12 3760 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 = ⟨𝑎, 𝑏 𝑡 = ⟨𝑎, 𝑏⟩) → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
5756anidms 377 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
5857notbid 591 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = ⟨𝑎, 𝑏⟩ → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
59583ad2ant1 924 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 = ⟨𝑎, 𝑏 u = ⟨𝑐, 𝑑 v = ⟨𝑒, f⟩) → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
60 breq12 3760 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 = ⟨𝑎, 𝑏 u = ⟨𝑐, 𝑑⟩) → (𝑡𝑇u ↔ ⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩))
61603adant3 923 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 = ⟨𝑎, 𝑏 u = ⟨𝑐, 𝑑 v = ⟨𝑒, f⟩) → (𝑡𝑇u ↔ ⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩))
62 breq12 3760 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((u = ⟨𝑐, 𝑑 v = ⟨𝑒, f⟩) → (u𝑇v ↔ ⟨𝑐, 𝑑𝑇𝑒, f⟩))
63623adant1 921 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 = ⟨𝑎, 𝑏 u = ⟨𝑐, 𝑑 v = ⟨𝑒, f⟩) → (u𝑇v ↔ ⟨𝑐, 𝑑𝑇𝑒, f⟩))
6461, 63anbi12d 442 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 = ⟨𝑎, 𝑏 u = ⟨𝑐, 𝑑 v = ⟨𝑒, f⟩) → ((𝑡𝑇u u𝑇v) ↔ (⟨𝑎, 𝑏𝑇𝑐, 𝑑𝑐, 𝑑𝑇𝑒, f⟩)))
65 breq12 3760 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 = ⟨𝑎, 𝑏 v = ⟨𝑒, f⟩) → (𝑡𝑇v ↔ ⟨𝑎, 𝑏𝑇𝑒, f⟩))
66653adant2 922 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 = ⟨𝑎, 𝑏 u = ⟨𝑐, 𝑑 v = ⟨𝑒, f⟩) → (𝑡𝑇v ↔ ⟨𝑎, 𝑏𝑇𝑒, f⟩))
6764, 66imbi12d 223 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 = ⟨𝑎, 𝑏 u = ⟨𝑐, 𝑑 v = ⟨𝑒, f⟩) → (((𝑡𝑇u u𝑇v) → 𝑡𝑇v) ↔ ((⟨𝑎, 𝑏𝑇𝑐, 𝑑𝑐, 𝑑𝑇𝑒, f⟩) → ⟨𝑎, 𝑏𝑇𝑒, f⟩)))
6859, 67anbi12d 442 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 = ⟨𝑎, 𝑏 u = ⟨𝑐, 𝑑 v = ⟨𝑒, f⟩) → ((¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v)) ↔ (¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏 ((⟨𝑎, 𝑏𝑇𝑐, 𝑑𝑐, 𝑑𝑇𝑒, f⟩) → ⟨𝑎, 𝑏𝑇𝑒, f⟩))))
69 poxp.1 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑇 = {⟨x, y⟩ ∣ ((x (A × B) y (A × B)) ((1stx)𝑅(1sty) ((1stx) = (1sty) (2ndx)𝑆(2ndy))))}
7069xporderlem 5793 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ↔ (((𝑎 A 𝑎 A) (𝑏 B 𝑏 B)) (𝑎𝑅𝑎 (𝑎 = 𝑎 𝑏𝑆𝑏))))
7170notbii 593 . . . . . . . . . . . . . . . . . . . . . 22 (¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ↔ ¬ (((𝑎 A 𝑎 A) (𝑏 B 𝑏 B)) (𝑎𝑅𝑎 (𝑎 = 𝑎 𝑏𝑆𝑏))))
7269xporderlem 5793 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ↔ (((𝑎 A 𝑐 A) (𝑏 B 𝑑 B)) (𝑎𝑅𝑐 (𝑎 = 𝑐 𝑏𝑆𝑑))))
7369xporderlem 5793 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑐, 𝑑𝑇𝑒, f⟩ ↔ (((𝑐 A 𝑒 A) (𝑑 B f B)) (𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f))))
7472, 73anbi12i 433 . . . . . . . . . . . . . . . . . . . . . . 23 ((⟨𝑎, 𝑏𝑇𝑐, 𝑑𝑐, 𝑑𝑇𝑒, f⟩) ↔ ((((𝑎 A 𝑐 A) (𝑏 B 𝑑 B)) (𝑎𝑅𝑐 (𝑎 = 𝑐 𝑏𝑆𝑑))) (((𝑐 A 𝑒 A) (𝑑 B f B)) (𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f)))))
7569xporderlem 5793 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑎, 𝑏𝑇𝑒, f⟩ ↔ (((𝑎 A 𝑒 A) (𝑏 B f B)) (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f))))
7674, 75imbi12i 228 . . . . . . . . . . . . . . . . . . . . . 22 (((⟨𝑎, 𝑏𝑇𝑐, 𝑑𝑐, 𝑑𝑇𝑒, f⟩) → ⟨𝑎, 𝑏𝑇𝑒, f⟩) ↔ (((((𝑎 A 𝑐 A) (𝑏 B 𝑑 B)) (𝑎𝑅𝑐 (𝑎 = 𝑐 𝑏𝑆𝑑))) (((𝑐 A 𝑒 A) (𝑑 B f B)) (𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f)))) → (((𝑎 A 𝑒 A) (𝑏 B f B)) (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f)))))
7771, 76anbi12i 433 . . . . . . . . . . . . . . . . . . . . 21 ((¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏 ((⟨𝑎, 𝑏𝑇𝑐, 𝑑𝑐, 𝑑𝑇𝑒, f⟩) → ⟨𝑎, 𝑏𝑇𝑒, f⟩)) ↔ (¬ (((𝑎 A 𝑎 A) (𝑏 B 𝑏 B)) (𝑎𝑅𝑎 (𝑎 = 𝑎 𝑏𝑆𝑏))) (((((𝑎 A 𝑐 A) (𝑏 B 𝑑 B)) (𝑎𝑅𝑐 (𝑎 = 𝑐 𝑏𝑆𝑑))) (((𝑐 A 𝑒 A) (𝑑 B f B)) (𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f)))) → (((𝑎 A 𝑒 A) (𝑏 B f B)) (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f))))))
7868, 77syl6bb 185 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 = ⟨𝑎, 𝑏 u = ⟨𝑐, 𝑑 v = ⟨𝑒, f⟩) → ((¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v)) ↔ (¬ (((𝑎 A 𝑎 A) (𝑏 B 𝑏 B)) (𝑎𝑅𝑎 (𝑎 = 𝑎 𝑏𝑆𝑏))) (((((𝑎 A 𝑐 A) (𝑏 B 𝑑 B)) (𝑎𝑅𝑐 (𝑎 = 𝑐 𝑏𝑆𝑑))) (((𝑐 A 𝑒 A) (𝑑 B f B)) (𝑐𝑅𝑒 (𝑐 = 𝑒 𝑑𝑆f)))) → (((𝑎 A 𝑒 A) (𝑏 B f B)) (𝑎𝑅𝑒 (𝑎 = 𝑒 𝑏𝑆f)))))))
7955, 78syl5ibr 145 . . . . . . . . . . . . . . . . . . 19 ((𝑡 = ⟨𝑎, 𝑏 u = ⟨𝑐, 𝑑 v = ⟨𝑒, f⟩) → (((𝑅 Po A 𝑆 Po B) ((𝑎 A 𝑏 B) (𝑐 A 𝑑 B) (𝑒 A f B))) → (¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v))))
8079expcomd 1327 . . . . . . . . . . . . . . . . . 18 ((𝑡 = ⟨𝑎, 𝑏 u = ⟨𝑐, 𝑑 v = ⟨𝑒, f⟩) → (((𝑎 A 𝑏 B) (𝑐 A 𝑑 B) (𝑒 A f B)) → ((𝑅 Po A 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v)))))
8180imp 115 . . . . . . . . . . . . . . . . 17 (((𝑡 = ⟨𝑎, 𝑏 u = ⟨𝑐, 𝑑 v = ⟨𝑒, f⟩) ((𝑎 A 𝑏 B) (𝑐 A 𝑑 B) (𝑒 A f B))) → ((𝑅 Po A 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v))))
824, 81sylbi 114 . . . . . . . . . . . . . . . 16 (((𝑡 = ⟨𝑎, 𝑏 (𝑎 A 𝑏 B)) (u = ⟨𝑐, 𝑑 (𝑐 A 𝑑 B)) (v = ⟨𝑒, f (𝑒 A f B))) → ((𝑅 Po A 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v))))
83823exp 1102 . . . . . . . . . . . . . . 15 ((𝑡 = ⟨𝑎, 𝑏 (𝑎 A 𝑏 B)) → ((u = ⟨𝑐, 𝑑 (𝑐 A 𝑑 B)) → ((v = ⟨𝑒, f (𝑒 A f B)) → ((𝑅 Po A 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v))))))
8483com3l 75 . . . . . . . . . . . . . 14 ((u = ⟨𝑐, 𝑑 (𝑐 A 𝑑 B)) → ((v = ⟨𝑒, f (𝑒 A f B)) → ((𝑡 = ⟨𝑎, 𝑏 (𝑎 A 𝑏 B)) → ((𝑅 Po A 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v))))))
8584exlimivv 1773 . . . . . . . . . . . . 13 (𝑐𝑑(u = ⟨𝑐, 𝑑 (𝑐 A 𝑑 B)) → ((v = ⟨𝑒, f (𝑒 A f B)) → ((𝑡 = ⟨𝑎, 𝑏 (𝑎 A 𝑏 B)) → ((𝑅 Po A 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v))))))
8685com3l 75 . . . . . . . . . . . 12 ((v = ⟨𝑒, f (𝑒 A f B)) → ((𝑡 = ⟨𝑎, 𝑏 (𝑎 A 𝑏 B)) → (𝑐𝑑(u = ⟨𝑐, 𝑑 (𝑐 A 𝑑 B)) → ((𝑅 Po A 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v))))))
8786exlimivv 1773 . . . . . . . . . . 11 (𝑒f(v = ⟨𝑒, f (𝑒 A f B)) → ((𝑡 = ⟨𝑎, 𝑏 (𝑎 A 𝑏 B)) → (𝑐𝑑(u = ⟨𝑐, 𝑑 (𝑐 A 𝑑 B)) → ((𝑅 Po A 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v))))))
8887com3l 75 . . . . . . . . . 10 ((𝑡 = ⟨𝑎, 𝑏 (𝑎 A 𝑏 B)) → (𝑐𝑑(u = ⟨𝑐, 𝑑 (𝑐 A 𝑑 B)) → (𝑒f(v = ⟨𝑒, f (𝑒 A f B)) → ((𝑅 Po A 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v))))))
8988exlimivv 1773 . . . . . . . . 9 (𝑎𝑏(𝑡 = ⟨𝑎, 𝑏 (𝑎 A 𝑏 B)) → (𝑐𝑑(u = ⟨𝑐, 𝑑 (𝑐 A 𝑑 B)) → (𝑒f(v = ⟨𝑒, f (𝑒 A f B)) → ((𝑅 Po A 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v))))))
90893imp 1097 . . . . . . . 8 ((𝑎𝑏(𝑡 = ⟨𝑎, 𝑏 (𝑎 A 𝑏 B)) 𝑐𝑑(u = ⟨𝑐, 𝑑 (𝑐 A 𝑑 B)) 𝑒f(v = ⟨𝑒, f (𝑒 A f B))) → ((𝑅 Po A 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v))))
911, 2, 3, 90syl3anb 1177 . . . . . . 7 ((𝑡 (A × B) u (A × B) v (A × B)) → ((𝑅 Po A 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v))))
92913expia 1105 . . . . . 6 ((𝑡 (A × B) u (A × B)) → (v (A × B) → ((𝑅 Po A 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v)))))
9392com3r 73 . . . . 5 ((𝑅 Po A 𝑆 Po B) → ((𝑡 (A × B) u (A × B)) → (v (A × B) → (¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v)))))
9493imp 115 . . . 4 (((𝑅 Po A 𝑆 Po B) (𝑡 (A × B) u (A × B))) → (v (A × B) → (¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v))))
9594ralrimiv 2385 . . 3 (((𝑅 Po A 𝑆 Po B) (𝑡 (A × B) u (A × B))) → v (A × B)(¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v)))
9695ralrimivva 2395 . 2 ((𝑅 Po A 𝑆 Po B) → 𝑡 (A × B)u (A × B)v (A × B)(¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v)))
97 df-po 4024 . 2 (𝑇 Po (A × B) ↔ 𝑡 (A × B)u (A × B)v (A × B)(¬ 𝑡𝑇𝑡 ((𝑡𝑇u u𝑇v) → 𝑡𝑇v)))
9896, 97sylibr 137 1 ((𝑅 Po A 𝑆 Po B) → 𝑇 Po (A × B))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   wa 97  wb 98   wo 628   w3a 884   = wceq 1242  wex 1378   wcel 1390  wral 2300  cop 3370   class class class wbr 3755  {copab 3808   Po wpo 4022   × cxp 4286  cfv 4845  1st c1st 5707  2nd c2nd 5708
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-po 4024  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-iota 4810  df-fun 4847  df-fv 4853  df-1st 5709  df-2nd 5710
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator