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

Theorem soxp 7810
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 5460 . . 3 (𝑅 Or 𝐴𝑅 Po 𝐴)
2 sopo 5460 . . 3 (𝑆 Or 𝐵𝑆 Po 𝐵)
3 soxp.1 . . . 4 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))}
43poxp 7809 . . 3 ((𝑅 Po 𝐴𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵))
51, 2, 4syl2an 598 . 2 ((𝑅 Or 𝐴𝑆 Or 𝐵) → 𝑇 Po (𝐴 × 𝐵))
6 elxp 5546 . . . . 5 (𝑡 ∈ (𝐴 × 𝐵) ↔ ∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)))
7 elxp 5546 . . . . 5 (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)))
8 ioran 981 . . . . . . . . . . . . . . . . . . . . 21 (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) ↔ (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ ¬ (𝑎 = 𝑐𝑏 = 𝑑)))
9 ioran 981 . . . . . . . . . . . . . . . . . . . . . . 23 (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ ¬ (𝑎 = 𝑐𝑏𝑆𝑑)))
10 ianor 979 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ (𝑎 = 𝑐𝑏𝑆𝑑) ↔ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑))
1110anbi2i 625 . . . . . . . . . . . . . . . . . . . . . . 23 ((¬ 𝑎𝑅𝑐 ∧ ¬ (𝑎 = 𝑐𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)))
129, 11bitri 278 . . . . . . . . . . . . . . . . . . . . . 22 (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)))
13 ianor 979 . . . . . . . . . . . . . . . . . . . . . 22 (¬ (𝑎 = 𝑐𝑏 = 𝑑) ↔ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑))
1412, 13anbi12i 629 . . . . . . . . . . . . . . . . . . . . 21 ((¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ ¬ (𝑎 = 𝑐𝑏 = 𝑑)) ↔ ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)))
158, 14bitri 278 . . . . . . . . . . . . . . . . . . . 20 (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) ↔ ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)))
16 solin 5466 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) → (𝑎𝑅𝑐𝑎 = 𝑐𝑐𝑅𝑎))
17 3orass 1087 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎𝑅𝑐𝑎 = 𝑐𝑐𝑅𝑎) ↔ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑐𝑅𝑎)))
18 df-or 845 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑐𝑅𝑎)) ↔ (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐𝑐𝑅𝑎)))
1917, 18bitri 278 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝑅𝑐𝑎 = 𝑐𝑐𝑅𝑎) ↔ (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐𝑐𝑅𝑎)))
2016, 19sylib 221 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) → (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐𝑐𝑅𝑎)))
21 solin 5466 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵)) → (𝑏𝑆𝑑𝑏 = 𝑑𝑑𝑆𝑏))
22 3orass 1087 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑏𝑆𝑑𝑏 = 𝑑𝑑𝑆𝑏) ↔ (𝑏𝑆𝑑 ∨ (𝑏 = 𝑑𝑑𝑆𝑏)))
23 df-or 845 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑏𝑆𝑑 ∨ (𝑏 = 𝑑𝑑𝑆𝑏)) ↔ (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑𝑑𝑆𝑏)))
2422, 23bitri 278 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏𝑆𝑑𝑏 = 𝑑𝑑𝑆𝑏) ↔ (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑𝑑𝑆𝑏)))
2521, 24sylib 221 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵)) → (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑𝑑𝑆𝑏)))
2625orim2d 964 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵)) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑) → (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏))))
2720, 26im2anan9 622 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) → ((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏)))))
28 pm2.53 848 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 = 𝑐𝑐𝑅𝑎) → (¬ 𝑎 = 𝑐𝑐𝑅𝑎))
29 orc 864 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐𝑅𝑎 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))
3028, 29syl6 35 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎 = 𝑐𝑐𝑅𝑎) → (¬ 𝑎 = 𝑐 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
3130adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏))) → (¬ 𝑎 = 𝑐 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
32 orel1 886 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑏 = 𝑑 → ((𝑏 = 𝑑𝑑𝑆𝑏) → 𝑑𝑆𝑏))
3332orim2d 964 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑏 = 𝑑 → ((¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏)) → (¬ 𝑎 = 𝑐𝑑𝑆𝑏)))
3433anim2d 614 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑏 = 𝑑 → (((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏))) → ((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐𝑑𝑆𝑏))))
35 imor 850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎 = 𝑐𝑑𝑆𝑏) ↔ (¬ 𝑎 = 𝑐𝑑𝑆𝑏))
3635biimpri 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((¬ 𝑎 = 𝑐𝑑𝑆𝑏) → (𝑎 = 𝑐𝑑𝑆𝑏))
3736com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑐 → ((¬ 𝑎 = 𝑐𝑑𝑆𝑏) → 𝑑𝑆𝑏))
38 equcomi 2024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 = 𝑐𝑐 = 𝑎)
3938anim1i 617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎 = 𝑐𝑑𝑆𝑏) → (𝑐 = 𝑎𝑑𝑆𝑏))
4039olcd 871 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 = 𝑐𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))
4140ex 416 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑐 → (𝑑𝑆𝑏 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4237, 41syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑐 → ((¬ 𝑎 = 𝑐𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4329a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐𝑅𝑎 → ((¬ 𝑎 = 𝑐𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4442, 43jaoi 854 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 = 𝑐𝑐𝑅𝑎) → ((¬ 𝑎 = 𝑐𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4544imp 410 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐𝑑𝑆𝑏)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))
4634, 45syl6com 37 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏))) → (¬ 𝑏 = 𝑑 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4731, 46jaod 856 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏))) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4827, 47syl6 35 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
4948impd 414 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → (((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
5015, 49syl5bi 245 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
51 df-3or 1085 . . . . . . . . . . . . . . . . . . . 20 (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))) ↔ (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
52 df-or 845 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))) ↔ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
5351, 52bitri 278 . . . . . . . . . . . . . . . . . . 19 (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))) ↔ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
5450, 53sylibr 237 . . . . . . . . . . . . . . . . . 18 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
55 pm3.2 473 . . . . . . . . . . . . . . . . . . . 20 (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) → (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)))))
5655ad2ant2l 745 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) → (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)))))
57 idd 24 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((𝑎 = 𝑐𝑏 = 𝑑) → (𝑎 = 𝑐𝑏 = 𝑑)))
58 simpr 488 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) → (𝑎𝐴𝑐𝐴))
5958ancomd 465 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) → (𝑐𝐴𝑎𝐴))
60 simpr 488 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵)) → (𝑏𝐵𝑑𝐵))
6160ancomd 465 . . . . . . . . . . . . . . . . . . . 20 ((𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵)) → (𝑑𝐵𝑏𝐵))
62 pm3.2 473 . . . . . . . . . . . . . . . . . . . 20 (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) → ((𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)) → (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
6359, 61, 62syl2an 598 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)) → (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
6456, 57, 633orim123d 1441 . . . . . . . . . . . . . . . . . 18 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))) → ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))))
6554, 64mpd 15 . . . . . . . . . . . . . . . . 17 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
6665an4s 659 . . . . . . . . . . . . . . . 16 (((𝑅 Or 𝐴𝑆 Or 𝐵) ∧ ((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵))) → ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
6766expcom 417 . . . . . . . . . . . . . . 15 (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))))
6867an4s 659 . . . . . . . . . . . . . 14 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))))
69 breq12 5038 . . . . . . . . . . . . . . . . 17 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩))
70 eqeq12 2815 . . . . . . . . . . . . . . . . 17 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡 = 𝑢 ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
71 breq12 5038 . . . . . . . . . . . . . . . . . 18 ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑡 = ⟨𝑎, 𝑏⟩) → (𝑢𝑇𝑡 ↔ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩))
7271ancoms 462 . . . . . . . . . . . . . . . . 17 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑢𝑇𝑡 ↔ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩))
7369, 70, 723orbi123d 1432 . . . . . . . . . . . . . . . 16 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → ((𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡) ↔ (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∨ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ∨ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩)))
743xporderlem 7808 . . . . . . . . . . . . . . . . 17 (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ↔ (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))))
75 vex 3447 . . . . . . . . . . . . . . . . . 18 𝑎 ∈ V
76 vex 3447 . . . . . . . . . . . . . . . . . 18 𝑏 ∈ V
7775, 76opth 5336 . . . . . . . . . . . . . . . . 17 (⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ↔ (𝑎 = 𝑐𝑏 = 𝑑))
783xporderlem 7808 . . . . . . . . . . . . . . . . 17 (⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩ ↔ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
7974, 77, 783orbi123i 1153 . . . . . . . . . . . . . . . 16 ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∨ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ∨ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩) ↔ ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
8073, 79syl6bb 290 . . . . . . . . . . . . . . 15 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → ((𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡) ↔ ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))))
8180biimprcd 253 . . . . . . . . . . . . . 14 (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
8268, 81syl6 35 . . . . . . . . . . . . 13 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
8382com3r 87 . . . . . . . . . . . 12 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
8483imp 410 . . . . . . . . . . 11 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵))) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
8584an4s 659 . . . . . . . . . 10 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵))) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
8685expcom 417 . . . . . . . . 9 ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
8786exlimivv 1933 . . . . . . . 8 (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
8887com12 32 . . . . . . 7 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
8988exlimivv 1933 . . . . . 6 (∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
9089imp 410 . . . . 5 ((∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ ∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵))) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
916, 7, 90syl2anb 600 . . . 4 ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
9291com12 32 . . 3 ((𝑅 Or 𝐴𝑆 Or 𝐵) → ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
9392ralrimivv 3158 . 2 ((𝑅 Or 𝐴𝑆 Or 𝐵) → ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)(𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))
94 df-so 5443 . 2 (𝑇 Or (𝐴 × 𝐵) ↔ (𝑇 Po (𝐴 × 𝐵) ∧ ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)(𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
955, 93, 94sylanbrc 586 1 ((𝑅 Or 𝐴𝑆 Or 𝐵) → 𝑇 Or (𝐴 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  w3o 1083   = wceq 1538  wex 1781  wcel 2112  wral 3109  cop 4534   class class class wbr 5033  {copab 5095   Po wpo 5440   Or wor 5441   × cxp 5521  cfv 6328  1st c1st 7673  2nd c2nd 7674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-po 5442  df-so 5443  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-iota 6287  df-fun 6330  df-fv 6336  df-1st 7675  df-2nd 7676
This theorem is referenced by:  wexp  7811  rrx2plordso  45125
  Copyright terms: Public domain W3C validator