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

Theorem wemapsolem 9493
Description: Lemma for wemapso 9494. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 21-Jul-2024.)
Hypotheses
Ref Expression
wemapso.t 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐴 ((𝑥𝑧)𝑆(𝑦𝑧) ∧ ∀𝑤𝐴 (𝑤𝑅𝑧 → (𝑥𝑤) = (𝑦𝑤)))}
wemapsolem.1 𝑈 ⊆ (𝐵m 𝐴)
wemapsolem.2 (𝜑𝑅 Or 𝐴)
wemapsolem.3 (𝜑𝑆 Or 𝐵)
wemapsolem.4 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ∃𝑐 ∈ 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 (𝜑𝑅 Or 𝐴)
3 wemapsolem.3 . . . . 5 (𝜑𝑆 Or 𝐵)
4 sopo 5569 . . . . 5 (𝑆 Or 𝐵𝑆 Po 𝐵)
53, 4syl 17 . . . 4 (𝜑𝑆 Po 𝐵)
6 wemapso.t . . . . 5 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐴 ((𝑥𝑧)𝑆(𝑦𝑧) ∧ ∀𝑤𝐴 (𝑤𝑅𝑧 → (𝑥𝑤) = (𝑦𝑤)))}
76wemappo 9492 . . . 4 ((𝑅 Or 𝐴𝑆 Po 𝐵) → 𝑇 Po (𝐵m 𝐴))
82, 5, 7syl2anc 585 . . 3 (𝜑𝑇 Po (𝐵m 𝐴))
9 poss 5552 . . 3 (𝑈 ⊆ (𝐵m 𝐴) → (𝑇 Po (𝐵m 𝐴) → 𝑇 Po 𝑈))
101, 8, 9mpsyl 68 . 2 (𝜑𝑇 Po 𝑈)
11 df-ne 2945 . . . . 5 (𝑎𝑏 ↔ ¬ 𝑎 = 𝑏)
12 wemapsolem.4 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ∃𝑐 ∈ dom (𝑎𝑏)∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐)
13 simprll 778 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑎𝑈)
141, 13sselid 3947 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑎 ∈ (𝐵m 𝐴))
15 elmapi 8794 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ (𝐵m 𝐴) → 𝑎:𝐴𝐵)
1614, 15syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑎:𝐴𝐵)
1716ffnd 6674 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑎 Fn 𝐴)
18 simprlr 779 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑏𝑈)
191, 18sselid 3947 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑏 ∈ (𝐵m 𝐴))
20 elmapi 8794 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝐵m 𝐴) → 𝑏:𝐴𝐵)
2119, 20syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑏:𝐴𝐵)
2221ffnd 6674 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑏 Fn 𝐴)
23 fndmdif 6997 . . . . . . . . . . . . . . 15 ((𝑎 Fn 𝐴𝑏 Fn 𝐴) → dom (𝑎𝑏) = {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)})
2417, 22, 23syl2anc 585 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → dom (𝑎𝑏) = {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)})
2524eleq2d 2824 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑐 ∈ dom (𝑎𝑏) ↔ 𝑐 ∈ {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)}))
26 nesym 3001 . . . . . . . . . . . . . . 15 ((𝑎𝑥) ≠ (𝑏𝑥) ↔ ¬ (𝑏𝑥) = (𝑎𝑥))
27 fveq2 6847 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑐 → (𝑏𝑥) = (𝑏𝑐))
28 fveq2 6847 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑐 → (𝑎𝑥) = (𝑎𝑐))
2927, 28eqeq12d 2753 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑐 → ((𝑏𝑥) = (𝑎𝑥) ↔ (𝑏𝑐) = (𝑎𝑐)))
3029notbid 318 . . . . . . . . . . . . . . 15 (𝑥 = 𝑐 → (¬ (𝑏𝑥) = (𝑎𝑥) ↔ ¬ (𝑏𝑐) = (𝑎𝑐)))
3126, 30bitrid 283 . . . . . . . . . . . . . 14 (𝑥 = 𝑐 → ((𝑎𝑥) ≠ (𝑏𝑥) ↔ ¬ (𝑏𝑐) = (𝑎𝑐)))
3231elrab 3650 . . . . . . . . . . . . 13 (𝑐 ∈ {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)} ↔ (𝑐𝐴 ∧ ¬ (𝑏𝑐) = (𝑎𝑐)))
3325, 32bitrdi 287 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑐 ∈ dom (𝑎𝑏) ↔ (𝑐𝐴 ∧ ¬ (𝑏𝑐) = (𝑎𝑐))))
3424eleq2d 2824 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑑 ∈ dom (𝑎𝑏) ↔ 𝑑 ∈ {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)}))
35 fveq2 6847 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑑 → (𝑏𝑥) = (𝑏𝑑))
36 fveq2 6847 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑑 → (𝑎𝑥) = (𝑎𝑑))
3735, 36eqeq12d 2753 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑑 → ((𝑏𝑥) = (𝑎𝑥) ↔ (𝑏𝑑) = (𝑎𝑑)))
3837notbid 318 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑑 → (¬ (𝑏𝑥) = (𝑎𝑥) ↔ ¬ (𝑏𝑑) = (𝑎𝑑)))
3926, 38bitrid 283 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑑 → ((𝑎𝑥) ≠ (𝑏𝑥) ↔ ¬ (𝑏𝑑) = (𝑎𝑑)))
4039elrab 3650 . . . . . . . . . . . . . . . 16 (𝑑 ∈ {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)} ↔ (𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑)))
4134, 40bitrdi 287 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑑 ∈ dom (𝑎𝑏) ↔ (𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑))))
4241imbi1d 342 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ((𝑑 ∈ dom (𝑎𝑏) → ¬ 𝑑𝑅𝑐) ↔ ((𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑)) → ¬ 𝑑𝑅𝑐)))
43 impexp 452 . . . . . . . . . . . . . . 15 (((𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑)) → ¬ 𝑑𝑅𝑐) ↔ (𝑑𝐴 → (¬ (𝑏𝑑) = (𝑎𝑑) → ¬ 𝑑𝑅𝑐)))
44 con34b 316 . . . . . . . . . . . . . . . 16 ((𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)) ↔ (¬ (𝑏𝑑) = (𝑎𝑑) → ¬ 𝑑𝑅𝑐))
4544imbi2i 336 . . . . . . . . . . . . . . 15 ((𝑑𝐴 → (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ↔ (𝑑𝐴 → (¬ (𝑏𝑑) = (𝑎𝑑) → ¬ 𝑑𝑅𝑐)))
4643, 45bitr4i 278 . . . . . . . . . . . . . 14 (((𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑)) → ¬ 𝑑𝑅𝑐) ↔ (𝑑𝐴 → (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
4742, 46bitrdi 287 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ((𝑑 ∈ dom (𝑎𝑏) → ¬ 𝑑𝑅𝑐) ↔ (𝑑𝐴 → (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
4847ralbidv2 3171 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐 ↔ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
4933, 48anbi12d 632 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ((𝑐 ∈ dom (𝑎𝑏) ∧ ∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐) ↔ ((𝑐𝐴 ∧ ¬ (𝑏𝑐) = (𝑎𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
50 anass 470 . . . . . . . . . . 11 (((𝑐𝐴 ∧ ¬ (𝑏𝑐) = (𝑎𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ↔ (𝑐𝐴 ∧ (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
5149, 50bitrdi 287 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ((𝑐 ∈ dom (𝑎𝑏) ∧ ∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐) ↔ (𝑐𝐴 ∧ (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))))
5251rexbidv2 3172 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (∃𝑐 ∈ dom (𝑎𝑏)∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐 ↔ ∃𝑐𝐴 (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
5312, 52mpbid 231 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ∃𝑐𝐴 (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
543ad2antrr 725 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → 𝑆 Or 𝐵)
5521ffvelcdmda 7040 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → (𝑏𝑐) ∈ 𝐵)
5616ffvelcdmda 7040 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → (𝑎𝑐) ∈ 𝐵)
57 sotrieq 5579 . . . . . . . . . . . . 13 ((𝑆 Or 𝐵 ∧ ((𝑏𝑐) ∈ 𝐵 ∧ (𝑎𝑐) ∈ 𝐵)) → ((𝑏𝑐) = (𝑎𝑐) ↔ ¬ ((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐))))
5857con2bid 355 . . . . . . . . . . . 12 ((𝑆 Or 𝐵 ∧ ((𝑏𝑐) ∈ 𝐵 ∧ (𝑎𝑐) ∈ 𝐵)) → (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ↔ ¬ (𝑏𝑐) = (𝑎𝑐)))
5958biimprd 248 . . . . . . . . . . 11 ((𝑆 Or 𝐵 ∧ ((𝑏𝑐) ∈ 𝐵 ∧ (𝑎𝑐) ∈ 𝐵)) → (¬ (𝑏𝑐) = (𝑎𝑐) → ((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐))))
6054, 55, 56, 59syl12anc 836 . . . . . . . . . 10 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → (¬ (𝑏𝑐) = (𝑎𝑐) → ((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐))))
6160anim1d 612 . . . . . . . . 9 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → ((¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) → (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
6261reximdva 3166 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (∃𝑐𝐴 (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) → ∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
6353, 62mpd 15 . . . . . . 7 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
646wemaplem1 9489 . . . . . . . . . 10 ((𝑏 ∈ V ∧ 𝑎 ∈ V) → (𝑏𝑇𝑎 ↔ ∃𝑐𝐴 ((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
6564el2v 3456 . . . . . . . . 9 (𝑏𝑇𝑎 ↔ ∃𝑐𝐴 ((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
666wemaplem1 9489 . . . . . . . . . 10 ((𝑎 ∈ V ∧ 𝑏 ∈ V) → (𝑎𝑇𝑏 ↔ ∃𝑐𝐴 ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))))
6766el2v 3456 . . . . . . . . 9 (𝑎𝑇𝑏 ↔ ∃𝑐𝐴 ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑))))
6865, 67orbi12i 914 . . . . . . . 8 ((𝑏𝑇𝑎𝑎𝑇𝑏) ↔ (∃𝑐𝐴 ((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ∃𝑐𝐴 ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))))
69 r19.43 3126 . . . . . . . 8 (∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))) ↔ (∃𝑐𝐴 ((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ∃𝑐𝐴 ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))))
70 andir 1008 . . . . . . . . . 10 ((((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ↔ (((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
71 eqcom 2744 . . . . . . . . . . . . . 14 ((𝑏𝑑) = (𝑎𝑑) ↔ (𝑎𝑑) = (𝑏𝑑))
7271imbi2i 336 . . . . . . . . . . . . 13 ((𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)) ↔ (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))
7372ralbii 3097 . . . . . . . . . . . 12 (∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)) ↔ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))
7473anbi2i 624 . . . . . . . . . . 11 (((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ↔ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑))))
7574orbi2i 912 . . . . . . . . . 10 ((((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))) ↔ (((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))))
7670, 75bitr2i 276 . . . . . . . . 9 ((((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))) ↔ (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
7776rexbii 3098 . . . . . . . 8 (∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))) ↔ ∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
7868, 69, 773bitr2i 299 . . . . . . 7 ((𝑏𝑇𝑎𝑎𝑇𝑏) ↔ ∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
7963, 78sylibr 233 . . . . . 6 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑏𝑇𝑎𝑎𝑇𝑏))
8079expr 458 . . . . 5 ((𝜑 ∧ (𝑎𝑈𝑏𝑈)) → (𝑎𝑏 → (𝑏𝑇𝑎𝑎𝑇𝑏)))
8111, 80biimtrrid 242 . . . 4 ((𝜑 ∧ (𝑎𝑈𝑏𝑈)) → (¬ 𝑎 = 𝑏 → (𝑏𝑇𝑎𝑎𝑇𝑏)))
8281orrd 862 . . 3 ((𝜑 ∧ (𝑎𝑈𝑏𝑈)) → (𝑎 = 𝑏 ∨ (𝑏𝑇𝑎𝑎𝑇𝑏)))
83 3orrot 1093 . . . 4 ((𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎) ↔ (𝑎 = 𝑏𝑏𝑇𝑎𝑎𝑇𝑏))
84 3orass 1091 . . . 4 ((𝑎 = 𝑏𝑏𝑇𝑎𝑎𝑇𝑏) ↔ (𝑎 = 𝑏 ∨ (𝑏𝑇𝑎𝑎𝑇𝑏)))
8583, 84bitr2i 276 . . 3 ((𝑎 = 𝑏 ∨ (𝑏𝑇𝑎𝑎𝑇𝑏)) ↔ (𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎))
8682, 85sylib 217 . 2 ((𝜑 ∧ (𝑎𝑈𝑏𝑈)) → (𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎))
8710, 86issod 5583 1 (𝜑𝑇 Or 𝑈)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 846  w3o 1087   = wceq 1542  wcel 2107  wne 2944  wral 3065  wrex 3074  {crab 3410  Vcvv 3448  cdif 3912  wss 3915   class class class wbr 5110  {copab 5172   Po wpo 5548   Or wor 5549  dom cdm 5638   Fn wfn 6496  wf 6497  cfv 6501  (class class class)co 7362  m cmap 8772
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-po 5550  df-so 5551  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-1st 7926  df-2nd 7927  df-map 8774
This theorem is referenced by:  wemapso  9494  wemapso2lem  9495
  Copyright terms: Public domain W3C validator