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