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

Metamath Proof Explorer

Theorem cusgrfilem3

Description: Lemma 3 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 cusgrfilem3 ( 𝑁 ∈ 𝑉 → ( 𝑉 ∈ Fin ↔ 𝑃 ∈ Fin ) )

Proof

Step Hyp Ref Expression
1 cusgrfi.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 cusgrfi.p ⊢ 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) }
3 cusgrfi.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ↦ { 𝑥 , 𝑁 } )
4 diffi ⊢ ( 𝑉 ∈ Fin → ( 𝑉 ∖ { 𝑁 } ) ∈ Fin )
5 simpr ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ¬ 𝑉 ∈ Fin ) → ¬ 𝑉 ∈ Fin )
6 snfi ⊢ { 𝑁 } ∈ Fin
7 difinf ⊢ ( ( ¬ 𝑉 ∈ Fin ∧ { 𝑁 } ∈ Fin ) → ¬ ( 𝑉 ∖ { 𝑁 } ) ∈ Fin )
8 5 6 7 sylancl ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ¬ 𝑉 ∈ Fin ) → ¬ ( 𝑉 ∖ { 𝑁 } ) ∈ Fin )
9 8 ex ⊢ ( 𝑁 ∈ 𝑉 → ( ¬ 𝑉 ∈ Fin → ¬ ( 𝑉 ∖ { 𝑁 } ) ∈ Fin ) )
10 9 con4d ⊢ ( 𝑁 ∈ 𝑉 → ( ( 𝑉 ∖ { 𝑁 } ) ∈ Fin → 𝑉 ∈ Fin ) )
11 4 10 impbid2 ⊢ ( 𝑁 ∈ 𝑉 → ( 𝑉 ∈ Fin ↔ ( 𝑉 ∖ { 𝑁 } ) ∈ Fin ) )
12 1 fvexi ⊢ 𝑉 ∈ V
13 12 difexi ⊢ ( 𝑉 ∖ { 𝑁 } ) ∈ V
14 mptexg ⊢ ( ( 𝑉 ∖ { 𝑁 } ) ∈ V → ( 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ↦ { 𝑥 , 𝑁 } ) ∈ V )
15 13 14 mp1i ⊢ ( 𝑁 ∈ 𝑉 → ( 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ↦ { 𝑥 , 𝑁 } ) ∈ V )
16 3 15 eqeltrid ⊢ ( 𝑁 ∈ 𝑉 → 𝐹 ∈ V )
17 1 2 3 cusgrfilem2 ⊢ ( 𝑁 ∈ 𝑉 → 𝐹 : ( 𝑉 ∖ { 𝑁 } ) –1-1-onto→ 𝑃 )
18 f1oeq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 : ( 𝑉 ∖ { 𝑁 } ) –1-1-onto→ 𝑃 ↔ 𝐹 : ( 𝑉 ∖ { 𝑁 } ) –1-1-onto→ 𝑃 ) )
19 16 17 18 spcedv ⊢ ( 𝑁 ∈ 𝑉 → ∃ 𝑓 𝑓 : ( 𝑉 ∖ { 𝑁 } ) –1-1-onto→ 𝑃 )
20 bren ⊢ ( ( 𝑉 ∖ { 𝑁 } ) ≈ 𝑃 ↔ ∃ 𝑓 𝑓 : ( 𝑉 ∖ { 𝑁 } ) –1-1-onto→ 𝑃 )
21 19 20 sylibr ⊢ ( 𝑁 ∈ 𝑉 → ( 𝑉 ∖ { 𝑁 } ) ≈ 𝑃 )
22 enfi ⊢ ( ( 𝑉 ∖ { 𝑁 } ) ≈ 𝑃 → ( ( 𝑉 ∖ { 𝑁 } ) ∈ Fin ↔ 𝑃 ∈ Fin ) )
23 21 22 syl ⊢ ( 𝑁 ∈ 𝑉 → ( ( 𝑉 ∖ { 𝑁 } ) ∈ Fin ↔ 𝑃 ∈ Fin ) )
24 11 23 bitrd ⊢ ( 𝑁 ∈ 𝑉 → ( 𝑉 ∈ Fin ↔ 𝑃 ∈ Fin ) )