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

Theorem wemapsolem 9017
Description: Lemma for wemapso 9018. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Mario Carneiro, 8-Feb-2015.)
Hypotheses
Ref Expression
wemapso.t 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐴 ((𝑥𝑧)𝑆(𝑦𝑧) ∧ ∀𝑤𝐴 (𝑤𝑅𝑧 → (𝑥𝑤) = (𝑦𝑤)))}
wemapsolem.1 𝑈 ⊆ (𝐵m 𝐴)
wemapsolem.2 (𝜑𝐴 ∈ V)
wemapsolem.3 (𝜑𝑅 Or 𝐴)
wemapsolem.4 (𝜑𝑆 Or 𝐵)
wemapsolem.5 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ∃𝑐 ∈ dom (𝑎𝑏)∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐)
Assertion
Ref Expression
wemapsolem (𝜑𝑇 Or 𝑈)
Distinct variable groups:   𝑎,𝑏,𝑐,𝑑,𝑥,𝐵   𝑇,𝑎,𝑏,𝑐,𝑑   𝑈,𝑎,𝑏,𝑐,𝑑   𝑤,𝑎,𝑦,𝑧,𝑏,𝑐,𝑥,𝐴,𝑑   𝑅,𝑎,𝑏,𝑐,𝑑,𝑤,𝑥,𝑦,𝑧   𝑆,𝑎,𝑏,𝑐,𝑑,𝑤,𝑥,𝑦,𝑧   𝜑,𝑎,𝑏,𝑐,𝑑
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤)   𝐵(𝑦,𝑧,𝑤)   𝑇(𝑥,𝑦,𝑧,𝑤)   𝑈(𝑥,𝑦,𝑧,𝑤)

