Theorem uspgredg2v

Description: In a simple pseudograph, the mapping of edges having a fixed endpoint to the "other" vertex of the edge (which may be the fixed vertex itself in the case of a loop) is a one-to-one function into the set of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 6-Dec-2020)

	Ref	Expression
Hypotheses	uspgredg2v.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	uspgredg2v.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	uspgredg2v.a	⊢ 𝐴 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 }
	uspgredg2v.f	⊢ 𝐹 = ( 𝑦 ∈ 𝐴 ↦ ( ℩ 𝑧 ∈ 𝑉 𝑦 = { 𝑁 , 𝑧 } ) )
Assertion	uspgredg2v	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐹 : 𝐴 –1-1→ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		uspgredg2v.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		uspgredg2v.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		uspgredg2v.a	⊢ 𝐴 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 }
4		uspgredg2v.f	⊢ 𝐹 = ( 𝑦 ∈ 𝐴 ↦ ( ℩ 𝑧 ∈ 𝑉 𝑦 = { 𝑁 , 𝑧 } ) )
5	1 2 3	uspgredg2vlem	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑦 ∈ 𝐴 ) → ( ℩ 𝑧 ∈ 𝑉 𝑦 = { 𝑁 , 𝑧 } ) ∈ 𝑉 )
6	5	ralrimiva	⊢ ( 𝐺 ∈ USPGraph → ∀ 𝑦 ∈ 𝐴 ( ℩ 𝑧 ∈ 𝑉 𝑦 = { 𝑁 , 𝑧 } ) ∈ 𝑉 )
7	6	adantr	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ 𝑉 ) → ∀ 𝑦 ∈ 𝐴 ( ℩ 𝑧 ∈ 𝑉 𝑦 = { 𝑁 , 𝑧 } ) ∈ 𝑉 )
8		preq2	⊢ ( 𝑧 = 𝑛 → { 𝑁 , 𝑧 } = { 𝑁 , 𝑛 } )
9	8	eqeq2d	⊢ ( 𝑧 = 𝑛 → ( 𝑦 = { 𝑁 , 𝑧 } ↔ 𝑦 = { 𝑁 , 𝑛 } ) )
10	9	cbvriotavw	⊢ ( ℩ 𝑧 ∈ 𝑉 𝑦 = { 𝑁 , 𝑧 } ) = ( ℩ 𝑛 ∈ 𝑉 𝑦 = { 𝑁 , 𝑛 } )
11	8	eqeq2d	⊢ ( 𝑧 = 𝑛 → ( 𝑥 = { 𝑁 , 𝑧 } ↔ 𝑥 = { 𝑁 , 𝑛 } ) )
12	11	cbvriotavw	⊢ ( ℩ 𝑧 ∈ 𝑉 𝑥 = { 𝑁 , 𝑧 } ) = ( ℩ 𝑛 ∈ 𝑉 𝑥 = { 𝑁 , 𝑛 } )
13		simpl	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐺 ∈ USPGraph )
14		eleq2w	⊢ ( 𝑒 = 𝑦 → ( 𝑁 ∈ 𝑒 ↔ 𝑁 ∈ 𝑦 ) )
15	14 3	elrab2	⊢ ( 𝑦 ∈ 𝐴 ↔ ( 𝑦 ∈ 𝐸 ∧ 𝑁 ∈ 𝑦 ) )
16	2	eleq2i	⊢ ( 𝑦 ∈ 𝐸 ↔ 𝑦 ∈ ( Edg ‘ 𝐺 ) )
17	16	biimpi	⊢ ( 𝑦 ∈ 𝐸 → 𝑦 ∈ ( Edg ‘ 𝐺 ) )
18	17	anim1i	⊢ ( ( 𝑦 ∈ 𝐸 ∧ 𝑁 ∈ 𝑦 ) → ( 𝑦 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑦 ) )
19	15 18	sylbi	⊢ ( 𝑦 ∈ 𝐴 → ( 𝑦 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑦 ) )
20	19	adantr	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑦 ) )
21	13 20	anim12i	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝐺 ∈ USPGraph ∧ ( 𝑦 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑦 ) ) )
22		3anass	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑦 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑦 ) ↔ ( 𝐺 ∈ USPGraph ∧ ( 𝑦 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑦 ) ) )
23	21 22	sylibr	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝐺 ∈ USPGraph ∧ 𝑦 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑦 ) )
24		uspgredg2vtxeu	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑦 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑦 ) → ∃! 𝑛 ∈ ( Vtx ‘ 𝐺 ) 𝑦 = { 𝑁 , 𝑛 } )
25		reueq1	⊢ ( 𝑉 = ( Vtx ‘ 𝐺 ) → ( ∃! 𝑛 ∈ 𝑉 𝑦 = { 𝑁 , 𝑛 } ↔ ∃! 𝑛 ∈ ( Vtx ‘ 𝐺 ) 𝑦 = { 𝑁 , 𝑛 } ) )
26	1 25	ax-mp	⊢ ( ∃! 𝑛 ∈ 𝑉 𝑦 = { 𝑁 , 𝑛 } ↔ ∃! 𝑛 ∈ ( Vtx ‘ 𝐺 ) 𝑦 = { 𝑁 , 𝑛 } )
27	24 26	sylibr	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑦 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑦 ) → ∃! 𝑛 ∈ 𝑉 𝑦 = { 𝑁 , 𝑛 } )
28	23 27	syl	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ∃! 𝑛 ∈ 𝑉 𝑦 = { 𝑁 , 𝑛 } )
29		eleq2w	⊢ ( 𝑒 = 𝑥 → ( 𝑁 ∈ 𝑒 ↔ 𝑁 ∈ 𝑥 ) )
30	29 3	elrab2	⊢ ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐸 ∧ 𝑁 ∈ 𝑥 ) )
31	2	eleq2i	⊢ ( 𝑥 ∈ 𝐸 ↔ 𝑥 ∈ ( Edg ‘ 𝐺 ) )
32	31	biimpi	⊢ ( 𝑥 ∈ 𝐸 → 𝑥 ∈ ( Edg ‘ 𝐺 ) )
33	32	anim1i	⊢ ( ( 𝑥 ∈ 𝐸 ∧ 𝑁 ∈ 𝑥 ) → ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑥 ) )
34	30 33	sylbi	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑥 ) )
35	34	adantl	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑥 ) )
36	13 35	anim12i	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑥 ) ) )
37		3anass	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑥 ) ↔ ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑥 ) ) )
38	36 37	sylibr	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝐺 ∈ USPGraph ∧ 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑥 ) )
39		uspgredg2vtxeu	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑥 ) → ∃! 𝑛 ∈ ( Vtx ‘ 𝐺 ) 𝑥 = { 𝑁 , 𝑛 } )
40		reueq1	⊢ ( 𝑉 = ( Vtx ‘ 𝐺 ) → ( ∃! 𝑛 ∈ 𝑉 𝑥 = { 𝑁 , 𝑛 } ↔ ∃! 𝑛 ∈ ( Vtx ‘ 𝐺 ) 𝑥 = { 𝑁 , 𝑛 } ) )
41	1 40	ax-mp	⊢ ( ∃! 𝑛 ∈ 𝑉 𝑥 = { 𝑁 , 𝑛 } ↔ ∃! 𝑛 ∈ ( Vtx ‘ 𝐺 ) 𝑥 = { 𝑁 , 𝑛 } )
42	39 41	sylibr	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑥 ) → ∃! 𝑛 ∈ 𝑉 𝑥 = { 𝑁 , 𝑛 } )
43	38 42	syl	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ∃! 𝑛 ∈ 𝑉 𝑥 = { 𝑁 , 𝑛 } )
44	10 12 28 43	riotaeqimp	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) ∧ ( ℩ 𝑧 ∈ 𝑉 𝑦 = { 𝑁 , 𝑧 } ) = ( ℩ 𝑧 ∈ 𝑉 𝑥 = { 𝑁 , 𝑧 } ) ) → 𝑦 = 𝑥 )
45	44	ex	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ( ( ℩ 𝑧 ∈ 𝑉 𝑦 = { 𝑁 , 𝑧 } ) = ( ℩ 𝑧 ∈ 𝑉 𝑥 = { 𝑁 , 𝑧 } ) → 𝑦 = 𝑥 ) )
46	45	ralrimivva	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ 𝑉 ) → ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( ( ℩ 𝑧 ∈ 𝑉 𝑦 = { 𝑁 , 𝑧 } ) = ( ℩ 𝑧 ∈ 𝑉 𝑥 = { 𝑁 , 𝑧 } ) → 𝑦 = 𝑥 ) )
47		eqeq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 = { 𝑁 , 𝑧 } ↔ 𝑥 = { 𝑁 , 𝑧 } ) )
48	47	riotabidv	⊢ ( 𝑦 = 𝑥 → ( ℩ 𝑧 ∈ 𝑉 𝑦 = { 𝑁 , 𝑧 } ) = ( ℩ 𝑧 ∈ 𝑉 𝑥 = { 𝑁 , 𝑧 } ) )
49	4 48	f1mpt	⊢ ( 𝐹 : 𝐴 –1-1→ 𝑉 ↔ ( ∀ 𝑦 ∈ 𝐴 ( ℩ 𝑧 ∈ 𝑉 𝑦 = { 𝑁 , 𝑧 } ) ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( ( ℩ 𝑧 ∈ 𝑉 𝑦 = { 𝑁 , 𝑧 } ) = ( ℩ 𝑧 ∈ 𝑉 𝑥 = { 𝑁 , 𝑧 } ) → 𝑦 = 𝑥 ) ) )
50	7 46 49	sylanbrc	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐹 : 𝐴 –1-1→ 𝑉 )