This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cusgrfilem2

Description: Lemma 2 for cusgrfi . (Contributed by Alexander van der Vekens, 13-Jan-2018) (Revised by AV, 11-Nov-2020)

Ref Expression
Hypotheses cusgrfi.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
cusgrfi.p ⊢ 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) }
cusgrfi.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ↦ { 𝑥 , 𝑁 } )
Assertion cusgrfilem2 ( 𝑁 ∈ 𝑉 → 𝐹 : ( 𝑉 ∖ { 𝑁 } ) –1-1-onto→ 𝑃 )

Proof

Step Hyp Ref Expression
1 cusgrfi.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 cusgrfi.p ⊢ 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) }
3 cusgrfi.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ↦ { 𝑥 , 𝑁 } )
4 eldifi ⊢ ( 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) → 𝑥 ∈ 𝑉 )
5 id ⊢ ( 𝑁 ∈ 𝑉 → 𝑁 ∈ 𝑉 )
6 prelpwi ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → { 𝑥 , 𝑁 } ∈ 𝒫 𝑉 )
7 4 5 6 syl2anr ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → { 𝑥 , 𝑁 } ∈ 𝒫 𝑉 )
8 4 adantl ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → 𝑥 ∈ 𝑉 )
9 eldifsni ⊢ ( 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) → 𝑥 ≠ 𝑁 )
10 9 adantl ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → 𝑥 ≠ 𝑁 )
11 eqidd ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → { 𝑥 , 𝑁 } = { 𝑥 , 𝑁 } )
12 10 11 jca ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( 𝑥 ≠ 𝑁 ∧ { 𝑥 , 𝑁 } = { 𝑥 , 𝑁 } ) )
13 id ⊢ ( 𝑥 ∈ 𝑉 → 𝑥 ∈ 𝑉 )
14 neeq1 ⊢ ( 𝑎 = 𝑥 → ( 𝑎 ≠ 𝑁 ↔ 𝑥 ≠ 𝑁 ) )
15 preq1 ⊢ ( 𝑎 = 𝑥 → { 𝑎 , 𝑁 } = { 𝑥 , 𝑁 } )
16 15 eqeq2d ⊢ ( 𝑎 = 𝑥 → ( { 𝑥 , 𝑁 } = { 𝑎 , 𝑁 } ↔ { 𝑥 , 𝑁 } = { 𝑥 , 𝑁 } ) )
17 14 16 anbi12d ⊢ ( 𝑎 = 𝑥 → ( ( 𝑎 ≠ 𝑁 ∧ { 𝑥 , 𝑁 } = { 𝑎 , 𝑁 } ) ↔ ( 𝑥 ≠ 𝑁 ∧ { 𝑥 , 𝑁 } = { 𝑥 , 𝑁 } ) ) )
18 17 adantl ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑎 = 𝑥 ) → ( ( 𝑎 ≠ 𝑁 ∧ { 𝑥 , 𝑁 } = { 𝑎 , 𝑁 } ) ↔ ( 𝑥 ≠ 𝑁 ∧ { 𝑥 , 𝑁 } = { 𝑥 , 𝑁 } ) ) )
19 13 18 rspcedv ⊢ ( 𝑥 ∈ 𝑉 → ( ( 𝑥 ≠ 𝑁 ∧ { 𝑥 , 𝑁 } = { 𝑥 , 𝑁 } ) → ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ { 𝑥 , 𝑁 } = { 𝑎 , 𝑁 } ) ) )
20 8 12 19 sylc ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ { 𝑥 , 𝑁 } = { 𝑎 , 𝑁 } ) )
21 2 eleq2i ⊢ ( { 𝑥 , 𝑁 } ∈ 𝑃 ↔ { 𝑥 , 𝑁 } ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) } )
22 eqeq1 ⊢ ( 𝑣 = { 𝑥 , 𝑁 } → ( 𝑣 = { 𝑎 , 𝑁 } ↔ { 𝑥 , 𝑁 } = { 𝑎 , 𝑁 } ) )
23 22 anbi2d ⊢ ( 𝑣 = { 𝑥 , 𝑁 } → ( ( 𝑎 ≠ 𝑁 ∧ 𝑣 = { 𝑎 , 𝑁 } ) ↔ ( 𝑎 ≠ 𝑁 ∧ { 𝑥 , 𝑁 } = { 𝑎 , 𝑁 } ) ) )
24 23 rexbidv ⊢ ( 𝑣 = { 𝑥 , 𝑁 } → ( ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑣 = { 𝑎 , 𝑁 } ) ↔ ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ { 𝑥 , 𝑁 } = { 𝑎 , 𝑁 } ) ) )
25 eqeq1 ⊢ ( 𝑥 = 𝑣 → ( 𝑥 = { 𝑎 , 𝑁 } ↔ 𝑣 = { 𝑎 , 𝑁 } ) )
26 25 anbi2d ⊢ ( 𝑥 = 𝑣 → ( ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) ↔ ( 𝑎 ≠ 𝑁 ∧ 𝑣 = { 𝑎 , 𝑁 } ) ) )
27 26 rexbidv ⊢ ( 𝑥 = 𝑣 → ( ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) ↔ ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑣 = { 𝑎 , 𝑁 } ) ) )
28 27 cbvrabv ⊢ { 𝑥 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) } = { 𝑣 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑣 = { 𝑎 , 𝑁 } ) }
29 24 28 elrab2 ⊢ ( { 𝑥 , 𝑁 } ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) } ↔ ( { 𝑥 , 𝑁 } ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ { 𝑥 , 𝑁 } = { 𝑎 , 𝑁 } ) ) )
30 21 29 bitri ⊢ ( { 𝑥 , 𝑁 } ∈ 𝑃 ↔ ( { 𝑥 , 𝑁 } ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ { 𝑥 , 𝑁 } = { 𝑎 , 𝑁 } ) ) )
31 7 20 30 sylanbrc ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → { 𝑥 , 𝑁 } ∈ 𝑃 )
32 31 ralrimiva ⊢ ( 𝑁 ∈ 𝑉 → ∀ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑥 , 𝑁 } ∈ 𝑃 )
33 simpl ⊢ ( ( 𝑎 ≠ 𝑁 ∧ 𝑒 = { 𝑎 , 𝑁 } ) → 𝑎 ≠ 𝑁 )
34 33 anim2i ⊢ ( ( 𝑎 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑁 ∧ 𝑒 = { 𝑎 , 𝑁 } ) ) → ( 𝑎 ∈ 𝑉 ∧ 𝑎 ≠ 𝑁 ) )
35 34 adantl ⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑒 ∈ 𝒫 𝑉 ) ∧ ( 𝑎 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑁 ∧ 𝑒 = { 𝑎 , 𝑁 } ) ) ) → ( 𝑎 ∈ 𝑉 ∧ 𝑎 ≠ 𝑁 ) )
36 eldifsn ⊢ ( 𝑎 ∈ ( 𝑉 ∖ { 𝑁 } ) ↔ ( 𝑎 ∈ 𝑉 ∧ 𝑎 ≠ 𝑁 ) )
37 35 36 sylibr ⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑒 ∈ 𝒫 𝑉 ) ∧ ( 𝑎 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑁 ∧ 𝑒 = { 𝑎 , 𝑁 } ) ) ) → 𝑎 ∈ ( 𝑉 ∖ { 𝑁 } ) )
38 eqeq1 ⊢ ( 𝑒 = { 𝑎 , 𝑁 } → ( 𝑒 = { 𝑥 , 𝑁 } ↔ { 𝑎 , 𝑁 } = { 𝑥 , 𝑁 } ) )
39 38 adantl ⊢ ( ( 𝑎 ≠ 𝑁 ∧ 𝑒 = { 𝑎 , 𝑁 } ) → ( 𝑒 = { 𝑥 , 𝑁 } ↔ { 𝑎 , 𝑁 } = { 𝑥 , 𝑁 } ) )
40 39 ad2antlr ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑁 ∧ 𝑒 = { 𝑎 , 𝑁 } ) ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( 𝑒 = { 𝑥 , 𝑁 } ↔ { 𝑎 , 𝑁 } = { 𝑥 , 𝑁 } ) )
41 vex ⊢ 𝑎 ∈ V
42 vex ⊢ 𝑥 ∈ V
43 41 42 preqr1 ⊢ ( { 𝑎 , 𝑁 } = { 𝑥 , 𝑁 } → 𝑎 = 𝑥 )
44 43 equcomd ⊢ ( { 𝑎 , 𝑁 } = { 𝑥 , 𝑁 } → 𝑥 = 𝑎 )
45 40 44 biimtrdi ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑁 ∧ 𝑒 = { 𝑎 , 𝑁 } ) ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( 𝑒 = { 𝑥 , 𝑁 } → 𝑥 = 𝑎 ) )
46 45 adantll ⊢ ( ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑒 ∈ 𝒫 𝑉 ) ∧ ( 𝑎 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑁 ∧ 𝑒 = { 𝑎 , 𝑁 } ) ) ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( 𝑒 = { 𝑥 , 𝑁 } → 𝑥 = 𝑎 ) )
47 15 equcoms ⊢ ( 𝑥 = 𝑎 → { 𝑎 , 𝑁 } = { 𝑥 , 𝑁 } )
48 47 eqeq2d ⊢ ( 𝑥 = 𝑎 → ( 𝑒 = { 𝑎 , 𝑁 } ↔ 𝑒 = { 𝑥 , 𝑁 } ) )
49 48 biimpcd ⊢ ( 𝑒 = { 𝑎 , 𝑁 } → ( 𝑥 = 𝑎 → 𝑒 = { 𝑥 , 𝑁 } ) )
50 49 adantl ⊢ ( ( 𝑎 ≠ 𝑁 ∧ 𝑒 = { 𝑎 , 𝑁 } ) → ( 𝑥 = 𝑎 → 𝑒 = { 𝑥 , 𝑁 } ) )
51 50 adantl ⊢ ( ( 𝑎 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑁 ∧ 𝑒 = { 𝑎 , 𝑁 } ) ) → ( 𝑥 = 𝑎 → 𝑒 = { 𝑥 , 𝑁 } ) )
52 51 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑒 ∈ 𝒫 𝑉 ) ∧ ( 𝑎 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑁 ∧ 𝑒 = { 𝑎 , 𝑁 } ) ) ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( 𝑥 = 𝑎 → 𝑒 = { 𝑥 , 𝑁 } ) )
53 46 52 impbid ⊢ ( ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑒 ∈ 𝒫 𝑉 ) ∧ ( 𝑎 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑁 ∧ 𝑒 = { 𝑎 , 𝑁 } ) ) ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( 𝑒 = { 𝑥 , 𝑁 } ↔ 𝑥 = 𝑎 ) )
54 53 ralrimiva ⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑒 ∈ 𝒫 𝑉 ) ∧ ( 𝑎 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑁 ∧ 𝑒 = { 𝑎 , 𝑁 } ) ) ) → ∀ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑒 = { 𝑥 , 𝑁 } ↔ 𝑥 = 𝑎 ) )
55 37 54 jca ⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑒 ∈ 𝒫 𝑉 ) ∧ ( 𝑎 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑁 ∧ 𝑒 = { 𝑎 , 𝑁 } ) ) ) → ( 𝑎 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ ∀ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑒 = { 𝑥 , 𝑁 } ↔ 𝑥 = 𝑎 ) ) )
56 55 ex ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑒 ∈ 𝒫 𝑉 ) → ( ( 𝑎 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑁 ∧ 𝑒 = { 𝑎 , 𝑁 } ) ) → ( 𝑎 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ ∀ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑒 = { 𝑥 , 𝑁 } ↔ 𝑥 = 𝑎 ) ) ) )
57 56 reximdv2 ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑒 ∈ 𝒫 𝑉 ) → ( ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑒 = { 𝑎 , 𝑁 } ) → ∃ 𝑎 ∈ ( 𝑉 ∖ { 𝑁 } ) ∀ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑒 = { 𝑥 , 𝑁 } ↔ 𝑥 = 𝑎 ) ) )
58 57 expimpd ⊢ ( 𝑁 ∈ 𝑉 → ( ( 𝑒 ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑒 = { 𝑎 , 𝑁 } ) ) → ∃ 𝑎 ∈ ( 𝑉 ∖ { 𝑁 } ) ∀ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑒 = { 𝑥 , 𝑁 } ↔ 𝑥 = 𝑎 ) ) )
59 eqeq1 ⊢ ( 𝑥 = 𝑒 → ( 𝑥 = { 𝑎 , 𝑁 } ↔ 𝑒 = { 𝑎 , 𝑁 } ) )
60 59 anbi2d ⊢ ( 𝑥 = 𝑒 → ( ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) ↔ ( 𝑎 ≠ 𝑁 ∧ 𝑒 = { 𝑎 , 𝑁 } ) ) )
61 60 rexbidv ⊢ ( 𝑥 = 𝑒 → ( ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) ↔ ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑒 = { 𝑎 , 𝑁 } ) ) )
62 61 2 elrab2 ⊢ ( 𝑒 ∈ 𝑃 ↔ ( 𝑒 ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑒 = { 𝑎 , 𝑁 } ) ) )
63 reu6 ⊢ ( ∃! 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑒 = { 𝑥 , 𝑁 } ↔ ∃ 𝑎 ∈ ( 𝑉 ∖ { 𝑁 } ) ∀ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑒 = { 𝑥 , 𝑁 } ↔ 𝑥 = 𝑎 ) )
64 58 62 63 3imtr4g ⊢ ( 𝑁 ∈ 𝑉 → ( 𝑒 ∈ 𝑃 → ∃! 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑒 = { 𝑥 , 𝑁 } ) )
65 64 ralrimiv ⊢ ( 𝑁 ∈ 𝑉 → ∀ 𝑒 ∈ 𝑃 ∃! 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑒 = { 𝑥 , 𝑁 } )
66 3 f1ompt ⊢ ( 𝐹 : ( 𝑉 ∖ { 𝑁 } ) –1-1-onto→ 𝑃 ↔ ( ∀ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑥 , 𝑁 } ∈ 𝑃 ∧ ∀ 𝑒 ∈ 𝑃 ∃! 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑒 = { 𝑥 , 𝑁 } ) )
67 32 65 66 sylanbrc ⊢ ( 𝑁 ∈ 𝑉 → 𝐹 : ( 𝑉 ∖ { 𝑁 } ) –1-1-onto→ 𝑃 )