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

Theorem poxp 7818
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 5577 . . . . . . . 8 (𝑡 ∈ (𝐴 × 𝐵) ↔ ∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)))
2 elxp 5577 . . . . . . . 8 (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)))
3 elxp 5577 . . . . . . . 8 (𝑣 ∈ (𝐴 × 𝐵) ↔ ∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)))
4 3an6 1439 . . . . . . . . . . . . . . . . 17 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) ∧ (𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵))) ↔ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))))
5 poirr 5484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 Po 𝐴𝑎𝐴) → ¬ 𝑎𝑅𝑎)
65ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑅 Po 𝐴 → (𝑎𝐴 → ¬ 𝑎𝑅𝑎))
7 poirr 5484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑆 Po 𝐵𝑏𝐵) → ¬ 𝑏𝑆𝑏)
87intnand 489 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑆 Po 𝐵𝑏𝐵) → ¬ (𝑎 = 𝑎𝑏𝑆𝑏))
98ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑆 Po 𝐵 → (𝑏𝐵 → ¬ (𝑎 = 𝑎𝑏𝑆𝑏)))
106, 9im2anan9 619 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 Po 𝐴𝑆 Po 𝐵) → ((𝑎𝐴𝑏𝐵) → (¬ 𝑎𝑅𝑎 ∧ ¬ (𝑎 = 𝑎𝑏𝑆𝑏))))
11 ioran 979 . . . . . . . . . . . . . . . . . . . . . . . . 25 (¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏)) ↔ (¬ 𝑎𝑅𝑎 ∧ ¬ (𝑎 = 𝑎𝑏𝑆𝑏)))
1210, 11syl6ibr 253 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Po 𝐴𝑆 Po 𝐵) → ((𝑎𝐴𝑏𝐵) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
1312imp 407 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ (𝑎𝐴𝑏𝐵)) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏)))
1413intnand 489 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ (𝑎𝐴𝑏𝐵)) → ¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
15143ad2antr1 1182 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → ¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
16 an4 652 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) ↔ ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ ((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))))
17 3an6 1439 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵)) ↔ ((𝑎𝐴𝑐𝐴𝑒𝐴) ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)))
18 potr 5485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) → ((𝑎𝑅𝑐𝑐𝑅𝑒) → 𝑎𝑅𝑒))
19183impia 1111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴) ∧ (𝑎𝑅𝑐𝑐𝑅𝑒)) → 𝑎𝑅𝑒)
2019orcd 871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴) ∧ (𝑎𝑅𝑐𝑐𝑅𝑒)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))
21203expia 1115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) → ((𝑎𝑅𝑐𝑐𝑅𝑒) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
2221expdimp 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ 𝑎𝑅𝑐) → (𝑐𝑅𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
23 breq2 5067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑒 → (𝑎𝑅𝑐𝑎𝑅𝑒))
2423biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 = 𝑒𝑎𝑅𝑐) → 𝑎𝑅𝑒)
2524orcd 871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 = 𝑒𝑎𝑅𝑐) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))
2625expcom 414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎𝑅𝑐 → (𝑐 = 𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
2726adantrd 492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎𝑅𝑐 → ((𝑐 = 𝑒𝑑𝑆𝑓) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
2827adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ 𝑎𝑅𝑐) → ((𝑐 = 𝑒𝑑𝑆𝑓) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
2922, 28jaod 855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ 𝑎𝑅𝑐) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
3029ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) → (𝑎𝑅𝑐 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
31 potr 5485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) → ((𝑏𝑆𝑑𝑑𝑆𝑓) → 𝑏𝑆𝑓))
3231expdimp 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) ∧ 𝑏𝑆𝑑) → (𝑑𝑆𝑓𝑏𝑆𝑓))
3332anim2d 611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐 = 𝑒𝑑𝑆𝑓) → (𝑐 = 𝑒𝑏𝑆𝑓)))
3433orim2d 962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑏𝑆𝑓))))
35 breq1 5066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑎 = 𝑐 → (𝑎𝑅𝑒𝑐𝑅𝑒))
36 equequ1 2025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑎 = 𝑐 → (𝑎 = 𝑒𝑐 = 𝑒))
3736anbi1d 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑎 = 𝑐 → ((𝑎 = 𝑒𝑏𝑆𝑓) ↔ (𝑐 = 𝑒𝑏𝑆𝑓)))
3835, 37orbi12d 914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎 = 𝑐 → ((𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)) ↔ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑏𝑆𝑓))))
3938imbi2d 342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 = 𝑐 → (((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))) ↔ ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑏𝑆𝑓)))))
4034, 39syl5ibr 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 = 𝑐 → (((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
4140expd 416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 = 𝑐 → ((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))))
4241com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) → (𝑎 = 𝑐 → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))))
4342impd 411 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵)) → ((𝑎 = 𝑐𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
4430, 43jaao 950 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ (𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
4544impd 411 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑅 Po 𝐴 ∧ (𝑎𝐴𝑐𝐴𝑒𝐴)) ∧ (𝑆 Po 𝐵 ∧ (𝑏𝐵𝑑𝐵𝑓𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
4645an4s 656 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑐𝐴𝑒𝐴) ∧ (𝑏𝐵𝑑𝐵𝑓𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
4717, 46sylan2b 593 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
48 an4 652 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎𝐴𝑏𝐵) ∧ (𝑒𝐴𝑓𝐵)) ↔ ((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)))
4948biimpi 217 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑎𝐴𝑏𝐵) ∧ (𝑒𝐴𝑓𝐵)) → ((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)))
50493adant2 1125 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵)) → ((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)))
5150adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → ((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)))
5247, 51jctild 526 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
5352adantld 491 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ ((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
5416, 53syl5bi 243 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
5515, 54jca 512 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))) ∧ (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))))
56 breq12 5068 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑡 = ⟨𝑎, 𝑏⟩) → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
5756anidms 567 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
5857notbid 319 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = ⟨𝑎, 𝑏⟩ → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
59583ad2ant1 1127 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩))
60 breq12 5068 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩))
61603adant3 1126 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩))
62 breq12 5068 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑢𝑇𝑣 ↔ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩))
63623adant1 1124 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑢𝑇𝑣 ↔ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩))
6461, 63anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((𝑡𝑇𝑢𝑢𝑇𝑣) ↔ (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩)))
65 breq12 5068 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑣 ↔ ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩))
66653adant2 1125 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑣 ↔ ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩))
6764, 66imbi12d 346 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣) ↔ ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) → ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩)))
6859, 67anbi12d 630 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)) ↔ (¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ∧ ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) → ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩))))
69 poxp.1 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))}
7069xporderlem 7817 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ↔ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
7170notbii 321 . . . . . . . . . . . . . . . . . . . . . 22 (¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ↔ ¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))))
7269xporderlem 7817 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ↔ (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))))
7369xporderlem 7817 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩ ↔ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓))))
7472, 73anbi12i 626 . . . . . . . . . . . . . . . . . . . . . . 23 ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) ↔ ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))))
7569xporderlem 7817 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩ ↔ (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))
7674, 75imbi12i 352 . . . . . . . . . . . . . . . . . . . . . 22 (((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) → ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩) ↔ (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))
7771, 76anbi12i 626 . . . . . . . . . . . . . . . . . . . . 21 ((¬ ⟨𝑎, 𝑏𝑇𝑎, 𝑏⟩ ∧ ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑𝑇𝑒, 𝑓⟩) → ⟨𝑎, 𝑏𝑇𝑒, 𝑓⟩)) ↔ (¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))) ∧ (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓))))))
7868, 77syl6bb 288 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)) ↔ (¬ (((𝑎𝐴𝑎𝐴) ∧ (𝑏𝐵𝑏𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎𝑏𝑆𝑏))) ∧ (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∧ (((𝑐𝐴𝑒𝐴) ∧ (𝑑𝐵𝑓𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒𝑑𝑆𝑓)))) → (((𝑎𝐴𝑒𝐴) ∧ (𝑏𝐵𝑓𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒𝑏𝑆𝑓)))))))
7955, 78syl5ibr 247 . . . . . . . . . . . . . . . . . . 19 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
8079expcomd 417 . . . . . . . . . . . . . . . . . 18 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
8180imp 407 . . . . . . . . . . . . . . . . 17 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵) ∧ (𝑒𝐴𝑓𝐵))) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
824, 81sylbi 218 . . . . . . . . . . . . . . . 16 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) ∧ (𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵))) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
83823exp 1113 . . . . . . . . . . . . . . 15 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8483com3l 89 . . . . . . . . . . . . . 14 ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8584exlimivv 1926 . . . . . . . . . . . . 13 (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8685com3l 89 . . . . . . . . . . . 12 ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8786exlimivv 1926 . . . . . . . . . . 11 (∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8887com3l 89 . . . . . . . . . 10 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → (∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
8988exlimivv 1926 . . . . . . . . 9 (∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → (∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
90893imp 1105 . . . . . . . 8 ((∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ ∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) ∧ ∃𝑒𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒𝐴𝑓𝐵))) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
911, 2, 3, 90syl3anb 1155 . . . . . . 7 ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ (𝐴 × 𝐵)) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
92913expia 1115 . . . . . 6 ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑣 ∈ (𝐴 × 𝐵) → ((𝑅 Po 𝐴𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
9392com3r 87 . . . . 5 ((𝑅 Po 𝐴𝑆 Po 𝐵) → ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑣 ∈ (𝐴 × 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
9493imp 407 . . . 4 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ (𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵))) → (𝑣 ∈ (𝐴 × 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
9594ralrimiv 3186 . . 3 (((𝑅 Po 𝐴𝑆 Po 𝐵) ∧ (𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵))) → ∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
9695ralrimivva 3196 . 2 ((𝑅 Po 𝐴𝑆 Po 𝐵) → ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
97 df-po 5473 . 2 (𝑇 Po (𝐴 × 𝐵) ↔ ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
9896, 97sylibr 235 1 ((𝑅 Po 𝐴𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 843  w3a 1081   = wceq 1530  wex 1773  wcel 2107  wral 3143  cop 4570   class class class wbr 5063  {copab 5125   Po wpo 5471   × cxp 5552  cfv 6354  1st c1st 7683  2nd c2nd 7684
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-po 5473  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-iota 6313  df-fun 6356  df-fv 6362  df-1st 7685  df-2nd 7686
This theorem is referenced by:  soxp  7819
  Copyright terms: Public domain W3C validator