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

Theorem wemapsolem 8611
Description: Lemma for wemapso 8612. (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 5187 . . . . 5 (𝑆 Or 𝐵𝑆 Po 𝐵)
64, 5syl 17 . . . 4 (𝜑𝑆 Po 𝐵)
7 wemapso.t . . . . 5 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐴 ((𝑥𝑧)𝑆(𝑦𝑧) ∧ ∀𝑤𝐴 (𝑤𝑅𝑧 → (𝑥𝑤) = (𝑦𝑤)))}
87wemappo 8610 . . . 4 ((𝐴 ∈ V ∧ 𝑅 Or 𝐴𝑆 Po 𝐵) → 𝑇 Po (𝐵𝑚 𝐴))
92, 3, 6, 8syl3anc 1476 . . 3 (𝜑𝑇 Po (𝐵𝑚 𝐴))
10 poss 5172 . . 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 8031 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ (𝐵𝑚 𝐴) → 𝑎:𝐴𝐵)
1715, 16syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑎:𝐴𝐵)
18 ffn 6185 . . . . . . . . . . . . . . . 16 (𝑎:𝐴𝐵𝑎 Fn 𝐴)
1917, 18syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑎 Fn 𝐴)
20 simprlr 765 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑏𝑈)
211, 20sseldi 3750 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑏 ∈ (𝐵𝑚 𝐴))
22 elmapi 8031 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝐵𝑚 𝐴) → 𝑏:𝐴𝐵)
2321, 22syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑏:𝐴𝐵)
24 ffn 6185 . . . . . . . . . . . . . . . 16 (𝑏:𝐴𝐵𝑏 Fn 𝐴)
2523, 24syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑏 Fn 𝐴)
26 fndmdif 6464 . . . . . . . . . . . . . . 15 ((𝑎 Fn 𝐴𝑏 Fn 𝐴) → dom (𝑎𝑏) = {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)})
2719, 25, 26syl2anc 573 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → dom (𝑎𝑏) = {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)})
2827eleq2d 2836 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑐 ∈ dom (𝑎𝑏) ↔ 𝑐 ∈ {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)}))
29 nesym 2999 . . . . . . . . . . . . . . 15 ((𝑎𝑥) ≠ (𝑏𝑥) ↔ ¬ (𝑏𝑥) = (𝑎𝑥))
30 fveq2 6332 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑐 → (𝑏𝑥) = (𝑏𝑐))
31 fveq2 6332 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑐 → (𝑎𝑥) = (𝑎𝑐))
3230, 31eqeq12d 2786 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑐 → ((𝑏𝑥) = (𝑎𝑥) ↔ (𝑏𝑐) = (𝑎𝑐)))
3332notbid 307 . . . . . . . . . . . . . . 15 (𝑥 = 𝑐 → (¬ (𝑏𝑥) = (𝑎𝑥) ↔ ¬ (𝑏𝑐) = (𝑎𝑐)))
3429, 33syl5bb 272 . . . . . . . . . . . . . 14 (𝑥 = 𝑐 → ((𝑎𝑥) ≠ (𝑏𝑥) ↔ ¬ (𝑏𝑐) = (𝑎𝑐)))
3534elrab 3515 . . . . . . . . . . . . 13 (𝑐 ∈ {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)} ↔ (𝑐𝐴 ∧ ¬ (𝑏𝑐) = (𝑎𝑐)))
3628, 35syl6bb 276 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑐 ∈ dom (𝑎𝑏) ↔ (𝑐𝐴 ∧ ¬ (𝑏𝑐) = (𝑎𝑐))))
3727eleq2d 2836 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑑 ∈ dom (𝑎𝑏) ↔ 𝑑 ∈ {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)}))
38 fveq2 6332 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑑 → (𝑏𝑥) = (𝑏𝑑))
39 fveq2 6332 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑑 → (𝑎𝑥) = (𝑎𝑑))
4038, 39eqeq12d 2786 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑑 → ((𝑏𝑥) = (𝑎𝑥) ↔ (𝑏𝑑) = (𝑎𝑑)))
4140notbid 307 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑑 → (¬ (𝑏𝑥) = (𝑎𝑥) ↔ ¬ (𝑏𝑑) = (𝑎𝑑)))
4229, 41syl5bb 272 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑑 → ((𝑎𝑥) ≠ (𝑏𝑥) ↔ ¬ (𝑏𝑑) = (𝑎𝑑)))
4342elrab 3515 . . . . . . . . . . . . . . . 16 (𝑑 ∈ {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)} ↔ (𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑)))
4437, 43syl6bb 276 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑑 ∈ dom (𝑎𝑏) ↔ (𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑))))
4544imbi1d 330 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ((𝑑 ∈ dom (𝑎𝑏) → ¬ 𝑑𝑅𝑐) ↔ ((𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑)) → ¬ 𝑑𝑅𝑐)))
46 impexp 437 . . . . . . . . . . . . . . 15 (((𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑)) → ¬ 𝑑𝑅𝑐) ↔ (𝑑𝐴 → (¬ (𝑏𝑑) = (𝑎𝑑) → ¬ 𝑑𝑅𝑐)))
47 con34b 305 . . . . . . . . . . . . . . . 16 ((𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)) ↔ (¬ (𝑏𝑑) = (𝑎𝑑) → ¬ 𝑑𝑅𝑐))
4847imbi2i 325 . . . . . . . . . . . . . . 15 ((𝑑𝐴 → (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ↔ (𝑑𝐴 → (¬ (𝑏𝑑) = (𝑎𝑑) → ¬ 𝑑𝑅𝑐)))
4946, 48bitr4i 267 . . . . . . . . . . . . . 14 (((𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑)) → ¬ 𝑑𝑅𝑐) ↔ (𝑑𝐴 → (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
5045, 49syl6bb 276 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ((𝑑 ∈ dom (𝑎𝑏) → ¬ 𝑑𝑅𝑐) ↔ (𝑑𝐴 → (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
5150ralbidv2 3133 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐 ↔ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
5236, 51anbi12d 616 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ((𝑐 ∈ dom (𝑎𝑏) ∧ ∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐) ↔ ((𝑐𝐴 ∧ ¬ (𝑏𝑐) = (𝑎𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
53 anass 459 . . . . . . . . . . 11 (((𝑐𝐴 ∧ ¬ (𝑏𝑐) = (𝑎𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ↔ (𝑐𝐴 ∧ (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
5452, 53syl6bb 276 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ((𝑐 ∈ dom (𝑎𝑏) ∧ ∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐) ↔ (𝑐𝐴 ∧ (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))))
5554rexbidv2 3196 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (∃𝑐 ∈ dom (𝑎𝑏)∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐 ↔ ∃𝑐𝐴 (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
5613, 55mpbid 222 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ∃𝑐𝐴 (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
574ad2antrr 705 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → 𝑆 Or 𝐵)
5823ffvelrnda 6502 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → (𝑏𝑐) ∈ 𝐵)
5917ffvelrnda 6502 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → (𝑎𝑐) ∈ 𝐵)
60 sotrieq 5197 . . . . . . . . . . . . 13 ((𝑆 Or 𝐵 ∧ ((𝑏𝑐) ∈ 𝐵 ∧ (𝑎𝑐) ∈ 𝐵)) → ((𝑏𝑐) = (𝑎𝑐) ↔ ¬ ((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐))))
6160con2bid 343 . . . . . . . . . . . 12 ((𝑆 Or 𝐵 ∧ ((𝑏𝑐) ∈ 𝐵 ∧ (𝑎𝑐) ∈ 𝐵)) → (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ↔ ¬ (𝑏𝑐) = (𝑎𝑐)))
6261biimprd 238 . . . . . . . . . . 11 ((𝑆 Or 𝐵 ∧ ((𝑏𝑐) ∈ 𝐵 ∧ (𝑎𝑐) ∈ 𝐵)) → (¬ (𝑏𝑐) = (𝑎𝑐) → ((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐))))
6357, 58, 59, 62syl12anc 1474 . . . . . . . . . 10 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → (¬ (𝑏𝑐) = (𝑎𝑐) → ((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐))))
6463anim1d 598 . . . . . . . . 9 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → ((¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) → (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
6564reximdva 3165 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (∃𝑐𝐴 (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) → ∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
6656, 65mpd 15 . . . . . . 7 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
67 vex 3354 . . . . . . . . . 10 𝑏 ∈ V
68 vex 3354 . . . . . . . . . 10 𝑎 ∈ V
697wemaplem1 8607 . . . . . . . . . 10 ((𝑏 ∈ V ∧ 𝑎 ∈ V) → (𝑏𝑇𝑎 ↔ ∃𝑐𝐴 ((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
7067, 68, 69mp2an 672 . . . . . . . . 9 (𝑏𝑇𝑎 ↔ ∃𝑐𝐴 ((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
717wemaplem1 8607 . . . . . . . . . 10 ((𝑎 ∈ V ∧ 𝑏 ∈ V) → (𝑎𝑇𝑏 ↔ ∃𝑐𝐴 ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))))
7268, 67, 71mp2an 672 . . . . . . . . 9 (𝑎𝑇𝑏 ↔ ∃𝑐𝐴 ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑))))
7370, 72orbi12i 900 . . . . . . . 8 ((𝑏𝑇𝑎𝑎𝑇𝑏) ↔ (∃𝑐𝐴 ((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ∃𝑐𝐴 ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))))
74 r19.43 3241 . . . . . . . 8 (∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))) ↔ (∃𝑐𝐴 ((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ∃𝑐𝐴 ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))))
75 andir 993 . . . . . . . . . 10 ((((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ↔ (((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
76 eqcom 2778 . . . . . . . . . . . . . 14 ((𝑏𝑑) = (𝑎𝑑) ↔ (𝑎𝑑) = (𝑏𝑑))
7776imbi2i 325 . . . . . . . . . . . . 13 ((𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)) ↔ (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))
7877ralbii 3129 . . . . . . . . . . . 12 (∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)) ↔ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))
7978anbi2i 609 . . . . . . . . . . 11 (((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ↔ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑))))
8079orbi2i 898 . . . . . . . . . 10 ((((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))) ↔ (((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))))
8175, 80bitr2i 265 . . . . . . . . 9 ((((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))) ↔ (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
8281rexbii 3189 . . . . . . . 8 (∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))) ↔ ∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
8373, 74, 823bitr2i 288 . . . . . . 7 ((𝑏𝑇𝑎𝑎𝑇𝑏) ↔ ∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
8466, 83sylibr 224 . . . . . 6 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑏𝑇𝑎𝑎𝑇𝑏))
8584expr 444 . . . . 5 ((𝜑 ∧ (𝑎𝑈𝑏𝑈)) → (𝑎𝑏 → (𝑏𝑇𝑎𝑎𝑇𝑏)))
8612, 85syl5bir 233 . . . 4 ((𝜑 ∧ (𝑎𝑈𝑏𝑈)) → (¬ 𝑎 = 𝑏 → (𝑏𝑇𝑎𝑎𝑇𝑏)))
8786orrd 852 . . 3 ((𝜑 ∧ (𝑎𝑈𝑏𝑈)) → (𝑎 = 𝑏 ∨ (𝑏𝑇𝑎𝑎𝑇𝑏)))
88 3orrot 1076 . . . 4 ((𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎) ↔ (𝑎 = 𝑏𝑏𝑇𝑎𝑎𝑇𝑏))
89 3orass 1074 . . . 4 ((𝑎 = 𝑏𝑏𝑇𝑎𝑎𝑇𝑏) ↔ (𝑎 = 𝑏 ∨ (𝑏𝑇𝑎𝑎𝑇𝑏)))
9088, 89bitr2i 265 . . 3 ((𝑎 = 𝑏 ∨ (𝑏𝑇𝑎𝑎𝑇𝑏)) ↔ (𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎))
9187, 90sylib 208 . 2 ((𝜑 ∧ (𝑎𝑈𝑏𝑈)) → (𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎))
9211, 91issod 5200 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 4786  {copab 4846   Po wpo 5168   Or wor 5169  dom cdm 5249   Fn wfn 6026  wf 6027  cfv 6031  (class class class)co 6793  𝑚 cmap 8009
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 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
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 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-po 5170  df-so 5171  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-fv 6039  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-1st 7315  df-2nd 7316  df-map 8011
This theorem is referenced by:  wemapso  8612  wemapso2lem  8613
  Copyright terms: Public domain W3C validator