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

Theorem soxp 7177
 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 4976 . . 3 (𝑅 Or 𝐴𝑅 Po 𝐴)
2 sopo 4976 . . 3 (𝑆 Or 𝐵𝑆 Po 𝐵)
3 soxp.1 . . . 4 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))}
43poxp 7176 . . 3 ((𝑅 Po 𝐴𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵))
51, 2, 4syl2an 493 . 2 ((𝑅 Or 𝐴𝑆 Or 𝐵) → 𝑇 Po (𝐴 × 𝐵))
6 elxp 5055 . . . . 5 (𝑡 ∈ (𝐴 × 𝐵) ↔ ∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)))
7 elxp 5055 . . . . 5 (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)))
8 ioran 510 . . . . . . . . . . . . . . . . . . . . 21 (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) ↔ (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ ¬ (𝑎 = 𝑐𝑏 = 𝑑)))
9 ioran 510 . . . . . . . . . . . . . . . . . . . . . . 23 (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ ¬ (𝑎 = 𝑐𝑏𝑆𝑑)))
10 ianor 508 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ (𝑎 = 𝑐𝑏𝑆𝑑) ↔ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑))
1110anbi2i 726 . . . . . . . . . . . . . . . . . . . . . . 23 ((¬ 𝑎𝑅𝑐 ∧ ¬ (𝑎 = 𝑐𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)))
129, 11bitri 263 . . . . . . . . . . . . . . . . . . . . . 22 (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)))
13 ianor 508 . . . . . . . . . . . . . . . . . . . . . 22 (¬ (𝑎 = 𝑐𝑏 = 𝑑) ↔ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑))
1412, 13anbi12i 729 . . . . . . . . . . . . . . . . . . . . 21 ((¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ ¬ (𝑎 = 𝑐𝑏 = 𝑑)) ↔ ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)))
158, 14bitri 263 . . . . . . . . . . . . . . . . . . . 20 (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) ↔ ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)))
16 solin 4982 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) → (𝑎𝑅𝑐𝑎 = 𝑐𝑐𝑅𝑎))
17 3orass 1034 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎𝑅𝑐𝑎 = 𝑐𝑐𝑅𝑎) ↔ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑐𝑅𝑎)))
18 df-or 384 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑐𝑅𝑎)) ↔ (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐𝑐𝑅𝑎)))
1917, 18bitri 263 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝑅𝑐𝑎 = 𝑐𝑐𝑅𝑎) ↔ (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐𝑐𝑅𝑎)))
2016, 19sylib 207 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) → (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐𝑐𝑅𝑎)))
21 solin 4982 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵)) → (𝑏𝑆𝑑𝑏 = 𝑑𝑑𝑆𝑏))
22 3orass 1034 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑏𝑆𝑑𝑏 = 𝑑𝑑𝑆𝑏) ↔ (𝑏𝑆𝑑 ∨ (𝑏 = 𝑑𝑑𝑆𝑏)))
23 df-or 384 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑏𝑆𝑑 ∨ (𝑏 = 𝑑𝑑𝑆𝑏)) ↔ (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑𝑑𝑆𝑏)))
2422, 23bitri 263 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏𝑆𝑑𝑏 = 𝑑𝑑𝑆𝑏) ↔ (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑𝑑𝑆𝑏)))
2521, 24sylib 207 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵)) → (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑𝑑𝑆𝑏)))
2625orim2d 881 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵)) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑) → (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏))))
2720, 26im2anan9 876 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) → ((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏)))))
28 pm2.53 387 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 = 𝑐𝑐𝑅𝑎) → (¬ 𝑎 = 𝑐𝑐𝑅𝑎))
29 orc 399 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐𝑅𝑎 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))
3028, 29syl6 34 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎 = 𝑐𝑐𝑅𝑎) → (¬ 𝑎 = 𝑐 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
3130adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏))) → (¬ 𝑎 = 𝑐 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
32 orel1 396 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑏 = 𝑑 → ((𝑏 = 𝑑𝑑𝑆𝑏) → 𝑑𝑆𝑏))
3332orim2d 881 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑏 = 𝑑 → ((¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏)) → (¬ 𝑎 = 𝑐𝑑𝑆𝑏)))
3433anim2d 587 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑏 = 𝑑 → (((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏))) → ((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐𝑑𝑆𝑏))))
35 imor 427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎 = 𝑐𝑑𝑆𝑏) ↔ (¬ 𝑎 = 𝑐𝑑𝑆𝑏))
3635biimpri 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((¬ 𝑎 = 𝑐𝑑𝑆𝑏) → (𝑎 = 𝑐𝑑𝑆𝑏))
3736com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑐 → ((¬ 𝑎 = 𝑐𝑑𝑆𝑏) → 𝑑𝑆𝑏))
38 equcomi 1931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 = 𝑐𝑐 = 𝑎)
3938anim1i 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎 = 𝑐𝑑𝑆𝑏) → (𝑐 = 𝑎𝑑𝑆𝑏))
4039olcd 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 = 𝑐𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))
4140ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑐 → (𝑑𝑆𝑏 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4237, 41syld 46 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑐 → ((¬ 𝑎 = 𝑐𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4329a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐𝑅𝑎 → ((¬ 𝑎 = 𝑐𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4442, 43jaoi 393 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 = 𝑐𝑐𝑅𝑎) → ((¬ 𝑎 = 𝑐𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4544imp 444 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐𝑑𝑆𝑏)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))
4634, 45syl6com 36 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏))) → (¬ 𝑏 = 𝑑 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4731, 46jaod 394 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏))) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4827, 47syl6 34 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
4948impd 446 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → (((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
5015, 49syl5bi 231 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
51 df-3or 1032 . . . . . . . . . . . . . . . . . . . 20 (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))) ↔ (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
52 df-or 384 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))) ↔ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
5351, 52bitri 263 . . . . . . . . . . . . . . . . . . 19 (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))) ↔ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
5450, 53sylibr 223 . . . . . . . . . . . . . . . . . 18 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
55 pm3.2 462 . . . . . . . . . . . . . . . . . . . 20 (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) → (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)))))
5655ad2ant2l 778 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) → (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)))))
57 idd 24 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((𝑎 = 𝑐𝑏 = 𝑑) → (𝑎 = 𝑐𝑏 = 𝑑)))
58 simpr 476 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) → (𝑎𝐴𝑐𝐴))
5958ancomd 466 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) → (𝑐𝐴𝑎𝐴))
60 simpr 476 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵)) → (𝑏𝐵𝑑𝐵))
6160ancomd 466 . . . . . . . . . . . . . . . . . . . 20 ((𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵)) → (𝑑𝐵𝑏𝐵))
62 pm3.2 462 . . . . . . . . . . . . . . . . . . . 20 (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) → ((𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)) → (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
6359, 61, 62syl2an 493 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)) → (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
6456, 57, 633orim123d 1399 . . . . . . . . . . . . . . . . . 18 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))) → ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))))
6554, 64mpd 15 . . . . . . . . . . . . . . . . 17 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
6665an4s 865 . . . . . . . . . . . . . . . 16 (((𝑅 Or 𝐴𝑆 Or 𝐵) ∧ ((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵))) → ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
6766expcom 450 . . . . . . . . . . . . . . 15 (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))))
6867an4s 865 . . . . . . . . . . . . . 14 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))))
69 breq12 4588 . . . . . . . . . . . . . . . . 17 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩))
70 eqeq12 2623 . . . . . . . . . . . . . . . . 17 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡 = 𝑢 ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
71 breq12 4588 . . . . . . . . . . . . . . . . . 18 ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑡 = ⟨𝑎, 𝑏⟩) → (𝑢𝑇𝑡 ↔ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩))
7271ancoms 468 . . . . . . . . . . . . . . . . 17 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑢𝑇𝑡 ↔ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩))
7369, 70, 723orbi123d 1390 . . . . . . . . . . . . . . . 16 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → ((𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡) ↔ (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∨ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ∨ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩)))
743xporderlem 7175 . . . . . . . . . . . . . . . . 17 (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ↔ (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))))
75 vex 3176 . . . . . . . . . . . . . . . . . 18 𝑎 ∈ V
76 vex 3176 . . . . . . . . . . . . . . . . . 18 𝑏 ∈ V
7775, 76opth 4871 . . . . . . . . . . . . . . . . 17 (⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ↔ (𝑎 = 𝑐𝑏 = 𝑑))
783xporderlem 7175 . . . . . . . . . . . . . . . . 17 (⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩ ↔ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
7974, 77, 783orbi123i 1245 . . . . . . . . . . . . . . . 16 ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∨ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ∨ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩) ↔ ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
8073, 79syl6bb 275 . . . . . . . . . . . . . . 15 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → ((𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡) ↔ ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))))
8180biimprcd 239 . . . . . . . . . . . . . 14 (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
8268, 81syl6 34 . . . . . . . . . . . . 13 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
8382com3r 85 . . . . . . . . . . . 12 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
8483imp 444 . . . . . . . . . . 11 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵))) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
8584an4s 865 . . . . . . . . . 10 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵))) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
8685expcom 450 . . . . . . . . 9 ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
8786exlimivv 1847 . . . . . . . 8 (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
8887com12 32 . . . . . . 7 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
8988exlimivv 1847 . . . . . 6 (∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
9089imp 444 . . . . 5 ((∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ ∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵))) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
916, 7, 90syl2anb 495 . . . 4 ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
9291com12 32 . . 3 ((𝑅 Or 𝐴𝑆 Or 𝐵) → ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
9392ralrimivv 2953 . 2 ((𝑅 Or 𝐴𝑆 Or 𝐵) → ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)(𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))
94 df-so 4960 . 2 (𝑇 Or (𝐴 × 𝐵) ↔ (𝑇 Po (𝐴 × 𝐵) ∧ ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)(𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
955, 93, 94sylanbrc 695 1 ((𝑅 Or 𝐴𝑆 Or 𝐵) → 𝑇 Or (𝐴 × 𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∨ w3o 1030   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∀wral 2896  ⟨cop 4131   class class class wbr 4583  {copab 4642   Po wpo 4957   Or wor 4958   × cxp 5036  ‘cfv 5804  1st c1st 7057  2nd c2nd 7058 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-iota 5768  df-fun 5806  df-fv 5812  df-1st 7059  df-2nd 7060 This theorem is referenced by:  wexp  7178
 Copyright terms: Public domain W3C validator