MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  poxp Structured version   Visualization version   GIF version

Theorem poxp 7458
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 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))}
Assertion
Ref Expression
poxp ((𝑅 Po 𝐴𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝑅,𝑦   𝑥,𝑆,𝑦
Allowed substitution hints:   𝑇(𝑥,𝑦)

Proof of Theorem poxp
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑡 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elxp 5288 . . . . . . . 8 (𝑡 ∈ (𝐴 × 𝐵) ↔ ∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)))
2 elxp 5288 . . . . . . . 8 (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)))
3 elxp 5288 . . . . . . . 8 (𝑣 ∈ (𝐴 × 𝐵) ↔ ∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)))
4 3an6 1558 . . . . . . . . . . . . . . . . 17 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) ∧ (𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵))) ↔ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))))
5 poirr 5198 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 Po 𝐴𝑎𝐴) → ¬ 𝑎𝑅𝑎)
65ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑅 Po 𝐴 → (𝑎𝐴 → ¬ 𝑎𝑅𝑎))
7 poirr 5198 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑆 Po 𝐵𝑏𝐵) → ¬ 𝑏𝑆𝑏)
87intnand 1000 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑆 Po 𝐵𝑏𝐵) → ¬ (𝑎 = 𝑎𝑏𝑆𝑏))
98ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑆 Po 𝐵 → (𝑏𝐵 → ¬ (𝑎 = 𝑎𝑏𝑆𝑏)))
106, 9im2anan9 916 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 Po 𝐴𝑆 Po 𝐵) → ((𝑎𝐴𝑏𝐵) → (¬ 𝑎𝑅𝑎 ∧ ¬ (𝑎 = 𝑎𝑏𝑆𝑏))))
11 ioran 512 . . . . . . . . . . . . . . . . . . . . . . . . 25 (¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏)) ↔ (¬ 𝑎𝑅𝑎 ∧ ¬ (𝑎 = 𝑎𝑏𝑆𝑏)))
1210, 11syl6ibr 242 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Po 𝐴𝑆 Po 𝐵) → ((𝑎𝐴𝑏𝐵) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
1312imp 444 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ (𝑎𝐴𝑏𝐵)) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏)))
1413intnand 1000 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ (𝑎𝐴𝑏𝐵)) → ¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
15143ad2antr1 1204 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → ¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
16 an4 900 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) ↔ ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ ((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))))
17 3an6 1558 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵)) ↔ ((𝑎𝐴𝑐𝐴𝑒𝐴) ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)))
18 potr 5199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) → ((𝑎𝑅𝑐𝑐𝑅𝑒) → 𝑎𝑅𝑒))
19183impia 1110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴) ∧ (𝑎𝑅𝑐𝑐𝑅𝑒)) → 𝑎𝑅𝑒)
2019orcd 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴) ∧ (𝑎𝑅𝑐𝑐𝑅𝑒)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))
21203expia 1115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) → ((𝑎𝑅𝑐𝑐𝑅𝑒) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
2221expdimp 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ 𝑎𝑅𝑐) → (𝑐𝑅𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
23 breq2 4808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑒 → (𝑎𝑅𝑐𝑎𝑅𝑒))
2423biimpa 502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 = 𝑒𝑎𝑅𝑐) → 𝑎𝑅𝑒)
2524orcd 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 = 𝑒𝑎𝑅𝑐) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))
2625expcom 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎𝑅𝑐 → (𝑐 = 𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
2726adantrd 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎𝑅𝑐 → ((𝑐 = 𝑒𝑑𝑆𝑓) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
2827adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ 𝑎𝑅𝑐) → ((𝑐 = 𝑒𝑑𝑆𝑓) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
2922, 28jaod 394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ 𝑎𝑅𝑐) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
3029ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) → (𝑎𝑅𝑐 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
31 potr 5199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) → ((𝑏𝑆𝑑𝑑𝑆𝑓) → 𝑏𝑆𝑓))
3231expdimp 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) ∧ 𝑏𝑆𝑑) → (𝑑𝑆𝑓𝑏𝑆𝑓))
3332anim2d 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐 = 𝑒𝑑𝑆𝑓) → (𝑐 = 𝑒𝑏𝑆𝑓)))
3433orim2d 921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑏𝑆𝑓))))
35 breq1 4807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑎 = 𝑐 → (𝑎𝑅𝑒𝑐𝑅𝑒))
36 equequ1 2107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑎 = 𝑐 → (𝑎 = 𝑒𝑐 = 𝑒))
3736anbi1d 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑎 = 𝑐 → ((𝑎 = 𝑒𝑏𝑆𝑓) ↔ (𝑐 = 𝑒𝑏𝑆𝑓)))
3835, 37orbi12d 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎 = 𝑐 → ((𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)) ↔ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑏𝑆𝑓))))
3938imbi2d 329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 = 𝑐 → (((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))) ↔ ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑏𝑆𝑓)))))
4034, 39syl5ibr 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 = 𝑐 → (((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
4140expd 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 = 𝑐 → ((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))))
4241com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) → (𝑎 = 𝑐 → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))))
4342impd 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) → ((𝑎 = 𝑐𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
4430, 43jaao 532 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ (𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
4544impd 446 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ (𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
4645an4s 904 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑐𝐴𝑒𝐴) ∧ (𝑏𝐵𝑑𝐵𝑓𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
4717, 46sylan2b 493 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
48 an4 900 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎𝐴𝑏𝐵) ∧ (𝑒𝐴𝑓𝐵)) ↔ ((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)))
4948biimpi 206 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑎𝐴𝑏𝐵) ∧ (𝑒𝐴𝑓𝐵)) → ((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)))
50493adant2 1126 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵)) → ((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)))
5150adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → ((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)))
5247, 51jctild 567 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
5352adantld 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ ((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
5416, 53syl5bi 232 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
5515, 54jca 555 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))) ∧ (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))))
56 breq12 4809 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑡 = ⟨𝑎, 𝑏⟩) → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
5756anidms 680 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
5857notbid 307 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = ⟨𝑎, 𝑏⟩ → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
59583ad2ant1 1128 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
60 breq12 4809 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩))
61603adant3 1127 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩))
62 breq12 4809 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑢𝑇𝑣 ↔ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩))
63623adant1 1125 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑢𝑇𝑣 ↔ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩))
6461, 63anbi12d 749 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((𝑡𝑇𝑢𝑢𝑇𝑣) ↔ (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩)))
65 breq12 4809 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑣 ↔ ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩))
66653adant2 1126 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑣 ↔ ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩))
6764, 66imbi12d 333 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣) ↔ ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) → ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩)))
6859, 67anbi12d 749 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)) ↔ (¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ∧ ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) → ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩))))
69 poxp.1 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))}
7069xporderlem 7457 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ↔ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
7170notbii 309 . . . . . . . . . . . . . . . . . . . . . 22 (¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ↔ ¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
7269xporderlem 7457 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ↔ (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))))
7369xporderlem 7457 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩ ↔ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))))
7472, 73anbi12i 735 . . . . . . . . . . . . . . . . . . . . . . 23 ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) ↔ ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))))
7569xporderlem 7457 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩ ↔ (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
7674, 75imbi12i 339 . . . . . . . . . . . . . . . . . . . . . 22 (((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) → ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩) ↔ (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
7771, 76anbi12i 735 . . . . . . . . . . . . . . . . . . . . 21 ((¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ∧ ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) → ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩)) ↔ (¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))) ∧ (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))))
7868, 77syl6bb 276 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)) ↔ (¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))) ∧ (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))))
7955, 78syl5ibr 236 . . . . . . . . . . . . . . . . . . 19 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
8079expcomd 453 . . . . . . . . . . . . . . . . . 18 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
8180imp 444 . . . . . . . . . . . . . . . . 17 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
824, 81sylbi 207 . . . . . . . . . . . . . . . 16 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) ∧ (𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵))) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
83823exp 1113 . . . . . . . . . . . . . . 15 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8483com3l 89 . . . . . . . . . . . . . 14 ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8584exlimivv 2009 . . . . . . . . . . . . 13 (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8685com3l 89 . . . . . . . . . . . 12 ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8786exlimivv 2009 . . . . . . . . . . 11 (∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8887com3l 89 . . . . . . . . . 10 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → (∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8988exlimivv 2009 . . . . . . . . 9 (∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → (∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
90893imp 1102 . . . . . . . 8 ((∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ ∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) ∧ ∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵))) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
911, 2, 3, 90syl3anb 1165 . . . . . . 7 ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ (𝐴 × 𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
92913expia 1115 . . . . . 6 ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑣 ∈ (𝐴 × 𝐵) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
9392com3r 87 . . . . 5 ((𝑅 Po 𝐴𝑆 Po 𝐵) → ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑣 ∈ (𝐴 × 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
9493imp 444 . . . 4 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ (𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵))) → (𝑣 ∈ (𝐴 × 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
9594ralrimiv 3103 . . 3 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ (𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵))) → ∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
9695ralrimivva 3109 . 2 ((𝑅 Po 𝐴𝑆 Po 𝐵) → ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
97 df-po 5187 . 2 (𝑇 Po (𝐴 × 𝐵) ↔ ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
9896, 97sylibr 224 1 ((𝑅 Po 𝐴𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1072   = wceq 1632  wex 1853  wcel 2139  wral 3050  cop 4327   class class class wbr 4804  {copab 4864   Po wpo 5185   × cxp 5264  cfv 6049  1st c1st 7332  2nd c2nd 7333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-po 5187  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-iota 6012  df-fun 6051  df-fv 6057  df-1st 7334  df-2nd 7335
This theorem is referenced by:  soxp  7459
  Copyright terms: Public domain W3C validator