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

Theorem soxp 7235
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 5012 . . 3 (𝑅 Or 𝐴𝑅 Po 𝐴)
2 sopo 5012 . . 3 (𝑆 Or 𝐵𝑆 Po 𝐵)
3 soxp.1 . . . 4 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))}
43poxp 7234 . . 3 ((𝑅 Po 𝐴𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵))
51, 2, 4syl2an 494 . 2 ((𝑅 Or 𝐴𝑆 Or 𝐵) → 𝑇 Po (𝐴 × 𝐵))
6 elxp 5091 . . . . 5 (𝑡 ∈ (𝐴 × 𝐵) ↔ ∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)))
7 elxp 5091 . . . . 5 (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)))
8 ioran 511 . . . . . . . . . . . . . . . . . . . . 21 (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) ↔ (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ ¬ (𝑎 = 𝑐𝑏 = 𝑑)))
9 ioran 511 . . . . . . . . . . . . . . . . . . . . . . 23 (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ ¬ (𝑎 = 𝑐𝑏𝑆𝑑)))
10 ianor 509 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ (𝑎 = 𝑐𝑏𝑆𝑑) ↔ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑))
1110anbi2i 729 . . . . . . . . . . . . . . . . . . . . . . 23 ((¬ 𝑎𝑅𝑐 ∧ ¬ (𝑎 = 𝑐𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)))
129, 11bitri 264 . . . . . . . . . . . . . . . . . . . . . 22 (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)))
13 ianor 509 . . . . . . . . . . . . . . . . . . . . . 22 (¬ (𝑎 = 𝑐𝑏 = 𝑑) ↔ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑))
1412, 13anbi12i 732 . . . . . . . . . . . . . . . . . . . . 21 ((¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∧ ¬ (𝑎 = 𝑐𝑏 = 𝑑)) ↔ ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)))
158, 14bitri 264 . . . . . . . . . . . . . . . . . . . 20 (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) ↔ ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)))
16 solin 5018 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) → (𝑎𝑅𝑐𝑎 = 𝑐𝑐𝑅𝑎))
17 3orass 1039 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎𝑅𝑐𝑎 = 𝑐𝑐𝑅𝑎) ↔ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑐𝑅𝑎)))
18 df-or 385 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑐𝑅𝑎)) ↔ (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐𝑐𝑅𝑎)))
1917, 18bitri 264 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝑅𝑐𝑎 = 𝑐𝑐𝑅𝑎) ↔ (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐𝑐𝑅𝑎)))
2016, 19sylib 208 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) → (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐𝑐𝑅𝑎)))
21 solin 5018 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵)) → (𝑏𝑆𝑑𝑏 = 𝑑𝑑𝑆𝑏))
22 3orass 1039 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑏𝑆𝑑𝑏 = 𝑑𝑑𝑆𝑏) ↔ (𝑏𝑆𝑑 ∨ (𝑏 = 𝑑𝑑𝑆𝑏)))
23 df-or 385 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑏𝑆𝑑 ∨ (𝑏 = 𝑑𝑑𝑆𝑏)) ↔ (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑𝑑𝑆𝑏)))
2422, 23bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏𝑆𝑑𝑏 = 𝑑𝑑𝑆𝑏) ↔ (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑𝑑𝑆𝑏)))
2521, 24sylib 208 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵)) → (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑𝑑𝑆𝑏)))
2625orim2d 884 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵)) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑) → (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏))))
2720, 26im2anan9 879 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) → ((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏)))))
28 pm2.53 388 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 = 𝑐𝑐𝑅𝑎) → (¬ 𝑎 = 𝑐𝑐𝑅𝑎))
29 orc 400 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐𝑅𝑎 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))
3028, 29syl6 35 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎 = 𝑐𝑐𝑅𝑎) → (¬ 𝑎 = 𝑐 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
3130adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏))) → (¬ 𝑎 = 𝑐 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
32 orel1 397 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑏 = 𝑑 → ((𝑏 = 𝑑𝑑𝑆𝑏) → 𝑑𝑆𝑏))
3332orim2d 884 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑏 = 𝑑 → ((¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏)) → (¬ 𝑎 = 𝑐𝑑𝑆𝑏)))
3433anim2d 588 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑏 = 𝑑 → (((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏))) → ((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐𝑑𝑆𝑏))))
35 imor 428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎 = 𝑐𝑑𝑆𝑏) ↔ (¬ 𝑎 = 𝑐𝑑𝑆𝑏))
3635biimpri 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((¬ 𝑎 = 𝑐𝑑𝑆𝑏) → (𝑎 = 𝑐𝑑𝑆𝑏))
3736com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑐 → ((¬ 𝑎 = 𝑐𝑑𝑆𝑏) → 𝑑𝑆𝑏))
38 equcomi 1941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 = 𝑐𝑐 = 𝑎)
3938anim1i 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎 = 𝑐𝑑𝑆𝑏) → (𝑐 = 𝑎𝑑𝑆𝑏))
4039olcd 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 = 𝑐𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))
4140ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑐 → (𝑑𝑆𝑏 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4237, 41syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑐 → ((¬ 𝑎 = 𝑐𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4329a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐𝑅𝑎 → ((¬ 𝑎 = 𝑐𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4442, 43jaoi 394 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 = 𝑐𝑐𝑅𝑎) → ((¬ 𝑎 = 𝑐𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4544imp 445 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐𝑑𝑆𝑏)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))
4634, 45syl6com 37 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏))) → (¬ 𝑏 = 𝑑 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4731, 46jaod 395 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎 = 𝑐𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑𝑑𝑆𝑏))) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
4827, 47syl6 35 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
4948impd 447 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → (((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
5015, 49syl5bi 232 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
51 df-3or 1037 . . . . . . . . . . . . . . . . . . . 20 (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))) ↔ (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
52 df-or 385 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))) ↔ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
5351, 52bitri 264 . . . . . . . . . . . . . . . . . . 19 (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))) ↔ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
5450, 53sylibr 224 . . . . . . . . . . . . . . . . . 18 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
55 pm3.2 463 . . . . . . . . . . . . . . . . . . . 20 (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) → (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)))))
5655ad2ant2l 781 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) → (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)))))
57 idd 24 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((𝑎 = 𝑐𝑏 = 𝑑) → (𝑎 = 𝑐𝑏 = 𝑑)))
58 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) → (𝑎𝐴𝑐𝐴))
5958ancomd 467 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) → (𝑐𝐴𝑎𝐴))
60 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵)) → (𝑏𝐵𝑑𝐵))
6160ancomd 467 . . . . . . . . . . . . . . . . . . . 20 ((𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵)) → (𝑑𝐵𝑏𝐵))
62 pm3.2 463 . . . . . . . . . . . . . . . . . . . 20 (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) → ((𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)) → (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
6359, 61, 62syl2an 494 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)) → (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
6456, 57, 633orim123d 1404 . . . . . . . . . . . . . . . . . 18 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))) → ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))))
6554, 64mpd 15 . . . . . . . . . . . . . . . . 17 (((𝑅 Or 𝐴 ∧ (𝑎𝐴𝑐𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏𝐵𝑑𝐵))) → ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
6665an4s 868 . . . . . . . . . . . . . . . 16 (((𝑅 Or 𝐴𝑆 Or 𝐵) ∧ ((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵))) → ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
6766expcom 451 . . . . . . . . . . . . . . 15 (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))))
6867an4s 868 . . . . . . . . . . . . . 14 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))))
69 breq12 4618 . . . . . . . . . . . . . . . . 17 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩))
70 eqeq12 2634 . . . . . . . . . . . . . . . . 17 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡 = 𝑢 ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
71 breq12 4618 . . . . . . . . . . . . . . . . . 18 ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑡 = ⟨𝑎, 𝑏⟩) → (𝑢𝑇𝑡 ↔ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩))
7271ancoms 469 . . . . . . . . . . . . . . . . 17 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑢𝑇𝑡 ↔ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩))
7369, 70, 723orbi123d 1395 . . . . . . . . . . . . . . . 16 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → ((𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡) ↔ (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∨ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ∨ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩)))
743xporderlem 7233 . . . . . . . . . . . . . . . . 17 (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ↔ (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))))
75 vex 3189 . . . . . . . . . . . . . . . . . 18 𝑎 ∈ V
76 vex 3189 . . . . . . . . . . . . . . . . . 18 𝑏 ∈ V
7775, 76opth 4905 . . . . . . . . . . . . . . . . 17 (⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ↔ (𝑎 = 𝑐𝑏 = 𝑑))
783xporderlem 7233 . . . . . . . . . . . . . . . . 17 (⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩ ↔ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))
7974, 77, 783orbi123i 1250 . . . . . . . . . . . . . . . 16 ((⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ∨ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ∨ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩) ↔ ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))))
8073, 79syl6bb 276 . . . . . . . . . . . . . . 15 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → ((𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡) ↔ ((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏))))))
8180biimprcd 240 . . . . . . . . . . . . . 14 (((((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐𝑏 = 𝑑) ∨ (((𝑐𝐴𝑎𝐴) ∧ (𝑑𝐵𝑏𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎𝑑𝑆𝑏)))) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
8268, 81syl6 35 . . . . . . . . . . . . 13 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
8382com3r 87 . . . . . . . . . . . 12 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
8483imp 445 . . . . . . . . . . 11 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) ∧ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵))) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
8584an4s 868 . . . . . . . . . 10 (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵))) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
8685expcom 451 . . . . . . . . 9 ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
8786exlimivv 1857 . . . . . . . 8 (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
8887com12 32 . . . . . . 7 ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
8988exlimivv 1857 . . . . . 6 (∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) → (∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))))
9089imp 445 . . . . 5 ((∃𝑎𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝐴𝑏𝐵)) ∧ ∃𝑐𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐𝐴𝑑𝐵))) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
916, 7, 90syl2anb 496 . . . 4 ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → ((𝑅 Or 𝐴𝑆 Or 𝐵) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
9291com12 32 . . 3 ((𝑅 Or 𝐴𝑆 Or 𝐵) → ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
9392ralrimivv 2964 . 2 ((𝑅 Or 𝐴𝑆 Or 𝐵) → ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)(𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡))
94 df-so 4996 . 2 (𝑇 Or (𝐴 × 𝐵) ↔ (𝑇 Po (𝐴 × 𝐵) ∧ ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)(𝑡𝑇𝑢𝑡 = 𝑢𝑢𝑇𝑡)))
955, 93, 94sylanbrc 697 1 ((𝑅 Or 𝐴𝑆 Or 𝐵) → 𝑇 Or (𝐴 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3o 1035   = wceq 1480  wex 1701  wcel 1987  wral 2907  cop 4154   class class class wbr 4613  {copab 4672   Po wpo 4993   Or wor 4994   × cxp 5072  cfv 5847  1st c1st 7111  2nd c2nd 7112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-po 4995  df-so 4996  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-iota 5810  df-fun 5849  df-fv 5855  df-1st 7113  df-2nd 7114
This theorem is referenced by:  wexp  7236
  Copyright terms: Public domain W3C validator