Proof of Theorem wemapsolem
StepHypRef Expression
1 wemapsolem.1 . . 3 𝑈 ⊆ (𝐵m 𝐴)
2 wemapsolem.2 . . . 4 (𝜑𝐴 ∈ V)
3 wemapsolem.3 . . . 4 (𝜑𝑅 Or 𝐴)
4 wemapsolem.4 . . . . 5 (𝜑𝑆 Or 𝐵)
5 sopo 5495 . . . . 5 (𝑆 Or 𝐵𝑆 Po 𝐵)
64, 5syl 17 . . . 4 (𝜑𝑆 Po 𝐵)
7 wemapso.t . . . . 5 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐴 ((𝑥𝑧)𝑆(𝑦𝑧) ∧ ∀𝑤𝐴 (𝑤𝑅𝑧 → (𝑥𝑤) = (𝑦𝑤)))}
87wemappo 9016 . . . 4 ((𝐴 ∈ V ∧ 𝑅 Or 𝐴𝑆 Po 𝐵) → 𝑇 Po (𝐵m 𝐴))
92, 3, 6, 8syl3anc 1367 . . 3 (𝜑𝑇 Po (𝐵m 𝐴))
10 poss 5479 . . 3 (𝑈 ⊆ (𝐵m 𝐴) → (𝑇 Po (𝐵m 𝐴) → 𝑇 Po 𝑈))
111, 9, 10mpsyl 68 . 2 (𝜑𝑇 Po 𝑈)
12 df-ne 3020 . . . . 5 (𝑎𝑏 ↔ ¬ 𝑎 = 𝑏)
13 wemapsolem.5 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ∃𝑐 ∈ dom (𝑎𝑏)∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐)
14 simprll 777 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑎𝑈)
151, 14sseldi 3968 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑎 ∈ (𝐵m 𝐴))
16 elmapi 8431 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ (𝐵m 𝐴) → 𝑎:𝐴𝐵)
1715, 16syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑎:𝐴𝐵)
1817ffnd 6518 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑎 Fn 𝐴)
19 simprlr 778 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑏𝑈)
201, 19sseldi 3968 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑏 ∈ (𝐵m 𝐴))
21 elmapi 8431 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝐵m 𝐴) → 𝑏:𝐴𝐵)
2220, 21syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑏:𝐴𝐵)
2322ffnd 6518 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑏 Fn 𝐴)
24 fndmdif 6815 . . . . . . . . . . . . . . 15 ((𝑎 Fn 𝐴𝑏 Fn 𝐴) → dom (𝑎𝑏) = {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)})
2518, 23, 24syl2anc 586 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → dom (𝑎𝑏) = {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)})
2625eleq2d 2901 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑐 ∈ dom (𝑎𝑏) ↔ 𝑐 ∈ {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)}))
27 nesym 3075 . . . . . . . . . . . . . . 15 ((𝑎𝑥) ≠ (𝑏𝑥) ↔ ¬ (𝑏𝑥) = (𝑎𝑥))
28 fveq2 6673 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑐 → (𝑏𝑥) = (𝑏𝑐))
29 fveq2 6673 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑐 → (𝑎𝑥) = (𝑎𝑐))
3028, 29eqeq12d 2840 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑐 → ((𝑏𝑥) = (𝑎𝑥) ↔ (𝑏𝑐) = (𝑎𝑐)))
3130notbid 320 . . . . . . . . . . . . . . 15 (𝑥 = 𝑐 → (¬ (𝑏𝑥) = (𝑎𝑥) ↔ ¬ (𝑏𝑐) = (𝑎𝑐)))
3227, 31syl5bb 285 . . . . . . . . . . . . . 14 (𝑥 = 𝑐 → ((𝑎𝑥) ≠ (𝑏𝑥) ↔ ¬ (𝑏𝑐) = (𝑎𝑐)))
3332elrab 3683 . . . . . . . . . . . . 13 (𝑐 ∈ {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)} ↔ (𝑐𝐴 ∧ ¬ (𝑏𝑐) = (𝑎𝑐)))
3426, 33syl6bb 289 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑐 ∈ dom (𝑎𝑏) ↔ (𝑐𝐴 ∧ ¬ (𝑏𝑐) = (𝑎𝑐))))
3525eleq2d 2901 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑑 ∈ dom (𝑎𝑏) ↔ 𝑑 ∈ {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)}))
36 fveq2 6673 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑑 → (𝑏𝑥) = (𝑏𝑑))
37 fveq2 6673 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑑 → (𝑎𝑥) = (𝑎𝑑))
3836, 37eqeq12d 2840 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑑 → ((𝑏𝑥) = (𝑎𝑥) ↔ (𝑏𝑑) = (𝑎𝑑)))
3938notbid 320 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑑 → (¬ (𝑏𝑥) = (𝑎𝑥) ↔ ¬ (𝑏𝑑) = (𝑎𝑑)))
4027, 39syl5bb 285 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑑 → ((𝑎𝑥) ≠ (𝑏𝑥) ↔ ¬ (𝑏𝑑) = (𝑎𝑑)))
4140elrab 3683 . . . . . . . . . . . . . . . 16 (𝑑 ∈ {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)} ↔ (𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑)))
4235, 41syl6bb 289 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑑 ∈ dom (𝑎𝑏) ↔ (𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑))))
4342imbi1d 344 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ((𝑑 ∈ dom (𝑎𝑏) → ¬ 𝑑𝑅𝑐) ↔ ((𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑)) → ¬ 𝑑𝑅𝑐)))
44 impexp 453 . . . . . . . . . . . . . . 15 (((𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑)) → ¬ 𝑑𝑅𝑐) ↔ (𝑑𝐴 → (¬ (𝑏𝑑) = (𝑎𝑑) → ¬ 𝑑𝑅𝑐)))
45 con34b 318 . . . . . . . . . . . . . . . 16 ((𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)) ↔ (¬ (𝑏𝑑) = (𝑎𝑑) → ¬ 𝑑𝑅𝑐))
4645imbi2i 338 . . . . . . . . . . . . . . 15 ((𝑑𝐴 → (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ↔ (𝑑𝐴 → (¬ (𝑏𝑑) = (𝑎𝑑) → ¬ 𝑑𝑅𝑐)))
4744, 46bitr4i 280 . . . . . . . . . . . . . 14 (((𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑)) → ¬ 𝑑𝑅𝑐) ↔ (𝑑𝐴 → (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
4843, 47syl6bb 289 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ((𝑑 ∈ dom (𝑎𝑏) → ¬ 𝑑𝑅𝑐) ↔ (𝑑𝐴 → (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
4948ralbidv2 3198 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐 ↔ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
5034, 49anbi12d 632 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ((𝑐 ∈ dom (𝑎𝑏) ∧ ∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐) ↔ ((𝑐𝐴 ∧ ¬ (𝑏𝑐) = (𝑎𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
51 anass 471 . . . . . . . . . . 11 (((𝑐𝐴 ∧ ¬ (𝑏𝑐) = (𝑎𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ↔ (𝑐𝐴 ∧ (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
5250, 51syl6bb 289 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ((𝑐 ∈ dom (𝑎𝑏) ∧ ∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐) ↔ (𝑐𝐴 ∧ (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))))
5352rexbidv2 3298 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (∃𝑐 ∈ dom (𝑎𝑏)∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐 ↔ ∃𝑐𝐴 (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
5413, 53mpbid 234 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ∃𝑐𝐴 (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
554ad2antrr 724 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → 𝑆 Or 𝐵)
5622ffvelrnda 6854 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → (𝑏𝑐) ∈ 𝐵)
5717ffvelrnda 6854 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → (𝑎𝑐) ∈ 𝐵)
58 sotrieq 5505 . . . . . . . . . . . . 13 ((𝑆 Or 𝐵 ∧ ((𝑏𝑐) ∈ 𝐵 ∧ (𝑎𝑐) ∈ 𝐵)) → ((𝑏𝑐) = (𝑎𝑐) ↔ ¬ ((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐))))
5958con2bid 357 . . . . . . . . . . . 12 ((𝑆 Or 𝐵 ∧ ((𝑏𝑐) ∈ 𝐵 ∧ (𝑎𝑐) ∈ 𝐵)) → (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ↔ ¬ (𝑏𝑐) = (𝑎𝑐)))
6059biimprd 250 . . . . . . . . . . 11 ((𝑆 Or 𝐵 ∧ ((𝑏𝑐) ∈ 𝐵 ∧ (𝑎𝑐) ∈ 𝐵)) → (¬ (𝑏𝑐) = (𝑎𝑐) → ((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐))))
6155, 56, 57, 60syl12anc 834 . . . . . . . . . 10 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → (¬ (𝑏𝑐) = (𝑎𝑐) → ((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐))))
6261anim1d 612 . . . . . . . . 9 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → ((¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) → (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
6362reximdva 3277 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (∃𝑐𝐴 (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) → ∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
6454, 63mpd 15 . . . . . . 7 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
657wemaplem1 9013 . . . . . . . . . 10 ((𝑏 ∈ V ∧ 𝑎 ∈ V) → (𝑏𝑇𝑎 ↔ ∃𝑐𝐴 ((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
6665el2v 3504 . . . . . . . . 9 (𝑏𝑇𝑎 ↔ ∃𝑐𝐴 ((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
677wemaplem1 9013 . . . . . . . . . 10 ((𝑎 ∈ V ∧ 𝑏 ∈ V) → (𝑎𝑇𝑏 ↔ ∃𝑐𝐴 ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))))
6867el2v 3504 . . . . . . . . 9 (𝑎𝑇𝑏 ↔ ∃𝑐𝐴 ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑))))
6966, 68orbi12i 911 . . . . . . . 8 ((𝑏𝑇𝑎𝑎𝑇𝑏) ↔ (∃𝑐𝐴 ((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ∃𝑐𝐴 ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))))
70 r19.43 3354 . . . . . . . 8 (∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))) ↔ (∃𝑐𝐴 ((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ∃𝑐𝐴 ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))))
71 andir 1005 . . . . . . . . . 10 ((((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ↔ (((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
72 eqcom 2831 . . . . . . . . . . . . . 14 ((𝑏𝑑) = (𝑎𝑑) ↔ (𝑎𝑑) = (𝑏𝑑))
7372imbi2i 338 . . . . . . . . . . . . 13 ((𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)) ↔ (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))
7473ralbii 3168 . . . . . . . . . . . 12 (∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)) ↔ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))
7574anbi2i 624 . . . . . . . . . . 11 (((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ↔ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑))))
7675orbi2i 909 . . . . . . . . . 10 ((((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))) ↔ (((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))))
7771, 76bitr2i 278 . . . . . . . . 9 ((((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))) ↔ (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
7877rexbii 3250 . . . . . . . 8 (∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))) ↔ ∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
7969, 70, 783bitr2i 301 . . . . . . 7 ((𝑏𝑇𝑎𝑎𝑇𝑏) ↔ ∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
8064, 79sylibr 236 . . . . . 6 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑏𝑇𝑎𝑎𝑇𝑏))
8180expr 459 . . . . 5 ((𝜑 ∧ (𝑎𝑈𝑏𝑈)) → (𝑎𝑏 → (𝑏𝑇𝑎𝑎𝑇𝑏)))
8212, 81syl5bir 245 . . . 4 ((𝜑 ∧ (𝑎𝑈𝑏𝑈)) → (¬ 𝑎 = 𝑏 → (𝑏𝑇𝑎𝑎𝑇𝑏)))
8382orrd 859 . . 3 ((𝜑 ∧ (𝑎𝑈𝑏𝑈)) → (𝑎 = 𝑏 ∨ (𝑏𝑇𝑎𝑎𝑇𝑏)))
84 3orrot 1088 . . . 4 ((𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎) ↔ (𝑎 = 𝑏𝑏𝑇𝑎𝑎𝑇𝑏))
85 3orass 1086 . . . 4 ((𝑎 = 𝑏𝑏𝑇𝑎𝑎𝑇𝑏) ↔ (𝑎 = 𝑏 ∨ (𝑏𝑇𝑎𝑎𝑇𝑏)))
8684, 85bitr2i 278 . . 3 ((𝑎 = 𝑏 ∨ (𝑏𝑇𝑎𝑎𝑇𝑏)) ↔ (𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎))
8783, 86sylib 220 . 2 ((𝜑 ∧ (𝑎𝑈𝑏𝑈)) → (𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎))
8811, 87issod 5509 1 (𝜑𝑇 Or 𝑈)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wo 843  w3o 1082   = wceq 1536  wcel 2113  wne 3019  wral 3141  wrex 3142  {crab 3145  Vcvv 3497  cdif 3936  wss 3939   class class class wbr 5069  {copab 5131   Po wpo 5475   Or wor 5476  dom cdm 5558   Fn wfn 6353  wf 6354  cfv 6358  (class class class)co 7159  m cmap 8409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-iun 4924  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-po 5477  df-so 5478  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-fv 6366  df-ov 7162  df-oprab 7163  df-mpo 7164  df-1st 7692  df-2nd 7693  df-map 8411
This theorem is referenced by:  wemapso  9018  wemapso2lem  9019
  Copyright terms: Public domain W3C validator