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

Theorem wemapsolem 9190
Description: Lemma for wemapso 9191. (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 5501 . . . . 5 (𝑆 Or 𝐵𝑆 Po 𝐵)
53, 4syl 17 . . . 4 (𝜑𝑆 Po 𝐵)
6 wemapso.t . . . . 5 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐴 ((𝑥𝑧)𝑆(𝑦𝑧) ∧ ∀𝑤𝐴 (𝑤𝑅𝑧 → (𝑥𝑤) = (𝑦𝑤)))}
76wemappo 9189 . . . 4 ((𝑅 Or 𝐴𝑆 Po 𝐵) → 𝑇 Po (𝐵m 𝐴))
82, 5, 7syl2anc 587 . . 3 (𝜑𝑇 Po (𝐵m 𝐴))
9 poss 5484 . . 3 (𝑈 ⊆ (𝐵m 𝐴) → (𝑇 Po (𝐵m 𝐴) → 𝑇 Po 𝑈))
101, 8, 9mpsyl 68 . 2 (𝜑𝑇 Po 𝑈)
11 df-ne 2942 . . . . 5 (𝑎𝑏 ↔ ¬ 𝑎 = 𝑏)
12 wemapsolem.4 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ∃𝑐 ∈ dom (𝑎𝑏)∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐)
13 simprll 779 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑎𝑈)
141, 13sselid 3912 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑎 ∈ (𝐵m 𝐴))
15 elmapi 8550 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ (𝐵m 𝐴) → 𝑎:𝐴𝐵)
1614, 15syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑎:𝐴𝐵)
1716ffnd 6564 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑎 Fn 𝐴)
18 simprlr 780 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑏𝑈)
191, 18sselid 3912 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑏 ∈ (𝐵m 𝐴))
20 elmapi 8550 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝐵m 𝐴) → 𝑏:𝐴𝐵)
2119, 20syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑏:𝐴𝐵)
2221ffnd 6564 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → 𝑏 Fn 𝐴)
23 fndmdif 6880 . . . . . . . . . . . . . . 15 ((𝑎 Fn 𝐴𝑏 Fn 𝐴) → dom (𝑎𝑏) = {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)})
2417, 22, 23syl2anc 587 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → dom (𝑎𝑏) = {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)})
2524eleq2d 2824 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑐 ∈ dom (𝑎𝑏) ↔ 𝑐 ∈ {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)}))
26 nesym 2998 . . . . . . . . . . . . . . 15 ((𝑎𝑥) ≠ (𝑏𝑥) ↔ ¬ (𝑏𝑥) = (𝑎𝑥))
27 fveq2 6735 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑐 → (𝑏𝑥) = (𝑏𝑐))
28 fveq2 6735 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑐 → (𝑎𝑥) = (𝑎𝑐))
2927, 28eqeq12d 2754 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑐 → ((𝑏𝑥) = (𝑎𝑥) ↔ (𝑏𝑐) = (𝑎𝑐)))
3029notbid 321 . . . . . . . . . . . . . . 15 (𝑥 = 𝑐 → (¬ (𝑏𝑥) = (𝑎𝑥) ↔ ¬ (𝑏𝑐) = (𝑎𝑐)))
3126, 30syl5bb 286 . . . . . . . . . . . . . 14 (𝑥 = 𝑐 → ((𝑎𝑥) ≠ (𝑏𝑥) ↔ ¬ (𝑏𝑐) = (𝑎𝑐)))
3231elrab 3614 . . . . . . . . . . . . 13 (𝑐 ∈ {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)} ↔ (𝑐𝐴 ∧ ¬ (𝑏𝑐) = (𝑎𝑐)))
3325, 32bitrdi 290 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑐 ∈ dom (𝑎𝑏) ↔ (𝑐𝐴 ∧ ¬ (𝑏𝑐) = (𝑎𝑐))))
3424eleq2d 2824 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑑 ∈ dom (𝑎𝑏) ↔ 𝑑 ∈ {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)}))
35 fveq2 6735 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑑 → (𝑏𝑥) = (𝑏𝑑))
36 fveq2 6735 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑑 → (𝑎𝑥) = (𝑎𝑑))
3735, 36eqeq12d 2754 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑑 → ((𝑏𝑥) = (𝑎𝑥) ↔ (𝑏𝑑) = (𝑎𝑑)))
3837notbid 321 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑑 → (¬ (𝑏𝑥) = (𝑎𝑥) ↔ ¬ (𝑏𝑑) = (𝑎𝑑)))
3926, 38syl5bb 286 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑑 → ((𝑎𝑥) ≠ (𝑏𝑥) ↔ ¬ (𝑏𝑑) = (𝑎𝑑)))
4039elrab 3614 . . . . . . . . . . . . . . . 16 (𝑑 ∈ {𝑥𝐴 ∣ (𝑎𝑥) ≠ (𝑏𝑥)} ↔ (𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑)))
4134, 40bitrdi 290 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑑 ∈ dom (𝑎𝑏) ↔ (𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑))))
4241imbi1d 345 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ((𝑑 ∈ dom (𝑎𝑏) → ¬ 𝑑𝑅𝑐) ↔ ((𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑)) → ¬ 𝑑𝑅𝑐)))
43 impexp 454 . . . . . . . . . . . . . . 15 (((𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑)) → ¬ 𝑑𝑅𝑐) ↔ (𝑑𝐴 → (¬ (𝑏𝑑) = (𝑎𝑑) → ¬ 𝑑𝑅𝑐)))
44 con34b 319 . . . . . . . . . . . . . . . 16 ((𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)) ↔ (¬ (𝑏𝑑) = (𝑎𝑑) → ¬ 𝑑𝑅𝑐))
4544imbi2i 339 . . . . . . . . . . . . . . 15 ((𝑑𝐴 → (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ↔ (𝑑𝐴 → (¬ (𝑏𝑑) = (𝑎𝑑) → ¬ 𝑑𝑅𝑐)))
4643, 45bitr4i 281 . . . . . . . . . . . . . 14 (((𝑑𝐴 ∧ ¬ (𝑏𝑑) = (𝑎𝑑)) → ¬ 𝑑𝑅𝑐) ↔ (𝑑𝐴 → (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
4742, 46bitrdi 290 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ((𝑑 ∈ dom (𝑎𝑏) → ¬ 𝑑𝑅𝑐) ↔ (𝑑𝐴 → (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
4847ralbidv2 3117 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐 ↔ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
4933, 48anbi12d 634 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ((𝑐 ∈ dom (𝑎𝑏) ∧ ∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐) ↔ ((𝑐𝐴 ∧ ¬ (𝑏𝑐) = (𝑎𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
50 anass 472 . . . . . . . . . . 11 (((𝑐𝐴 ∧ ¬ (𝑏𝑐) = (𝑎𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ↔ (𝑐𝐴 ∧ (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
5149, 50bitrdi 290 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ((𝑐 ∈ dom (𝑎𝑏) ∧ ∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐) ↔ (𝑐𝐴 ∧ (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))))
5251rexbidv2 3222 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (∃𝑐 ∈ dom (𝑎𝑏)∀𝑑 ∈ dom (𝑎𝑏) ¬ 𝑑𝑅𝑐 ↔ ∃𝑐𝐴 (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
5312, 52mpbid 235 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ∃𝑐𝐴 (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
543ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → 𝑆 Or 𝐵)
5521ffvelrnda 6922 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → (𝑏𝑐) ∈ 𝐵)
5616ffvelrnda 6922 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → (𝑎𝑐) ∈ 𝐵)
57 sotrieq 5511 . . . . . . . . . . . . 13 ((𝑆 Or 𝐵 ∧ ((𝑏𝑐) ∈ 𝐵 ∧ (𝑎𝑐) ∈ 𝐵)) → ((𝑏𝑐) = (𝑎𝑐) ↔ ¬ ((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐))))
5857con2bid 358 . . . . . . . . . . . 12 ((𝑆 Or 𝐵 ∧ ((𝑏𝑐) ∈ 𝐵 ∧ (𝑎𝑐) ∈ 𝐵)) → (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ↔ ¬ (𝑏𝑐) = (𝑎𝑐)))
5958biimprd 251 . . . . . . . . . . 11 ((𝑆 Or 𝐵 ∧ ((𝑏𝑐) ∈ 𝐵 ∧ (𝑎𝑐) ∈ 𝐵)) → (¬ (𝑏𝑐) = (𝑎𝑐) → ((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐))))
6054, 55, 56, 59syl12anc 837 . . . . . . . . . 10 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → (¬ (𝑏𝑐) = (𝑎𝑐) → ((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐))))
6160anim1d 614 . . . . . . . . 9 (((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) ∧ 𝑐𝐴) → ((¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) → (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
6261reximdva 3201 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (∃𝑐𝐴 (¬ (𝑏𝑐) = (𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) → ∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
6353, 62mpd 15 . . . . . . 7 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → ∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
646wemaplem1 9186 . . . . . . . . . 10 ((𝑏 ∈ V ∧ 𝑎 ∈ V) → (𝑏𝑇𝑎 ↔ ∃𝑐𝐴 ((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
6564el2v 3428 . . . . . . . . 9 (𝑏𝑇𝑎 ↔ ∃𝑐𝐴 ((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
666wemaplem1 9186 . . . . . . . . . 10 ((𝑎 ∈ V ∧ 𝑏 ∈ V) → (𝑎𝑇𝑏 ↔ ∃𝑐𝐴 ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))))
6766el2v 3428 . . . . . . . . 9 (𝑎𝑇𝑏 ↔ ∃𝑐𝐴 ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑))))
6865, 67orbi12i 915 . . . . . . . 8 ((𝑏𝑇𝑎𝑎𝑇𝑏) ↔ (∃𝑐𝐴 ((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ∃𝑐𝐴 ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))))
69 r19.43 3276 . . . . . . . 8 (∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))) ↔ (∃𝑐𝐴 ((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ∃𝑐𝐴 ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))))
70 andir 1009 . . . . . . . . . 10 ((((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ↔ (((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))))
71 eqcom 2745 . . . . . . . . . . . . . 14 ((𝑏𝑑) = (𝑎𝑑) ↔ (𝑎𝑑) = (𝑏𝑑))
7271imbi2i 339 . . . . . . . . . . . . 13 ((𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)) ↔ (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))
7372ralbii 3089 . . . . . . . . . . . 12 (∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)) ↔ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))
7473anbi2i 626 . . . . . . . . . . 11 (((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ↔ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑))))
7574orbi2i 913 . . . . . . . . . 10 ((((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑)))) ↔ (((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))))
7670, 75bitr2i 279 . . . . . . . . 9 ((((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))) ↔ (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
7776rexbii 3176 . . . . . . . 8 (∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))) ∨ ((𝑎𝑐)𝑆(𝑏𝑐) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑎𝑑) = (𝑏𝑑)))) ↔ ∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
7868, 69, 773bitr2i 302 . . . . . . 7 ((𝑏𝑇𝑎𝑎𝑇𝑏) ↔ ∃𝑐𝐴 (((𝑏𝑐)𝑆(𝑎𝑐) ∨ (𝑎𝑐)𝑆(𝑏𝑐)) ∧ ∀𝑑𝐴 (𝑑𝑅𝑐 → (𝑏𝑑) = (𝑎𝑑))))
7963, 78sylibr 237 . . . . . 6 ((𝜑 ∧ ((𝑎𝑈𝑏𝑈) ∧ 𝑎𝑏)) → (𝑏𝑇𝑎𝑎𝑇𝑏))
8079expr 460 . . . . 5 ((𝜑 ∧ (𝑎𝑈𝑏𝑈)) → (𝑎𝑏 → (𝑏𝑇𝑎𝑎𝑇𝑏)))
8111, 80syl5bir 246 . . . 4 ((𝜑 ∧ (𝑎𝑈𝑏𝑈)) → (¬ 𝑎 = 𝑏 → (𝑏𝑇𝑎𝑎𝑇𝑏)))
8281orrd 863 . . 3 ((𝜑 ∧ (𝑎𝑈𝑏𝑈)) → (𝑎 = 𝑏 ∨ (𝑏𝑇𝑎𝑎𝑇𝑏)))
83 3orrot 1094 . . . 4 ((𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎) ↔ (𝑎 = 𝑏𝑏𝑇𝑎𝑎𝑇𝑏))
84 3orass 1092 . . . 4 ((𝑎 = 𝑏𝑏𝑇𝑎𝑎𝑇𝑏) ↔ (𝑎 = 𝑏 ∨ (𝑏𝑇𝑎𝑎𝑇𝑏)))
8583, 84bitr2i 279 . . 3 ((𝑎 = 𝑏 ∨ (𝑏𝑇𝑎𝑎𝑇𝑏)) ↔ (𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎))
8682, 85sylib 221 . 2 ((𝜑 ∧ (𝑎𝑈𝑏𝑈)) → (𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎))
8710, 86issod 5515 1 (𝜑𝑇 Or 𝑈)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 847  w3o 1088   = wceq 1543  wcel 2111  wne 2941  wral 3062  wrex 3063  {crab 3066  Vcvv 3420  cdif 3877  wss 3880   class class class wbr 5067  {copab 5129   Po wpo 5480   Or wor 5481  dom cdm 5565   Fn wfn 6392  wf 6393  cfv 6397  (class class class)co 7231  m cmap 8528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5206  ax-nul 5213  ax-pow 5272  ax-pr 5336  ax-un 7541
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3422  df-sbc 3709  df-csb 3826  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4834  df-iun 4920  df-br 5068  df-opab 5130  df-mpt 5150  df-id 5469  df-po 5482  df-so 5483  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-fv 6405  df-ov 7234  df-oprab 7235  df-mpo 7236  df-1st 7779  df-2nd 7780  df-map 8530
This theorem is referenced by:  wemapso  9191  wemapso2lem  9192
  Copyright terms: Public domain W3C validator