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

Metamath Proof Explorer

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