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

Metamath Proof Explorer

Theorem usgredg2v

Description: In a simple graph, the mapping of edges having a fixed endpoint to the other vertex of the edge is a one-to-one function into the set of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 18-Oct-2020)

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

Proof

Step Hyp Ref Expression
1 usgredg2v.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 usgredg2v.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3 usgredg2v.a ⊢ 𝐴 = { 𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑥 ) }
4 usgredg2v.f ⊢ 𝐹 = ( 𝑦 ∈ 𝐴 ↦ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) )
5 1 2 3 usgredg2vlem1 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑦 ∈ 𝐴 ) → ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) ∈ 𝑉 )
6 5 ralrimiva ⊢ ( 𝐺 ∈ USGraph → ∀ 𝑦 ∈ 𝐴 ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) ∈ 𝑉 )
7 6 adantr ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ∀ 𝑦 ∈ 𝐴 ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) ∈ 𝑉 )
8 2 usgrf1 ⊢ ( 𝐺 ∈ USGraph → 𝐸 : dom 𝐸 –1-1→ ran 𝐸 )
9 8 adantr ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐸 : dom 𝐸 –1-1→ ran 𝐸 )
10 elrabi ⊢ ( 𝑦 ∈ { 𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑥 ) } → 𝑦 ∈ dom 𝐸 )
11 10 3 eleq2s ⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ dom 𝐸 )
12 elrabi ⊢ ( 𝑤 ∈ { 𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑥 ) } → 𝑤 ∈ dom 𝐸 )
13 12 3 eleq2s ⊢ ( 𝑤 ∈ 𝐴 → 𝑤 ∈ dom 𝐸 )
14 11 13 anim12i ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑦 ∈ dom 𝐸 ∧ 𝑤 ∈ dom 𝐸 ) )
15 f1fveq ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ ( 𝑦 ∈ dom 𝐸 ∧ 𝑤 ∈ dom 𝐸 ) ) → ( ( 𝐸 ‘ 𝑦 ) = ( 𝐸 ‘ 𝑤 ) ↔ 𝑦 = 𝑤 ) )
16 9 14 15 syl2an ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝐸 ‘ 𝑦 ) = ( 𝐸 ‘ 𝑤 ) ↔ 𝑦 = 𝑤 ) )
17 16 bicomd ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑦 = 𝑤 ↔ ( 𝐸 ‘ 𝑦 ) = ( 𝐸 ‘ 𝑤 ) ) )
18 17 notbid ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ¬ 𝑦 = 𝑤 ↔ ¬ ( 𝐸 ‘ 𝑦 ) = ( 𝐸 ‘ 𝑤 ) ) )
19 simpl ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐺 ∈ USGraph )
20 simpl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
21 19 20 anim12i ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝐺 ∈ USGraph ∧ 𝑦 ∈ 𝐴 ) )
22 preq1 ⊢ ( 𝑢 = 𝑧 → { 𝑢 , 𝑁 } = { 𝑧 , 𝑁 } )
23 22 eqeq2d ⊢ ( 𝑢 = 𝑧 → ( ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ↔ ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) )
24 23 cbvriotavw ⊢ ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } )
25 1 2 3 usgredg2vlem2 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑦 ∈ 𝐴 ) → ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) → ( 𝐸 ‘ 𝑦 ) = { ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) , 𝑁 } ) )
26 21 24 25 mpisyl ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝐸 ‘ 𝑦 ) = { ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) , 𝑁 } )
27 an3 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝐺 ∈ USGraph ∧ 𝑤 ∈ 𝐴 ) )
28 22 eqeq2d ⊢ ( 𝑢 = 𝑧 → ( ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ↔ ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) )
29 28 cbvriotavw ⊢ ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } )
30 1 2 3 usgredg2vlem2 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑤 ∈ 𝐴 ) → ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) → ( 𝐸 ‘ 𝑤 ) = { ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) , 𝑁 } ) )
31 27 29 30 mpisyl ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝐸 ‘ 𝑤 ) = { ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) , 𝑁 } )
32 26 31 eqeq12d ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝐸 ‘ 𝑦 ) = ( 𝐸 ‘ 𝑤 ) ↔ { ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) , 𝑁 } = { ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) , 𝑁 } ) )
33 32 notbid ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ¬ ( 𝐸 ‘ 𝑦 ) = ( 𝐸 ‘ 𝑤 ) ↔ ¬ { ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) , 𝑁 } = { ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) , 𝑁 } ) )
34 riotaex ⊢ ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) ∈ V
35 34 a1i ⊢ ( 𝑁 ∈ 𝑉 → ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) ∈ V )
36 id ⊢ ( 𝑁 ∈ 𝑉 → 𝑁 ∈ 𝑉 )
37 riotaex ⊢ ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ∈ V
38 37 a1i ⊢ ( 𝑁 ∈ 𝑉 → ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ∈ V )
39 preq12bg ⊢ ( ( ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) ∈ V ∧ 𝑁 ∈ 𝑉 ) ∧ ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ∈ V ∧ 𝑁 ∈ 𝑉 ) ) → ( { ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) , 𝑁 } = { ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) , 𝑁 } ↔ ( ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ∧ 𝑁 = 𝑁 ) ∨ ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = 𝑁 ∧ 𝑁 = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ) ) ) )
40 35 36 38 36 39 syl22anc ⊢ ( 𝑁 ∈ 𝑉 → ( { ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) , 𝑁 } = { ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) , 𝑁 } ↔ ( ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ∧ 𝑁 = 𝑁 ) ∨ ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = 𝑁 ∧ 𝑁 = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ) ) ) )
41 40 notbid ⊢ ( 𝑁 ∈ 𝑉 → ( ¬ { ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) , 𝑁 } = { ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) , 𝑁 } ↔ ¬ ( ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ∧ 𝑁 = 𝑁 ) ∨ ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = 𝑁 ∧ 𝑁 = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ) ) ) )
42 41 adantl ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( ¬ { ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) , 𝑁 } = { ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) , 𝑁 } ↔ ¬ ( ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ∧ 𝑁 = 𝑁 ) ∨ ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = 𝑁 ∧ 𝑁 = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ) ) ) )
43 ioran ⊢ ( ¬ ( ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ∧ 𝑁 = 𝑁 ) ∨ ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = 𝑁 ∧ 𝑁 = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ) ) ↔ ( ¬ ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ∧ 𝑁 = 𝑁 ) ∧ ¬ ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = 𝑁 ∧ 𝑁 = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ) ) )
44 ianor ⊢ ( ¬ ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ∧ 𝑁 = 𝑁 ) ↔ ( ¬ ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ∨ ¬ 𝑁 = 𝑁 ) )
45 24 29 eqeq12i ⊢ ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ↔ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) )
46 45 notbii ⊢ ( ¬ ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ↔ ¬ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) )
47 46 biimpi ⊢ ( ¬ ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) → ¬ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) )
48 47 a1d ⊢ ( ¬ ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) → ( 𝐺 ∈ USGraph → ¬ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) ) )
49 eqid ⊢ 𝑁 = 𝑁
50 49 pm2.24i ⊢ ( ¬ 𝑁 = 𝑁 → ( 𝐺 ∈ USGraph → ¬ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) ) )
51 48 50 jaoi ⊢ ( ( ¬ ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ∨ ¬ 𝑁 = 𝑁 ) → ( 𝐺 ∈ USGraph → ¬ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) ) )
52 44 51 sylbi ⊢ ( ¬ ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ∧ 𝑁 = 𝑁 ) → ( 𝐺 ∈ USGraph → ¬ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) ) )
53 52 adantr ⊢ ( ( ¬ ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ∧ 𝑁 = 𝑁 ) ∧ ¬ ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = 𝑁 ∧ 𝑁 = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ) ) → ( 𝐺 ∈ USGraph → ¬ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) ) )
54 43 53 sylbi ⊢ ( ¬ ( ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ∧ 𝑁 = 𝑁 ) ∨ ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = 𝑁 ∧ 𝑁 = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ) ) → ( 𝐺 ∈ USGraph → ¬ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) ) )
55 54 com12 ⊢ ( 𝐺 ∈ USGraph → ( ¬ ( ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ∧ 𝑁 = 𝑁 ) ∨ ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = 𝑁 ∧ 𝑁 = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ) ) → ¬ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) ) )
56 55 adantr ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( ¬ ( ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ∧ 𝑁 = 𝑁 ) ∨ ( ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) = 𝑁 ∧ 𝑁 = ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) ) ) → ¬ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) ) )
57 42 56 sylbid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( ¬ { ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) , 𝑁 } = { ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) , 𝑁 } → ¬ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) ) )
58 57 adantr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ¬ { ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑢 , 𝑁 } ) , 𝑁 } = { ( ℩ 𝑢 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑢 , 𝑁 } ) , 𝑁 } → ¬ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) ) )
59 33 58 sylbid ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ¬ ( 𝐸 ‘ 𝑦 ) = ( 𝐸 ‘ 𝑤 ) → ¬ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) ) )
60 18 59 sylbid ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ¬ 𝑦 = 𝑤 → ¬ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) ) )
61 60 con4d ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) → 𝑦 = 𝑤 ) )
62 61 ralrimivva ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ∀ 𝑦 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) → 𝑦 = 𝑤 ) )
63 fveqeq2 ⊢ ( 𝑦 = 𝑤 → ( ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ↔ ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) )
64 63 riotabidv ⊢ ( 𝑦 = 𝑤 → ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) )
65 4 64 f1mpt ⊢ ( 𝐹 : 𝐴 –1-1→ 𝑉 ↔ ( ∀ 𝑦 ∈ 𝐴 ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑤 ) = { 𝑧 , 𝑁 } ) → 𝑦 = 𝑤 ) ) )
66 7 62 65 sylanbrc ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐹 : 𝐴 –1-1→ 𝑉 )