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 ) )