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

Theorem poxp 5956
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 4430 . . . . . . . 8 (𝑡 ∈ (𝐴 × 𝐵) ↔ ∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)))
2 elxp 4430 . . . . . . . 8 (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)))
3 elxp 4430 . . . . . . . 8 (𝑣 ∈ (𝐴 × 𝐵) ↔ ∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)))
4 3an6 1256 . . . . . . . . . . . . . . . . 17 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) ∧ (𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵))) ↔ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))))
5 poirr 4110 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 Po 𝐴𝑎𝐴) → ¬ 𝑎𝑅𝑎)
65ex 113 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑅 Po 𝐴 → (𝑎𝐴 → ¬ 𝑎𝑅𝑎))
7 poirr 4110 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑆 Po 𝐵𝑏𝐵) → ¬ 𝑏𝑆𝑏)
87intnand 876 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑆 Po 𝐵𝑏𝐵) → ¬ (𝑎 = 𝑎𝑏𝑆𝑏))
98ex 113 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑆 Po 𝐵 → (𝑏𝐵 → ¬ (𝑎 = 𝑎𝑏𝑆𝑏)))
106, 9im2anan9 563 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 Po 𝐴𝑆 Po 𝐵) → ((𝑎𝐴𝑏𝐵) → (¬ 𝑎𝑅𝑎 ∧ ¬ (𝑎 = 𝑎𝑏𝑆𝑏))))
11 ioran 702 . . . . . . . . . . . . . . . . . . . . . . . . 25 (¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏)) ↔ (¬ 𝑎𝑅𝑎 ∧ ¬ (𝑎 = 𝑎𝑏𝑆𝑏)))
1210, 11syl6ibr 160 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Po 𝐴𝑆 Po 𝐵) → ((𝑎𝐴𝑏𝐵) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
1312imp 122 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ (𝑎𝐴𝑏𝐵)) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏)))
1413intnand 876 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ (𝑎𝐴𝑏𝐵)) → ¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
15143ad2antr1 1106 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → ¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
16 an4 551 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) ↔ ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ ((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))))
17 3an6 1256 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵)) ↔ ((𝑎𝐴𝑐𝐴𝑒𝐴) ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)))
18 potr 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) → ((𝑎𝑅𝑐𝑐𝑅𝑒) → 𝑎𝑅𝑒))
19183impia 1138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴) ∧ (𝑎𝑅𝑐𝑐𝑅𝑒)) → 𝑎𝑅𝑒)
2019orcd 685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴) ∧ (𝑎𝑅𝑐𝑐𝑅𝑒)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))
21203expia 1143 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) → ((𝑎𝑅𝑐𝑐𝑅𝑒) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
2221expdimp 255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ 𝑎𝑅𝑐) → (𝑐𝑅𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
23 breq2 3826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑒 → (𝑎𝑅𝑐𝑎𝑅𝑒))
2423biimpa 290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 = 𝑒𝑎𝑅𝑐) → 𝑎𝑅𝑒)
2524orcd 685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 = 𝑒𝑎𝑅𝑐) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))
2625expcom 114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎𝑅𝑐 → (𝑐 = 𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
2726adantrd 273 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎𝑅𝑐 → ((𝑐 = 𝑒𝑑𝑆𝑓) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
2827adantl 271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ 𝑎𝑅𝑐) → ((𝑐 = 𝑒𝑑𝑆𝑓) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
2922, 28jaod 670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ 𝑎𝑅𝑐) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
3029ex 113 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) → (𝑎𝑅𝑐 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
31 potr 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) → ((𝑏𝑆𝑑𝑑𝑆𝑓) → 𝑏𝑆𝑓))
3231expdimp 255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) ∧ 𝑏𝑆𝑑) → (𝑑𝑆𝑓𝑏𝑆𝑓))
3332anim2d 330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐 = 𝑒𝑑𝑆𝑓) → (𝑐 = 𝑒𝑏𝑆𝑓)))
3433orim2d 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑏𝑆𝑓))))
35 breq1 3825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑎 = 𝑐 → (𝑎𝑅𝑒𝑐𝑅𝑒))
36 equequ1 1642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑎 = 𝑐 → (𝑎 = 𝑒𝑐 = 𝑒))
3736anbi1d 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑎 = 𝑐 → ((𝑎 = 𝑒𝑏𝑆𝑓) ↔ (𝑐 = 𝑒𝑏𝑆𝑓)))
3835, 37orbi12d 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎 = 𝑐 → ((𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)) ↔ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑏𝑆𝑓))))
3938imbi2d 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 = 𝑐 → (((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))) ↔ ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑏𝑆𝑓)))))
4034, 39syl5ibr 154 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 = 𝑐 → (((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
4140expd 254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 = 𝑐 → ((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))))
4241com12 30 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) → (𝑎 = 𝑐 → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))))
4342impd 251 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) → ((𝑎 = 𝑐𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
4430, 43jaao 672 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ (𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
4544impd 251 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ (𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
4645an4s 553 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑐𝐴𝑒𝐴) ∧ (𝑏𝐵𝑑𝐵𝑓𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
4717, 46sylan2b 281 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
48 an4 551 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎𝐴𝑏𝐵) ∧ (𝑒𝐴𝑓𝐵)) ↔ ((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)))
4948biimpi 118 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑎𝐴𝑏𝐵) ∧ (𝑒𝐴𝑓𝐵)) → ((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)))
50493adant2 960 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵)) → ((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)))
5150adantl 271 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → ((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)))
5247, 51jctild 309 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
5352adantld 272 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ ((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
5416, 53syl5bi 150 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
5515, 54jca 300 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))) ∧ (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))))
56 breq12 3827 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑡 = ⟨𝑎, 𝑏⟩) → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
5756anidms 389 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
5857notbid 625 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = ⟨𝑎, 𝑏⟩ → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
59583ad2ant1 962 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
60 breq12 3827 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩))
61603adant3 961 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩))
62 breq12 3827 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑢𝑇𝑣 ↔ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩))
63623adant1 959 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑢𝑇𝑣 ↔ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩))
6461, 63anbi12d 457 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((𝑡𝑇𝑢𝑢𝑇𝑣) ↔ (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩)))
65 breq12 3827 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑣 ↔ ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩))
66653adant2 960 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑣 ↔ ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩))
6764, 66imbi12d 232 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣) ↔ ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) → ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩)))
6859, 67anbi12d 457 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)) ↔ (¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ∧ ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) → ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩))))
69 poxp.1 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))}
7069xporderlem 5955 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ↔ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
7170notbii 627 . . . . . . . . . . . . . . . . . . . . . 22 (¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ↔ ¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
7269xporderlem 5955 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ↔ (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))))
7369xporderlem 5955 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩ ↔ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))))
7472, 73anbi12i 448 . . . . . . . . . . . . . . . . . . . . . . 23 ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) ↔ ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))))
7569xporderlem 5955 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩ ↔ (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
7674, 75imbi12i 237 . . . . . . . . . . . . . . . . . . . . . 22 (((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) → ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩) ↔ (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
7771, 76anbi12i 448 . . . . . . . . . . . . . . . . . . . . 21 ((¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ∧ ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) → ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩)) ↔ (¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))) ∧ (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))))
7868, 77syl6bb 194 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)) ↔ (¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))) ∧ (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))))
7955, 78syl5ibr 154 . . . . . . . . . . . . . . . . . . 19 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
8079expcomd 1373 . . . . . . . . . . . . . . . . . 18 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
8180imp 122 . . . . . . . . . . . . . . . . 17 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
824, 81sylbi 119 . . . . . . . . . . . . . . . 16 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) ∧ (𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵))) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
83823exp 1140 . . . . . . . . . . . . . . 15 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8483com3l 80 . . . . . . . . . . . . . 14 ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8584exlimivv 1821 . . . . . . . . . . . . 13 (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8685com3l 80 . . . . . . . . . . . 12 ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8786exlimivv 1821 . . . . . . . . . . 11 (∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8887com3l 80 . . . . . . . . . 10 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → (∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8988exlimivv 1821 . . . . . . . . 9 (∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → (∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
90893imp 1135 . . . . . . . 8 ((∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ ∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) ∧ ∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵))) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
911, 2, 3, 90syl3anb 1215 . . . . . . 7 ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ (𝐴 × 𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
92913expia 1143 . . . . . 6 ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑣 ∈ (𝐴 × 𝐵) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
9392com3r 78 . . . . 5 ((𝑅 Po 𝐴𝑆 Po 𝐵) → ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑣 ∈ (𝐴 × 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
9493imp 122 . . . 4 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ (𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵))) → (𝑣 ∈ (𝐴 × 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
9594ralrimiv 2441 . . 3 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ (𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵))) → ∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
9695ralrimivva 2451 . 2 ((𝑅 Po 𝐴𝑆 Po 𝐵) → ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
97 df-po 4099 . 2 (𝑇 Po (𝐴 × 𝐵) ↔ ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
9896, 97sylibr 132 1 ((𝑅 Po 𝐴𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  wo 662  w3a 922   = wceq 1287  wex 1424  wcel 1436  wral 2355  cop 3434   class class class wbr 3822  {copab 3875   Po wpo 4097   × cxp 4411  cfv 4983  1st c1st 5868  2nd c2nd 5869
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3934  ax-pow 3986  ax-pr 4012  ax-un 4236
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-v 2617  df-sbc 2830  df-un 2992  df-in 2994  df-ss 3001  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-br 3823  df-opab 3877  df-mpt 3878  df-id 4096  df-po 4099  df-xp 4419  df-rel 4420  df-cnv 4421  df-co 4422  df-dm 4423  df-rn 4424  df-iota 4948  df-fun 4985  df-fv 4991  df-1st 5870  df-2nd 5871
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator