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

Theorem poxp 7334
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 5165 . . . . . . . 8 (𝑡 ∈ (𝐴 × 𝐵) ↔ ∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)))
2 elxp 5165 . . . . . . . 8 (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)))
3 elxp 5165 . . . . . . . 8 (𝑣 ∈ (𝐴 × 𝐵) ↔ ∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)))
4 3an6 1449 . . . . . . . . . . . . . . . . 17 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) ∧ (𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵))) ↔ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))))
5 poirr 5075 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 Po 𝐴𝑎𝐴) → ¬ 𝑎𝑅𝑎)
65ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑅 Po 𝐴 → (𝑎𝐴 → ¬ 𝑎𝑅𝑎))
7 poirr 5075 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑆 Po 𝐵𝑏𝐵) → ¬ 𝑏𝑆𝑏)
87intnand 982 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑆 Po 𝐵𝑏𝐵) → ¬ (𝑎 = 𝑎𝑏𝑆𝑏))
98ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑆 Po 𝐵 → (𝑏𝐵 → ¬ (𝑎 = 𝑎𝑏𝑆𝑏)))
106, 9im2anan9 898 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 Po 𝐴𝑆 Po 𝐵) → ((𝑎𝐴𝑏𝐵) → (¬ 𝑎𝑅𝑎 ∧ ¬ (𝑎 = 𝑎𝑏𝑆𝑏))))
11 ioran 510 . . . . . . . . . . . . . . . . . . . . . . . . 25 (¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏)) ↔ (¬ 𝑎𝑅𝑎 ∧ ¬ (𝑎 = 𝑎𝑏𝑆𝑏)))
1210, 11syl6ibr 242 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Po 𝐴𝑆 Po 𝐵) → ((𝑎𝐴𝑏𝐵) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
1312imp 444 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ (𝑎𝐴𝑏𝐵)) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏)))
1413intnand 982 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ (𝑎𝐴𝑏𝐵)) → ¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
15143ad2antr1 1246 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → ¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
16 an4 882 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) ↔ ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ ((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))))
17 3an6 1449 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵)) ↔ ((𝑎𝐴𝑐𝐴𝑒𝐴) ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)))
18 potr 5076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) → ((𝑎𝑅𝑐𝑐𝑅𝑒) → 𝑎𝑅𝑒))
19183impia 1280 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴) ∧ (𝑎𝑅𝑐𝑐𝑅𝑒)) → 𝑎𝑅𝑒)
2019orcd 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴) ∧ (𝑎𝑅𝑐𝑐𝑅𝑒)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))
21203expia 1286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) → ((𝑎𝑅𝑐𝑐𝑅𝑒) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
2221expdimp 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ 𝑎𝑅𝑐) → (𝑐𝑅𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
23 breq2 4689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑒 → (𝑎𝑅𝑐𝑎𝑅𝑒))
2423biimpa 500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 = 𝑒𝑎𝑅𝑐) → 𝑎𝑅𝑒)
2524orcd 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 = 𝑒𝑎𝑅𝑐) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))
2625expcom 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎𝑅𝑐 → (𝑐 = 𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
2726adantrd 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎𝑅𝑐 → ((𝑐 = 𝑒𝑑𝑆𝑓) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
2827adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ 𝑎𝑅𝑐) → ((𝑐 = 𝑒𝑑𝑆𝑓) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
2922, 28jaod 394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ 𝑎𝑅𝑐) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
3029ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) → (𝑎𝑅𝑐 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
31 potr 5076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) → ((𝑏𝑆𝑑𝑑𝑆𝑓) → 𝑏𝑆𝑓))
3231expdimp 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) ∧ 𝑏𝑆𝑑) → (𝑑𝑆𝑓𝑏𝑆𝑓))
3332anim2d 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐 = 𝑒𝑑𝑆𝑓) → (𝑐 = 𝑒𝑏𝑆𝑓)))
3433orim2d 903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑏𝑆𝑓))))
35 breq1 4688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑎 = 𝑐 → (𝑎𝑅𝑒𝑐𝑅𝑒))
36 equequ1 1998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑎 = 𝑐 → (𝑎 = 𝑒𝑐 = 𝑒))
3736anbi1d 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑎 = 𝑐 → ((𝑎 = 𝑒𝑏𝑆𝑓) ↔ (𝑐 = 𝑒𝑏𝑆𝑓)))
3835, 37orbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎 = 𝑐 → ((𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)) ↔ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑏𝑆𝑓))))
3938imbi2d 329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 = 𝑐 → (((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))) ↔ ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑏𝑆𝑓)))))
4034, 39syl5ibr 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 = 𝑐 → (((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
4140expd 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 = 𝑐 → ((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))))
4241com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) → (𝑎 = 𝑐 → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))))
4342impd 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) → ((𝑎 = 𝑐𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
4430, 43jaao 530 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ (𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
4544impd 446 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ (𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
4645an4s 886 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑐𝐴𝑒𝐴) ∧ (𝑏𝐵𝑑𝐵𝑓𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
4717, 46sylan2b 491 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
48 an4 882 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎𝐴𝑏𝐵) ∧ (𝑒𝐴𝑓𝐵)) ↔ ((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)))
4948biimpi 206 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑎𝐴𝑏𝐵) ∧ (𝑒𝐴𝑓𝐵)) → ((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)))
50493adant2 1100 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵)) → ((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)))
5150adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → ((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)))
5247, 51jctild 565 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
5352adantld 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ ((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
5416, 53syl5bi 232 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
5515, 54jca 553 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))) ∧ (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))))
56 breq12 4690 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑡 = ⟨𝑎, 𝑏⟩) → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
5756anidms 678 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
5857notbid 307 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = ⟨𝑎, 𝑏⟩ → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
59583ad2ant1 1102 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
60 breq12 4690 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩))
61603adant3 1101 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩))
62 breq12 4690 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑢𝑇𝑣 ↔ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩))
63623adant1 1099 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑢𝑇𝑣 ↔ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩))
6461, 63anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((𝑡𝑇𝑢𝑢𝑇𝑣) ↔ (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩)))
65 breq12 4690 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑣 ↔ ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩))
66653adant2 1100 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑣 ↔ ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩))
6764, 66imbi12d 333 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣) ↔ ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) → ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩)))
6859, 67anbi12d 747 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)) ↔ (¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ∧ ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) → ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩))))
69 poxp.1 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))}
7069xporderlem 7333 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ↔ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
7170notbii 309 . . . . . . . . . . . . . . . . . . . . . 22 (¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ↔ ¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
7269xporderlem 7333 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ↔ (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))))
7369xporderlem 7333 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩ ↔ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))))
7472, 73anbi12i 733 . . . . . . . . . . . . . . . . . . . . . . 23 ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) ↔ ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))))
7569xporderlem 7333 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩ ↔ (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
7674, 75imbi12i 339 . . . . . . . . . . . . . . . . . . . . . 22 (((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) → ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩) ↔ (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
7771, 76anbi12i 733 . . . . . . . . . . . . . . . . . . . . 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 1283 . . . . . . . . . . . . . . 15 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8483com3l 89 . . . . . . . . . . . . . 14 ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8584exlimivv 1900 . . . . . . . . . . . . 13 (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8685com3l 89 . . . . . . . . . . . 12 ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8786exlimivv 1900 . . . . . . . . . . 11 (∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8887com3l 89 . . . . . . . . . 10 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → (∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8988exlimivv 1900 . . . . . . . . 9 (∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → (∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
90893imp 1275 . . . . . . . 8 ((∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ ∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) ∧ ∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵))) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
911, 2, 3, 90syl3anb 1409 . . . . . . 7 ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ (𝐴 × 𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
92913expia 1286 . . . . . 6 ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑣 ∈ (𝐴 × 𝐵) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
9392com3r 87 . . . . 5 ((𝑅 Po 𝐴𝑆 Po 𝐵) → ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑣 ∈ (𝐴 × 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
9493imp 444 . . . 4 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ (𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵))) → (𝑣 ∈ (𝐴 × 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
9594ralrimiv 2994 . . 3 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ (𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵))) → ∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
9695ralrimivva 3000 . 2 ((𝑅 Po 𝐴𝑆 Po 𝐵) → ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
97 df-po 5064 . 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 1054   = wceq 1523  wex 1744  wcel 2030  wral 2941  cop 4216   class class class wbr 4685  {copab 4745   Po wpo 5062   × cxp 5141  cfv 5926  1st c1st 7208  2nd c2nd 7209
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-po 5064  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-iota 5889  df-fun 5928  df-fv 5934  df-1st 7210  df-2nd 7211
This theorem is referenced by:  soxp  7335
  Copyright terms: Public domain W3C validator