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

Theorem soxp 7521
Description: A lexicographical ordering of two strictly ordered classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.)
Hypothesis
Ref Expression
soxp.1 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))}
Assertion
Ref Expression
soxp ((𝑅 Or 𝐴𝑆 Or 𝐵) → 𝑇 Or (𝐴 × 𝐵))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝑅,𝑦   𝑥,𝑆,𝑦
Allowed substitution hints:   𝑇(𝑥,𝑦)

Proof of Theorem soxp
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑡 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sopo 5246 . . 3 (𝑅 Or 𝐴𝑅 Po 𝐴)
2 sopo 5246 . . 3 (𝑆 Or 𝐵𝑆 Po 𝐵)
3 soxp.1 . . . 4 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))}
43poxp 7520 . . 3 ((𝑅 Po 𝐴𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵))
51, 2, 4syl2an 585 . 2 ((𝑅 Or 𝐴𝑆 Or 𝐵) → 𝑇 Po (𝐴 × 𝐵))
6 elxp 5330 . . . . 5 (𝑡 ∈ (𝐴 × 𝐵) ↔ ∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)))
7 elxp 5330 . . . . 5 (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)))
8 ioran 997 . . . . . . . . . . . . . . . . . . . . 21 (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) ↔ (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ ¬ (𝑎 = 𝑐𝑏 = 𝑑)))
9 ioran 997 . . . . . . . . . . . . . . . . . . . . . . 23 (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ ¬ (𝑎 = 𝑐𝑏𝑆𝑑)))
10 ianor 995 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ (𝑎 = 𝑐𝑏𝑆𝑑) ↔ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑))
1110anbi2i 611 . . . . . . . . . . . . . . . . . . . . . . 23 ((¬ 𝑎𝑅𝑐 ∧ ¬ (𝑎 = 𝑐𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)))
129, 11bitri 266 . . . . . . . . . . . . . . . . . . . . . 22 (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)))
13 ianor 995 . . . . . . . . . . . . . . . . . . . . . 22 (¬ (𝑎 = 𝑐𝑏 = 𝑑) ↔ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑))
1412, 13anbi12i 614 . . . . . . . . . . . . . . . . . . . . 21 ((¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ ¬ (𝑎 = 𝑐𝑏 = 𝑑)) ↔ ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)))
158, 14bitri 266 . . . . . . . . . . . . . . . . . . . 20 (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) ↔ ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)))
16 solin 5252 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) → (𝑎𝑅𝑐𝑎 = 𝑐𝑐𝑅𝑎))
17 3orass 1103 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎𝑅𝑐𝑎 = 𝑐𝑐𝑅𝑎) ↔ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑐𝑅𝑎)))
18 df-or 866 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑐𝑅𝑎)) ↔ (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐𝑐𝑅𝑎)))
1917, 18bitri 266 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝑅𝑐𝑎 = 𝑐𝑐𝑅𝑎) ↔ (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐𝑐𝑅𝑎)))
2016, 19sylib 209 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) → (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐𝑐𝑅𝑎)))
21 solin 5252 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵)) → (𝑏𝑆𝑑𝑏 = 𝑑𝑑𝑆𝑏))
22 3orass 1103 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑏𝑆𝑑𝑏 = 𝑑𝑑𝑆𝑏) ↔ (𝑏𝑆𝑑 ∨ (𝑏 = 𝑑𝑑𝑆𝑏)))
23 df-or 866 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑏𝑆𝑑 ∨ (𝑏 = 𝑑𝑑𝑆𝑏)) ↔ (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑𝑑𝑆𝑏)))
2422, 23bitri 266 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏𝑆𝑑𝑏 = 𝑑𝑑𝑆𝑏) ↔ (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑𝑑𝑆𝑏)))
2521, 24sylib 209 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵)) → (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑𝑑𝑆𝑏)))
2625orim2d 980 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵)) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑) → (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏))))
2720, 26im2anan9 608 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) → ((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏)))))
28 pm2.53 869 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 = 𝑐𝑐𝑅𝑎) → (¬ 𝑎 = 𝑐𝑐𝑅𝑎))
29 orc 885 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐𝑅𝑎 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))
3028, 29syl6 35 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎 = 𝑐𝑐𝑅𝑎) → (¬ 𝑎 = 𝑐 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
3130adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏))) → (¬ 𝑎 = 𝑐 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
32 orel1 904 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑏 = 𝑑 → ((𝑏 = 𝑑𝑑𝑆𝑏) → 𝑑𝑆𝑏))
3332orim2d 980 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑏 = 𝑑 → ((¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏)) → (¬ 𝑎 = 𝑐𝑑𝑆𝑏)))
3433anim2d 601 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑏 = 𝑑 → (((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏))) → ((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐𝑑𝑆𝑏))))
35 imor 871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎 = 𝑐𝑑𝑆𝑏) ↔ (¬ 𝑎 = 𝑐𝑑𝑆𝑏))
3635biimpri 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((¬ 𝑎 = 𝑐𝑑𝑆𝑏) → (𝑎 = 𝑐𝑑𝑆𝑏))
3736com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑐 → ((¬ 𝑎 = 𝑐𝑑𝑆𝑏) → 𝑑𝑆𝑏))
38 equcomi 2115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 = 𝑐𝑐 = 𝑎)
3938anim1i 604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎 = 𝑐𝑑𝑆𝑏) → (𝑐 = 𝑎𝑑𝑆𝑏))
4039olcd 892 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 = 𝑐𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))
4140ex 399 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑐 → (𝑑𝑆𝑏 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4237, 41syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑐 → ((¬ 𝑎 = 𝑐𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4329a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐𝑅𝑎 → ((¬ 𝑎 = 𝑐𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4442, 43jaoi 875 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 = 𝑐𝑐𝑅𝑎) → ((¬ 𝑎 = 𝑐𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4544imp 395 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐𝑑𝑆𝑏)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))
4634, 45syl6com 37 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏))) → (¬ 𝑏 = 𝑑 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4731, 46jaod 877 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏))) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4827, 47syl6 35 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
4948impd 398 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → (((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
5015, 49syl5bi 233 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
51 df-3or 1101 . . . . . . . . . . . . . . . . . . . 20 (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))) ↔ (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
52 df-or 866 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))) ↔ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
5351, 52bitri 266 . . . . . . . . . . . . . . . . . . 19 (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))) ↔ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
5450, 53sylibr 225 . . . . . . . . . . . . . . . . . 18 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
55 pm3.2 457 . . . . . . . . . . . . . . . . . . . 20 (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) → (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)))))
5655ad2ant2l 743 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) → (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)))))
57 idd 24 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((𝑎 = 𝑐𝑏 = 𝑑) → (𝑎 = 𝑐𝑏 = 𝑑)))
58 simpr 473 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) → (𝑎𝐴𝑐𝐴))
5958ancomd 451 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) → (𝑐𝐴𝑎𝐴))
60 simpr 473 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵)) → (𝑏𝐵𝑑𝐵))
6160ancomd 451 . . . . . . . . . . . . . . . . . . . 20 ((𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵)) → (𝑑𝐵𝑏𝐵))
62 pm3.2 457 . . . . . . . . . . . . . . . . . . . 20 (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) → ((𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)) → (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
6359, 61, 62syl2an 585 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)) → (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
6456, 57, 633orim123d 1561 . . . . . . . . . . . . . . . . . 18 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))) → ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))))
6554, 64mpd 15 . . . . . . . . . . . . . . . . 17 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
6665an4s 642 . . . . . . . . . . . . . . . 16 (((𝑅 Or 𝐴𝑆 Or 𝐵) ∧ ((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵))) → ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
6766expcom 400 . . . . . . . . . . . . . . 15 (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))))
6867an4s 642 . . . . . . . . . . . . . 14 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))))
69 breq12 4845 . . . . . . . . . . . . . . . . 17 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩))
70 eqeq12 2818 . . . . . . . . . . . . . . . . 17 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡 = 𝑢 ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
71 breq12 4845 . . . . . . . . . . . . . . . . . 18 ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑡 = ⟨𝑎, 𝑏⟩) → (𝑢𝑇𝑡 ↔ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩))
7271ancoms 448 . . . . . . . . . . . . . . . . 17 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑢𝑇𝑡 ↔ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩))
7369, 70, 723orbi123d 1552 . . . . . . . . . . . . . . . 16 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → ((𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡) ↔ (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∨ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ∨ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩)))
743xporderlem 7519 . . . . . . . . . . . . . . . . 17 (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ↔ (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))))
75 vex 3393 . . . . . . . . . . . . . . . . . 18 𝑎 ∈ V
76 vex 3393 . . . . . . . . . . . . . . . . . 18 𝑏 ∈ V
7775, 76opth 5131 . . . . . . . . . . . . . . . . 17 (⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ↔ (𝑎 = 𝑐𝑏 = 𝑑))
783xporderlem 7519 . . . . . . . . . . . . . . . . 17 (⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩ ↔ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
7974, 77, 783orbi123i 1188 . . . . . . . . . . . . . . . 16 ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∨ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ∨ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩) ↔ ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
8073, 79syl6bb 278 . . . . . . . . . . . . . . 15 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → ((𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡) ↔ ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))))
8180biimprcd 241 . . . . . . . . . . . . . 14 (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
8268, 81syl6 35 . . . . . . . . . . . . 13 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
8382com3r 87 . . . . . . . . . . . 12 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
8483imp 395 . . . . . . . . . . 11 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵))) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
8584an4s 642 . . . . . . . . . 10 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵))) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
8685expcom 400 . . . . . . . . 9 ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
8786exlimivv 2025 . . . . . . . 8 (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
8887com12 32 . . . . . . 7 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
8988exlimivv 2025 . . . . . 6 (∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
9089imp 395 . . . . 5 ((∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ ∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵))) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
916, 7, 90syl2anb 587 . . . 4 ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
9291com12 32 . . 3 ((𝑅 Or 𝐴𝑆 Or 𝐵) → ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
9392ralrimivv 3157 . 2 ((𝑅 Or 𝐴𝑆 Or 𝐵) → ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)(𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))
94 df-so 5230 . 2 (𝑇 Or (𝐴 × 𝐵) ↔ (𝑇 Po (𝐴 × 𝐵) ∧ ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)(𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
955, 93, 94sylanbrc 574 1 ((𝑅 Or 𝐴𝑆 Or 𝐵) → 𝑇 Or (𝐴 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3o 1099   = wceq 1637  wex 1859  wcel 2158  wral 3095  cop 4373   class class class wbr 4840  {copab 4902   Po wpo 5227   Or wor 5228   × cxp 5306  cfv 6098  1st c1st 7393  2nd c2nd 7394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ral 3100  df-rex 3101  df-rab 3104  df-v 3392  df-sbc 3631  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-nul 4114  df-if 4277  df-sn 4368  df-pr 4370  df-op 4374  df-uni 4627  df-br 4841  df-opab 4903  df-mpt 4920  df-id 5216  df-po 5229  df-so 5230  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-iota 6061  df-fun 6100  df-fv 6106  df-1st 7395  df-2nd 7396
This theorem is referenced by:  wexp  7522
  Copyright terms: Public domain W3C validator