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

Theorem cusgrfilem2 28980
Description: Lemma 2 for cusgrfi 28982. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.)
Hypotheses
Ref Expression
cusgrfi.v 𝑉 = (Vtx‘𝐺)
cusgrfi.p 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})}
cusgrfi.f 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↩ {𝑥, 𝑁})
Assertion
Ref Expression
cusgrfilem2 (𝑁 ∈ 𝑉 → 𝐹:(𝑉 ∖ {𝑁})–1-1-onto→𝑃)
Distinct variable groups:   𝑥,𝐺   𝑁,𝑎,𝑥   𝑉,𝑎,𝑥   𝑥,𝑃
Allowed substitution hints:   𝑃(𝑎)   𝐹(𝑥,𝑎)   𝐺(𝑎)

Proof of Theorem cusgrfilem2
Dummy variables 𝑒 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eldifi 4125 . . . . 5 (𝑥 ∈ (𝑉 ∖ {𝑁}) → 𝑥 ∈ 𝑉)
2 id 22 . . . . 5 (𝑁 ∈ 𝑉 → 𝑁 ∈ 𝑉)
3 prelpwi 5446 . . . . 5 ((𝑥 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) → {𝑥, 𝑁} ∈ 𝒫 𝑉)
41, 2, 3syl2anr 595 . . . 4 ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → {𝑥, 𝑁} ∈ 𝒫 𝑉)
51adantl 480 . . . . 5 ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → 𝑥 ∈ 𝑉)
6 eldifsni 4792 . . . . . . 7 (𝑥 ∈ (𝑉 ∖ {𝑁}) → 𝑥 ≠ 𝑁)
76adantl 480 . . . . . 6 ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → 𝑥 ≠ 𝑁)
8 eqidd 2731 . . . . . 6 ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → {𝑥, 𝑁} = {𝑥, 𝑁})
97, 8jca 510 . . . . 5 ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → (𝑥 ≠ 𝑁 ∧ {𝑥, 𝑁} = {𝑥, 𝑁}))
10 id 22 . . . . . 6 (𝑥 ∈ 𝑉 → 𝑥 ∈ 𝑉)
11 neeq1 3001 . . . . . . . 8 (𝑎 = 𝑥 → (𝑎 ≠ 𝑁 ↔ 𝑥 ≠ 𝑁))
12 preq1 4736 . . . . . . . . 9 (𝑎 = 𝑥 → {𝑎, 𝑁} = {𝑥, 𝑁})
1312eqeq2d 2741 . . . . . . . 8 (𝑎 = 𝑥 → ({𝑥, 𝑁} = {𝑎, 𝑁} ↔ {𝑥, 𝑁} = {𝑥, 𝑁}))
1411, 13anbi12d 629 . . . . . . 7 (𝑎 = 𝑥 → ((𝑎 ≠ 𝑁 ∧ {𝑥, 𝑁} = {𝑎, 𝑁}) ↔ (𝑥 ≠ 𝑁 ∧ {𝑥, 𝑁} = {𝑥, 𝑁})))
1514adantl 480 . . . . . 6 ((𝑥 ∈ 𝑉 ∧ 𝑎 = 𝑥) → ((𝑎 ≠ 𝑁 ∧ {𝑥, 𝑁} = {𝑎, 𝑁}) ↔ (𝑥 ≠ 𝑁 ∧ {𝑥, 𝑁} = {𝑥, 𝑁})))
1610, 15rspcedv 3604 . . . . 5 (𝑥 ∈ 𝑉 → ((𝑥 ≠ 𝑁 ∧ {𝑥, 𝑁} = {𝑥, 𝑁}) → ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ {𝑥, 𝑁} = {𝑎, 𝑁})))
175, 9, 16sylc 65 . . . 4 ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ {𝑥, 𝑁} = {𝑎, 𝑁}))
18 cusgrfi.p . . . . . 6 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})}
1918eleq2i 2823 . . . . 5 ({𝑥, 𝑁} ∈ 𝑃 ↔ {𝑥, 𝑁} ∈ {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})})
20 eqeq1 2734 . . . . . . . 8 (𝑣 = {𝑥, 𝑁} → (𝑣 = {𝑎, 𝑁} ↔ {𝑥, 𝑁} = {𝑎, 𝑁}))
2120anbi2d 627 . . . . . . 7 (𝑣 = {𝑥, 𝑁} → ((𝑎 ≠ 𝑁 ∧ 𝑣 = {𝑎, 𝑁}) ↔ (𝑎 ≠ 𝑁 ∧ {𝑥, 𝑁} = {𝑎, 𝑁})))
2221rexbidv 3176 . . . . . 6 (𝑣 = {𝑥, 𝑁} → (∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑣 = {𝑎, 𝑁}) ↔ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ {𝑥, 𝑁} = {𝑎, 𝑁})))
23 eqeq1 2734 . . . . . . . . 9 (𝑥 = 𝑣 → (𝑥 = {𝑎, 𝑁} ↔ 𝑣 = {𝑎, 𝑁}))
2423anbi2d 627 . . . . . . . 8 (𝑥 = 𝑣 → ((𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁}) ↔ (𝑎 ≠ 𝑁 ∧ 𝑣 = {𝑎, 𝑁})))
2524rexbidv 3176 . . . . . . 7 (𝑥 = 𝑣 → (∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁}) ↔ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑣 = {𝑎, 𝑁})))
2625cbvrabv 3440 . . . . . 6 {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})} = {𝑣 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑣 = {𝑎, 𝑁})}
2722, 26elrab2 3685 . . . . 5 ({𝑥, 𝑁} ∈ {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})} ↔ ({𝑥, 𝑁} ∈ 𝒫 𝑉 ∧ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ {𝑥, 𝑁} = {𝑎, 𝑁})))
2819, 27bitri 274 . . . 4 ({𝑥, 𝑁} ∈ 𝑃 ↔ ({𝑥, 𝑁} ∈ 𝒫 𝑉 ∧ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ {𝑥, 𝑁} = {𝑎, 𝑁})))
294, 17, 28sylanbrc 581 . . 3 ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → {𝑥, 𝑁} ∈ 𝑃)
3029ralrimiva 3144 . 2 (𝑁 ∈ 𝑉 → ∀𝑥 ∈ (𝑉 ∖ {𝑁}){𝑥, 𝑁} ∈ 𝑃)
31 simpl 481 . . . . . . . . . . 11 ((𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}) → 𝑎 ≠ 𝑁)
3231anim2i 615 . . . . . . . . . 10 ((𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁})) → (𝑎 ∈ 𝑉 ∧ 𝑎 ≠ 𝑁))
3332adantl 480 . . . . . . . . 9 (((𝑁 ∈ 𝑉 ∧ 𝑒 ∈ 𝒫 𝑉) ∧ (𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}))) → (𝑎 ∈ 𝑉 ∧ 𝑎 ≠ 𝑁))
34 eldifsn 4789 . . . . . . . . 9 (𝑎 ∈ (𝑉 ∖ {𝑁}) ↔ (𝑎 ∈ 𝑉 ∧ 𝑎 ≠ 𝑁))
3533, 34sylibr 233 . . . . . . . 8 (((𝑁 ∈ 𝑉 ∧ 𝑒 ∈ 𝒫 𝑉) ∧ (𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}))) → 𝑎 ∈ (𝑉 ∖ {𝑁}))
36 eqeq1 2734 . . . . . . . . . . . . . 14 (𝑒 = {𝑎, 𝑁} → (𝑒 = {𝑥, 𝑁} ↔ {𝑎, 𝑁} = {𝑥, 𝑁}))
3736adantl 480 . . . . . . . . . . . . 13 ((𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}) → (𝑒 = {𝑥, 𝑁} ↔ {𝑎, 𝑁} = {𝑥, 𝑁}))
3837ad2antlr 723 . . . . . . . . . . . 12 (((𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁})) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → (𝑒 = {𝑥, 𝑁} ↔ {𝑎, 𝑁} = {𝑥, 𝑁}))
39 vex 3476 . . . . . . . . . . . . . 14 𝑎 ∈ V
40 vex 3476 . . . . . . . . . . . . . 14 𝑥 ∈ V
4139, 40preqr1 4848 . . . . . . . . . . . . 13 ({𝑎, 𝑁} = {𝑥, 𝑁} → 𝑎 = 𝑥)
4241equcomd 2020 . . . . . . . . . . . 12 ({𝑎, 𝑁} = {𝑥, 𝑁} → 𝑥 = 𝑎)
4338, 42syl6bi 252 . . . . . . . . . . 11 (((𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁})) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → (𝑒 = {𝑥, 𝑁} → 𝑥 = 𝑎))
4443adantll 710 . . . . . . . . . 10 ((((𝑁 ∈ 𝑉 ∧ 𝑒 ∈ 𝒫 𝑉) ∧ (𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}))) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → (𝑒 = {𝑥, 𝑁} → 𝑥 = 𝑎))
4512equcoms 2021 . . . . . . . . . . . . . . 15 (𝑥 = 𝑎 → {𝑎, 𝑁} = {𝑥, 𝑁})
4645eqeq2d 2741 . . . . . . . . . . . . . 14 (𝑥 = 𝑎 → (𝑒 = {𝑎, 𝑁} ↔ 𝑒 = {𝑥, 𝑁}))
4746biimpcd 248 . . . . . . . . . . . . 13 (𝑒 = {𝑎, 𝑁} → (𝑥 = 𝑎 → 𝑒 = {𝑥, 𝑁}))
4847adantl 480 . . . . . . . . . . . 12 ((𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}) → (𝑥 = 𝑎 → 𝑒 = {𝑥, 𝑁}))
4948adantl 480 . . . . . . . . . . 11 ((𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁})) → (𝑥 = 𝑎 → 𝑒 = {𝑥, 𝑁}))
5049ad2antlr 723 . . . . . . . . . 10 ((((𝑁 ∈ 𝑉 ∧ 𝑒 ∈ 𝒫 𝑉) ∧ (𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}))) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → (𝑥 = 𝑎 → 𝑒 = {𝑥, 𝑁}))
5144, 50impbid 211 . . . . . . . . 9 ((((𝑁 ∈ 𝑉 ∧ 𝑒 ∈ 𝒫 𝑉) ∧ (𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}))) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → (𝑒 = {𝑥, 𝑁} ↔ 𝑥 = 𝑎))
5251ralrimiva 3144 . . . . . . . 8 (((𝑁 ∈ 𝑉 ∧ 𝑒 ∈ 𝒫 𝑉) ∧ (𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}))) → ∀𝑥 ∈ (𝑉 ∖ {𝑁})(𝑒 = {𝑥, 𝑁} ↔ 𝑥 = 𝑎))
5335, 52jca 510 . . . . . . 7 (((𝑁 ∈ 𝑉 ∧ 𝑒 ∈ 𝒫 𝑉) ∧ (𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}))) → (𝑎 ∈ (𝑉 ∖ {𝑁}) ∧ ∀𝑥 ∈ (𝑉 ∖ {𝑁})(𝑒 = {𝑥, 𝑁} ↔ 𝑥 = 𝑎)))
5453ex 411 . . . . . 6 ((𝑁 ∈ 𝑉 ∧ 𝑒 ∈ 𝒫 𝑉) → ((𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁})) → (𝑎 ∈ (𝑉 ∖ {𝑁}) ∧ ∀𝑥 ∈ (𝑉 ∖ {𝑁})(𝑒 = {𝑥, 𝑁} ↔ 𝑥 = 𝑎))))
5554reximdv2 3162 . . . . 5 ((𝑁 ∈ 𝑉 ∧ 𝑒 ∈ 𝒫 𝑉) → (∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}) → ∃𝑎 ∈ (𝑉 ∖ {𝑁})∀𝑥 ∈ (𝑉 ∖ {𝑁})(𝑒 = {𝑥, 𝑁} ↔ 𝑥 = 𝑎)))
5655expimpd 452 . . . 4 (𝑁 ∈ 𝑉 → ((𝑒 ∈ 𝒫 𝑉 ∧ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁})) → ∃𝑎 ∈ (𝑉 ∖ {𝑁})∀𝑥 ∈ (𝑉 ∖ {𝑁})(𝑒 = {𝑥, 𝑁} ↔ 𝑥 = 𝑎)))
57 eqeq1 2734 . . . . . . 7 (𝑥 = 𝑒 → (𝑥 = {𝑎, 𝑁} ↔ 𝑒 = {𝑎, 𝑁}))
5857anbi2d 627 . . . . . 6 (𝑥 = 𝑒 → ((𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁}) ↔ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁})))
5958rexbidv 3176 . . . . 5 (𝑥 = 𝑒 → (∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁}) ↔ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁})))
6059, 18elrab2 3685 . . . 4 (𝑒 ∈ 𝑃 ↔ (𝑒 ∈ 𝒫 𝑉 ∧ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁})))
61 reu6 3721 . . . 4 (∃!𝑥 ∈ (𝑉 ∖ {𝑁})𝑒 = {𝑥, 𝑁} ↔ ∃𝑎 ∈ (𝑉 ∖ {𝑁})∀𝑥 ∈ (𝑉 ∖ {𝑁})(𝑒 = {𝑥, 𝑁} ↔ 𝑥 = 𝑎))
6256, 60, 613imtr4g 295 . . 3 (𝑁 ∈ 𝑉 → (𝑒 ∈ 𝑃 → ∃!𝑥 ∈ (𝑉 ∖ {𝑁})𝑒 = {𝑥, 𝑁}))
6362ralrimiv 3143 . 2 (𝑁 ∈ 𝑉 → ∀𝑒 ∈ 𝑃 ∃!𝑥 ∈ (𝑉 ∖ {𝑁})𝑒 = {𝑥, 𝑁})
64 cusgrfi.f . . 3 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↩ {𝑥, 𝑁})
6564f1ompt 7111 . 2 (𝐹:(𝑉 ∖ {𝑁})–1-1-onto→𝑃 ↔ (∀𝑥 ∈ (𝑉 ∖ {𝑁}){𝑥, 𝑁} ∈ 𝑃 ∧ ∀𝑒 ∈ 𝑃 ∃!𝑥 ∈ (𝑉 ∖ {𝑁})𝑒 = {𝑥, 𝑁}))
6630, 63, 65sylanbrc 581 1 (𝑁 ∈ 𝑉 → 𝐹:(𝑉 ∖ {𝑁})–1-1-onto→𝑃)
Colors of variables: wff setvar class
Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104   ≠ wne 2938  âˆ€wral 3059  âˆƒwrex 3068  âˆƒ!wreu 3372  {crab 3430   ∖ cdif 3944  ð’« cpw 4601  {csn 4627  {cpr 4629   ↩ cmpt 5230  â€“1-1-onto→wf1o 6541  â€˜cfv 6542  Vtxcvtx 28523
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549
This theorem is referenced by:  cusgrfilem3  28981
  Copyright terms: Public domain W3C validator