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

Theorem wemapsolem 8615
Description: Lemma for wemapso 8616. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Mario Carneiro, 8-Feb-2015.)
Hypotheses
Ref Expression
wemapso.t 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐴 ((𝑥𝑧)𝑆(𝑦𝑧) ∧ ∀𝑤𝐴 (𝑤𝑅𝑧 → (𝑥𝑤) = (𝑦𝑤)))}
wemapsolem.1 𝑈 ⊆ (𝐵𝑚 𝐴)
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 𝑈 ⊆ (𝐵𝑚 𝐴)
2 wemapsolem.2 . . . 4 (𝜑𝐴 ∈ V)
3 wemapsolem.3 . . . 4 (𝜑𝑅 Or 𝐴)
4 wemapsolem.4 . . . . 5 (𝜑𝑆 Or 𝐵)
5 sopo 5188 . . . . 5 (𝑆 Or 𝐵𝑆 Po 𝐵)
64, 5syl 17 . . . 4 (𝜑𝑆 Po 𝐵)
7 wemapso.t . . . . 5 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐴 ((𝑥𝑧)𝑆(𝑦𝑧) ∧ ∀𝑤𝐴 (𝑤𝑅𝑧 → (𝑥𝑤) = (𝑦𝑤)))}
87wemappo 8614 . . . 4 ((𝐴 ∈ V ∧ 𝑅 Or 𝐴𝑆 Po 𝐵) → 𝑇 Po (𝐵𝑚 𝐴))
92, 3, 6, 8syl3anc 1476 . . 3 (𝜑𝑇 Po (𝐵𝑚 𝐴))
10 poss 5173 . . 3 (𝑈 ⊆ (𝐵𝑚 𝐴) → (𝑇 Po (𝐵𝑚 𝐴) → 𝑇 Po 𝑈))
111, 9, 10mpsyl 68 . 2 (𝜑𝑇 Po 𝑈)
12 df-ne 2944 . . . . 5 (𝑎𝑏 ↔ ¬ 𝑎 = 𝑏)
13 wemapsolem.5 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ∃𝑐 ∈ dom (𝑎𝑏)∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐)
14 simprll 764 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑎𝑈)
151, 14sseldi 3750 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑎 ∈ (𝐵𝑚 𝐴))
16 elmapi 8035 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ (𝐵𝑚 𝐴) → 𝑎:𝐴𝐵)
1715, 16syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑎:𝐴𝐵)
1817ffnd 6185 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑎 Fn 𝐴)
19 simprlr 765 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑏𝑈)
201, 19sseldi 3750 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑏 ∈ (𝐵𝑚 𝐴))
21 elmapi 8035 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝐵𝑚 𝐴) → 𝑏:𝐴𝐵)
2220, 21syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑏:𝐴𝐵)
2322ffnd 6185 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑏 Fn 𝐴)
24 fndmdif 6466 . . . . . . . . . . . . . . 15 ((𝑎 Fn 𝐴𝑏 Fn 𝐴) → dom (𝑎𝑏) = {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)})
2518, 23, 24syl2anc 573 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → dom (𝑎𝑏) = {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)})
2625eleq2d 2836 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑐 ∈ dom (𝑎𝑏) ↔ 𝑐 ∈ {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)}))
27 nesym 2999 . . . . . . . . . . . . . . 15 ((𝑎𝑥) ≠ (𝑏𝑥) ↔ ¬ (𝑏𝑥) = (𝑎𝑥))
28 fveq2 6333 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑐 → (𝑏𝑥) = (𝑏𝑐))
29 fveq2 6333 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑐 → (𝑎𝑥) = (𝑎𝑐))
3028, 29eqeq12d 2786 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑐 → ((𝑏𝑥) = (𝑎𝑥) ↔ (𝑏𝑐) = (𝑎𝑐)))
3130notbid 307 . . . . . . . . . . . . . . 15 (𝑥 = 𝑐 → (¬ (𝑏𝑥) = (𝑎𝑥) ↔ ¬ (𝑏𝑐) = (𝑎𝑐)))
3227, 31syl5bb 272 . . . . . . . . . . . . . 14 (𝑥 = 𝑐 → ((𝑎𝑥) ≠ (𝑏𝑥) ↔ ¬ (𝑏𝑐) = (𝑎𝑐)))
3332elrab 3515 . . . . . . . . . . . . 13 (𝑐 ∈ {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)} ↔ (𝑐𝐴 ∧ ¬ (𝑏𝑐) = (𝑎𝑐)))
3426, 33syl6bb 276 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑐 ∈ dom (𝑎𝑏) ↔ (𝑐𝐴 ∧ ¬ (𝑏𝑐) = (𝑎𝑐))))
3525eleq2d 2836 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑑 ∈ dom (𝑎𝑏) ↔ 𝑑 ∈ {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)}))
36 fveq2 6333 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑑 → (𝑏𝑥) = (𝑏𝑑))
37 fveq2 6333 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑑 → (𝑎𝑥) = (𝑎𝑑))
3836, 37eqeq12d 2786 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑑 → ((𝑏𝑥) = (𝑎𝑥) ↔ (𝑏𝑑) = (𝑎𝑑)))
3938notbid 307 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑑 → (¬ (𝑏𝑥) = (𝑎𝑥) ↔ ¬ (𝑏𝑑) = (𝑎𝑑)))
4027, 39syl5bb 272 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑑 → ((𝑎𝑥) ≠ (𝑏𝑥) ↔ ¬ (𝑏𝑑) = (𝑎𝑑)))
4140elrab 3515 . . . . . . . . . . . . . . . 16 (𝑑 ∈ {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)} ↔ (𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑)))
4235, 41syl6bb 276 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑑 ∈ dom (𝑎𝑏) ↔ (𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑))))
4342imbi1d 330 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ((𝑑 ∈ dom (𝑎𝑏) → ¬ 𝑑𝑅𝑐) ↔ ((𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑)) → ¬ 𝑑𝑅𝑐)))
44 impexp 437 . . . . . . . . . . . . . . 15 (((𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑)) → ¬ 𝑑𝑅𝑐) ↔ (𝑑𝐴 → (¬ (𝑏𝑑) = (𝑎𝑑) → ¬ 𝑑𝑅𝑐)))
45 con34b 305 . . . . . . . . . . . . . . . 16 ((𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)) ↔ (¬ (𝑏𝑑) = (𝑎𝑑) → ¬ 𝑑𝑅𝑐))
4645imbi2i 325 . . . . . . . . . . . . . . 15 ((𝑑𝐴 → (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ↔ (𝑑𝐴 → (¬ (𝑏𝑑) = (𝑎𝑑) → ¬ 𝑑𝑅𝑐)))
4744, 46bitr4i 267 . . . . . . . . . . . . . 14 (((𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑)) → ¬ 𝑑𝑅𝑐) ↔ (𝑑𝐴 → (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
4843, 47syl6bb 276 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ((𝑑 ∈ dom (𝑎𝑏) → ¬ 𝑑𝑅𝑐) ↔ (𝑑𝐴 → (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
4948ralbidv2 3133 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐 ↔ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
5034, 49anbi12d 616 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ((𝑐 ∈ dom (𝑎𝑏) ∧ ∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐) ↔ ((𝑐𝐴 ∧ ¬ (𝑏𝑐) = (𝑎𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
51 anass 454 . . . . . . . . . . 11 (((𝑐𝐴 ∧ ¬ (𝑏𝑐) = (𝑎𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ↔ (𝑐𝐴 ∧ (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
5250, 51syl6bb 276 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ((𝑐 ∈ dom (𝑎𝑏) ∧ ∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐) ↔ (𝑐𝐴 ∧ (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))))
5352rexbidv2 3196 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (∃𝑐 ∈ dom (𝑎𝑏)∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐 ↔ ∃𝑐𝐴 (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
5413, 53mpbid 222 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ∃𝑐𝐴 (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
554ad2antrr 705 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → 𝑆 Or 𝐵)
5622ffvelrnda 6504 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → (𝑏𝑐) ∈ 𝐵)
5717ffvelrnda 6504 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → (𝑎𝑐) ∈ 𝐵)
58 sotrieq 5198 . . . . . . . . . . . . 13 ((𝑆 Or 𝐵 ∧ ((𝑏𝑐) ∈ 𝐵 ∧ (𝑎𝑐) ∈ 𝐵)) → ((𝑏𝑐) = (𝑎𝑐) ↔ ¬ ((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐))))
5958con2bid 343 . . . . . . . . . . . 12 ((𝑆 Or 𝐵 ∧ ((𝑏𝑐) ∈ 𝐵 ∧ (𝑎𝑐) ∈ 𝐵)) → (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ↔ ¬ (𝑏𝑐) = (𝑎𝑐)))
6059biimprd 238 . . . . . . . . . . 11 ((𝑆 Or 𝐵 ∧ ((𝑏𝑐) ∈ 𝐵 ∧ (𝑎𝑐) ∈ 𝐵)) → (¬ (𝑏𝑐) = (𝑎𝑐) → ((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐))))
6155, 56, 57, 60syl12anc 1474 . . . . . . . . . 10 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → (¬ (𝑏𝑐) = (𝑎𝑐) → ((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐))))
6261anim1d 598 . . . . . . . . 9 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → ((¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) → (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
6362reximdva 3165 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (∃𝑐𝐴 (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) → ∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
6454, 63mpd 15 . . . . . . 7 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
65 vex 3354 . . . . . . . . . 10 𝑏 ∈ V
66 vex 3354 . . . . . . . . . 10 𝑎 ∈ V
677wemaplem1 8611 . . . . . . . . . 10 ((𝑏 ∈ V ∧ 𝑎 ∈ V) → (𝑏𝑇𝑎 ↔ ∃𝑐𝐴 ((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
6865, 66, 67mp2an 672 . . . . . . . . 9 (𝑏𝑇𝑎 ↔ ∃𝑐𝐴 ((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
697wemaplem1 8611 . . . . . . . . . 10 ((𝑎 ∈ V ∧ 𝑏 ∈ V) → (𝑎𝑇𝑏 ↔ ∃𝑐𝐴 ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))))
7066, 65, 69mp2an 672 . . . . . . . . 9 (𝑎𝑇𝑏 ↔ ∃𝑐𝐴 ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑))))
7168, 70orbi12i 900 . . . . . . . 8 ((𝑏𝑇𝑎𝑎𝑇𝑏) ↔ (∃𝑐𝐴 ((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ∃𝑐𝐴 ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))))
72 r19.43 3241 . . . . . . . 8 (∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))) ↔ (∃𝑐𝐴 ((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ∃𝑐𝐴 ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))))
73 andir 993 . . . . . . . . . 10 ((((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ↔ (((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
74 eqcom 2778 . . . . . . . . . . . . . 14 ((𝑏𝑑) = (𝑎𝑑) ↔ (𝑎𝑑) = (𝑏𝑑))
7574imbi2i 325 . . . . . . . . . . . . 13 ((𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)) ↔ (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))
7675ralbii 3129 . . . . . . . . . . . 12 (∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)) ↔ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))
7776anbi2i 609 . . . . . . . . . . 11 (((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ↔ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑))))
7877orbi2i 898 . . . . . . . . . 10 ((((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))) ↔ (((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))))
7973, 78bitr2i 265 . . . . . . . . 9 ((((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))) ↔ (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
8079rexbii 3189 . . . . . . . 8 (∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))) ↔ ∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
8171, 72, 803bitr2i 288 . . . . . . 7 ((𝑏𝑇𝑎𝑎𝑇𝑏) ↔ ∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
8264, 81sylibr 224 . . . . . 6 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑏𝑇𝑎𝑎𝑇𝑏))
8382expr 444 . . . . 5 ((𝜑 ∧ (𝑎𝑈𝑏𝑈)) → (𝑎𝑏 → (𝑏𝑇𝑎𝑎𝑇𝑏)))
8412, 83syl5bir 233 . . . 4 ((𝜑 ∧ (𝑎𝑈𝑏𝑈)) → (¬ 𝑎 = 𝑏 → (𝑏𝑇𝑎𝑎𝑇𝑏)))
8584orrd 852 . . 3 ((𝜑 ∧ (𝑎𝑈𝑏𝑈)) → (𝑎 = 𝑏 ∨ (𝑏𝑇𝑎𝑎𝑇𝑏)))
86 3orrot 1076 . . . 4 ((𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎) ↔ (𝑎 = 𝑏𝑏𝑇𝑎𝑎𝑇𝑏))
87 3orass 1074 . . . 4 ((𝑎 = 𝑏𝑏𝑇𝑎𝑎𝑇𝑏) ↔ (𝑎 = 𝑏 ∨ (𝑏𝑇𝑎𝑎𝑇𝑏)))
8886, 87bitr2i 265 . . 3 ((𝑎 = 𝑏 ∨ (𝑏𝑇𝑎𝑎𝑇𝑏)) ↔ (𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎))
8985, 88sylib 208 . 2 ((𝜑 ∧ (𝑎𝑈𝑏𝑈)) → (𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎))
9011, 89issod 5201 1 (𝜑𝑇 Or 𝑈)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wo 836  w3o 1070   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  {crab 3065  Vcvv 3351  cdif 3720  wss 3723   class class class wbr 4787  {copab 4847   Po wpo 5169   Or wor 5170  dom cdm 5250   Fn wfn 6025  wf 6026  cfv 6030  (class class class)co 6796  𝑚 cmap 8013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7100
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-id 5158  df-po 5171  df-so 5172  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-fv 6038  df-ov 6799  df-oprab 6800  df-mpt2 6801  df-1st 7319  df-2nd 7320  df-map 8015
This theorem is referenced by:  wemapso  8616  wemapso2lem  8617
  Copyright terms: Public domain W3C validator