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

Theorem poxp 5932
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 4418 . . . . . . . 8 (𝑡 ∈ (𝐴 × 𝐵) ↔ ∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)))
2 elxp 4418 . . . . . . . 8 (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)))
3 elxp 4418 . . . . . . . 8 (𝑣 ∈ (𝐴 × 𝐵) ↔ ∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)))
4 3an6 1254 . . . . . . . . . . . . . . . . 17 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) ∧ (𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵))) ↔ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))))
5 poirr 4098 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 Po 𝐴𝑎𝐴) → ¬ 𝑎𝑅𝑎)
65ex 113 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑅 Po 𝐴 → (𝑎𝐴 → ¬ 𝑎𝑅𝑎))
7 poirr 4098 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑆 Po 𝐵𝑏𝐵) → ¬ 𝑏𝑆𝑏)
87intnand 874 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 874 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ (𝑎𝐴𝑏𝐵)) → ¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
15143ad2antr1 1104 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → ¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
16 an4 551 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) ↔ ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ ((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))))
17 3an6 1254 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵)) ↔ ((𝑎𝐴𝑐𝐴𝑒𝐴) ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)))
18 potr 4099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) → ((𝑎𝑅𝑐𝑐𝑅𝑒) → 𝑎𝑅𝑒))
19183impia 1136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴) ∧ (𝑎𝑅𝑐𝑐𝑅𝑒)) → 𝑎𝑅𝑒)
2019orcd 685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴) ∧ (𝑎𝑅𝑐𝑐𝑅𝑒)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))
21203expia 1141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) → ((𝑎𝑅𝑐𝑐𝑅𝑒) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
2221expdimp 255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ 𝑎𝑅𝑐) → (𝑐𝑅𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
23 breq2 3815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) → ((𝑏𝑆𝑑𝑑𝑆𝑓) → 𝑏𝑆𝑓))
3231expdimp 255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) ∧ 𝑏𝑆𝑑) → (𝑑𝑆𝑓𝑏𝑆𝑓))
3332anim2d 330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐 = 𝑒𝑑𝑆𝑓) → (𝑐 = 𝑒𝑏𝑆𝑓)))
3433orim2d 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑏𝑆𝑓))))
35 breq1 3814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑎 = 𝑐 → (𝑎𝑅𝑒𝑐𝑅𝑒))
36 equequ1 1640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 958 . . . . . . . . . . . . . . . . . . . . . . . . 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 3816 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑡 = ⟨𝑎, 𝑏⟩) → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
5756anidms 389 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
5857notbid 625 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = ⟨𝑎, 𝑏⟩ → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
59583ad2ant1 960 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
60 breq12 3816 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩))
61603adant3 959 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩))
62 breq12 3816 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑢𝑇𝑣 ↔ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩))
63623adant1 957 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑢𝑇𝑣 ↔ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩))
6461, 63anbi12d 457 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((𝑡𝑇𝑢𝑢𝑇𝑣) ↔ (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩)))
65 breq12 3816 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑣 ↔ ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩))
66653adant2 958 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑣 ↔ ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩))
6764, 66imbi12d 232 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣) ↔ ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) → ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩)))
6859, 67anbi12d 457 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)) ↔ (¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ∧ ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) → ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩))))
69 poxp.1 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))}
7069xporderlem 5931 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ↔ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
7170notbii 627 . . . . . . . . . . . . . . . . . . . . . 22 (¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ↔ ¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
7269xporderlem 5931 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ↔ (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))))
7369xporderlem 5931 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩ ↔ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))))
7472, 73anbi12i 448 . . . . . . . . . . . . . . . . . . . . . . 23 ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) ↔ ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))))
7569xporderlem 5931 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩ ↔ (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
7674, 75imbi12i 237 . . . . . . . . . . . . . . . . . . . . . 22 (((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) → ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩) ↔ (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
7771, 76anbi12i 448 . . . . . . . . . . . . . . . . . . . . 21 ((¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ∧ ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) → ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩)) ↔ (¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))) ∧ (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))))
7868, 77syl6bb 194 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)) ↔ (¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))) ∧ (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))))
7955, 78syl5ibr 154 . . . . . . . . . . . . . . . . . . 19 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
8079expcomd 1371 . . . . . . . . . . . . . . . . . 18 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
8180imp 122 . . . . . . . . . . . . . . . . 17 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
824, 81sylbi 119 . . . . . . . . . . . . . . . 16 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) ∧ (𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵))) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
83823exp 1138 . . . . . . . . . . . . . . 15 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8483com3l 80 . . . . . . . . . . . . . 14 ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8584exlimivv 1819 . . . . . . . . . . . . 13 (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8685com3l 80 . . . . . . . . . . . 12 ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8786exlimivv 1819 . . . . . . . . . . 11 (∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8887com3l 80 . . . . . . . . . 10 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → (∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8988exlimivv 1819 . . . . . . . . 9 (∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → (∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
90893imp 1133 . . . . . . . 8 ((∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ ∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) ∧ ∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵))) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
911, 2, 3, 90syl3anb 1213 . . . . . . 7 ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ (𝐴 × 𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
92913expia 1141 . . . . . 6 ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑣 ∈ (𝐴 × 𝐵) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
9392com3r 78 . . . . 5 ((𝑅 Po 𝐴𝑆 Po 𝐵) → ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑣 ∈ (𝐴 × 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
9493imp 122 . . . 4 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ (𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵))) → (𝑣 ∈ (𝐴 × 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
9594ralrimiv 2439 . . 3 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ (𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵))) → ∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
9695ralrimivva 2449 . 2 ((𝑅 Po 𝐴𝑆 Po 𝐵) → ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
97 df-po 4087 . 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 920   = wceq 1285  wex 1422  wcel 1434  wral 2353  cop 3425   class class class wbr 3811  {copab 3864   Po wpo 4085   × cxp 4399  cfv 4969  1st c1st 5844  2nd c2nd 5845
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-pow 3974  ax-pr 4000  ax-un 4224
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2614  df-sbc 2827  df-un 2988  df-in 2990  df-ss 2997  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-br 3812  df-opab 3866  df-mpt 3867  df-id 4084  df-po 4087  df-xp 4407  df-rel 4408  df-cnv 4409  df-co 4410  df-dm 4411  df-rn 4412  df-iota 4934  df-fun 4971  df-fv 4977  df-1st 5846  df-2nd 5847
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator