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