Metamath Proof Explorer

Theorem edglnl

Description: The edges incident with a vertex N are the edges joining N with other vertices and the loops on N in a pseudograph. (Contributed by AV, 18-Dec-2021)

Ref Expression
Hypotheses edglnl.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
edglnl.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion edglnl ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∪ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } )

Proof

Step Hyp Ref Expression
1 edglnl.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 edglnl.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3 iunrab ⊢ ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } = { 𝑖 ∈ dom 𝐸 ∣ ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) }
4 3 a1i ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } = { 𝑖 ∈ dom 𝐸 ∣ ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } )
5 4 uneq1d ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∪ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) = ( { 𝑖 ∈ dom 𝐸 ∣ ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∪ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) )
6 unrab ⊢ ( { 𝑖 ∈ dom 𝐸 ∣ ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∪ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) = { 𝑖 ∈ dom 𝐸 ∣ ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∨ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } ) }
7 simpl ⊢ ( ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) → 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) )
8 7 rexlimivw ⊢ ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) → 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) )
9 8 a1i ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑖 ∈ dom 𝐸 ) → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) → 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ) )
10 snidg ⊢ ( 𝑁 ∈ 𝑉 → 𝑁 ∈ { 𝑁 } )
11 10 ad2antlr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑖 ∈ dom 𝐸 ) → 𝑁 ∈ { 𝑁 } )
12 eleq2 ⊢ ( ( 𝐸 ‘ 𝑖 ) = { 𝑁 } → ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ↔ 𝑁 ∈ { 𝑁 } ) )
13 11 12 syl5ibrcom ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑖 ∈ dom 𝐸 ) → ( ( 𝐸 ‘ 𝑖 ) = { 𝑁 } → 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ) )
14 9 13 jaod ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑖 ∈ dom 𝐸 ) → ( ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∨ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } ) → 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ) )
15 upgruhgr ⊢ ( 𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph )
16 2 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun 𝐸 )
17 15 16 syl ⊢ ( 𝐺 ∈ UPGraph → Fun 𝐸 )
18 17 adantr ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → Fun 𝐸 )
19 2 iedgedg ⊢ ( ( Fun 𝐸 ∧ 𝑖 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑖 ) ∈ ( Edg ‘ 𝐺 ) )
20 18 19 sylan ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑖 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑖 ) ∈ ( Edg ‘ 𝐺 ) )
21 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
22 1 21 upgredg ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝐸 ‘ 𝑖 ) ∈ ( Edg ‘ 𝐺 ) ) → ∃ 𝑛 ∈ 𝑉 ∃ 𝑚 ∈ 𝑉 ( 𝐸 ‘ 𝑖 ) = { 𝑛 , 𝑚 } )
23 22 ex ⊢ ( 𝐺 ∈ UPGraph → ( ( 𝐸 ‘ 𝑖 ) ∈ ( Edg ‘ 𝐺 ) → ∃ 𝑛 ∈ 𝑉 ∃ 𝑚 ∈ 𝑉 ( 𝐸 ‘ 𝑖 ) = { 𝑛 , 𝑚 } ) )
24 23 ad2antrr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑖 ∈ dom 𝐸 ) → ( ( 𝐸 ‘ 𝑖 ) ∈ ( Edg ‘ 𝐺 ) → ∃ 𝑛 ∈ 𝑉 ∃ 𝑚 ∈ 𝑉 ( 𝐸 ‘ 𝑖 ) = { 𝑛 , 𝑚 } ) )
25 dfsn2 ⊢ { 𝑛 } = { 𝑛 , 𝑛 }
26 25 eqcomi ⊢ { 𝑛 , 𝑛 } = { 𝑛 }
27 elsni ⊢ ( 𝑁 ∈ { 𝑛 } → 𝑁 = 𝑛 )
28 sneq ⊢ ( 𝑁 = 𝑛 → { 𝑁 } = { 𝑛 } )
29 28 eqcomd ⊢ ( 𝑁 = 𝑛 → { 𝑛 } = { 𝑁 } )
30 27 29 syl ⊢ ( 𝑁 ∈ { 𝑛 } → { 𝑛 } = { 𝑁 } )
31 26 30 syl5eq ⊢ ( 𝑁 ∈ { 𝑛 } → { 𝑛 , 𝑛 } = { 𝑁 } )
32 31 26 eleq2s ⊢ ( 𝑁 ∈ { 𝑛 , 𝑛 } → { 𝑛 , 𝑛 } = { 𝑁 } )
33 preq2 ⊢ ( 𝑚 = 𝑛 → { 𝑛 , 𝑚 } = { 𝑛 , 𝑛 } )
34 33 eleq2d ⊢ ( 𝑚 = 𝑛 → ( 𝑁 ∈ { 𝑛 , 𝑚 } ↔ 𝑁 ∈ { 𝑛 , 𝑛 } ) )
35 33 eqeq1d ⊢ ( 𝑚 = 𝑛 → ( { 𝑛 , 𝑚 } = { 𝑁 } ↔ { 𝑛 , 𝑛 } = { 𝑁 } ) )
36 34 35 imbi12d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑁 ∈ { 𝑛 , 𝑚 } → { 𝑛 , 𝑚 } = { 𝑁 } ) ↔ ( 𝑁 ∈ { 𝑛 , 𝑛 } → { 𝑛 , 𝑛 } = { 𝑁 } ) ) )
37 32 36 mpbiri ⊢ ( 𝑚 = 𝑛 → ( 𝑁 ∈ { 𝑛 , 𝑚 } → { 𝑛 , 𝑚 } = { 𝑁 } ) )
38 37 imp ⊢ ( ( 𝑚 = 𝑛 ∧ 𝑁 ∈ { 𝑛 , 𝑚 } ) → { 𝑛 , 𝑚 } = { 𝑁 } )
39 38 olcd ⊢ ( ( 𝑚 = 𝑛 ∧ 𝑁 ∈ { 𝑛 , 𝑚 } ) → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ { 𝑛 , 𝑚 } ∧ 𝑣 ∈ { 𝑛 , 𝑚 } ) ∨ { 𝑛 , 𝑚 } = { 𝑁 } ) )
40 39 expcom ⊢ ( 𝑁 ∈ { 𝑛 , 𝑚 } → ( 𝑚 = 𝑛 → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ { 𝑛 , 𝑚 } ∧ 𝑣 ∈ { 𝑛 , 𝑚 } ) ∨ { 𝑛 , 𝑚 } = { 𝑁 } ) ) )
41 40 3ad2ant3 ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ) ∧ 𝑁 ∈ { 𝑛 , 𝑚 } ) → ( 𝑚 = 𝑛 → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ { 𝑛 , 𝑚 } ∧ 𝑣 ∈ { 𝑛 , 𝑚 } ) ∨ { 𝑛 , 𝑚 } = { 𝑁 } ) ) )
42 41 com12 ⊢ ( 𝑚 = 𝑛 → ( ( 𝑁 ∈ 𝑉 ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ) ∧ 𝑁 ∈ { 𝑛 , 𝑚 } ) → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ { 𝑛 , 𝑚 } ∧ 𝑣 ∈ { 𝑛 , 𝑚 } ) ∨ { 𝑛 , 𝑚 } = { 𝑁 } ) ) )
43 simpr3 ⊢ ( ( 𝑚 ≠ 𝑛 ∧ ( 𝑁 ∈ 𝑉 ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ) ∧ 𝑁 ∈ { 𝑛 , 𝑚 } ) ) → 𝑁 ∈ { 𝑛 , 𝑚 } )
44 simpl ⊢ ( ( 𝑚 ≠ 𝑛 ∧ ( 𝑁 ∈ 𝑉 ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ) ∧ 𝑁 ∈ { 𝑛 , 𝑚 } ) ) → 𝑚 ≠ 𝑛 )
45 44 necomd ⊢ ( ( 𝑚 ≠ 𝑛 ∧ ( 𝑁 ∈ 𝑉 ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ) ∧ 𝑁 ∈ { 𝑛 , 𝑚 } ) ) → 𝑛 ≠ 𝑚 )
46 simpr2 ⊢ ( ( 𝑚 ≠ 𝑛 ∧ ( 𝑁 ∈ 𝑉 ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ) ∧ 𝑁 ∈ { 𝑛 , 𝑚 } ) ) → ( 𝑛 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ) )
47 prproe ⊢ ( ( 𝑁 ∈ { 𝑛 , 𝑚 } ∧ 𝑛 ≠ 𝑚 ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ) ) → ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑣 ∈ { 𝑛 , 𝑚 } )
48 43 45 46 47 syl3anc ⊢ ( ( 𝑚 ≠ 𝑛 ∧ ( 𝑁 ∈ 𝑉 ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ) ∧ 𝑁 ∈ { 𝑛 , 𝑚 } ) ) → ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑣 ∈ { 𝑛 , 𝑚 } )
49 r19.42v ⊢ ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ { 𝑛 , 𝑚 } ∧ 𝑣 ∈ { 𝑛 , 𝑚 } ) ↔ ( 𝑁 ∈ { 𝑛 , 𝑚 } ∧ ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑣 ∈ { 𝑛 , 𝑚 } ) )
50 43 48 49 sylanbrc ⊢ ( ( 𝑚 ≠ 𝑛 ∧ ( 𝑁 ∈ 𝑉 ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ) ∧ 𝑁 ∈ { 𝑛 , 𝑚 } ) ) → ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ { 𝑛 , 𝑚 } ∧ 𝑣 ∈ { 𝑛 , 𝑚 } ) )
51 50 orcd ⊢ ( ( 𝑚 ≠ 𝑛 ∧ ( 𝑁 ∈ 𝑉 ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ) ∧ 𝑁 ∈ { 𝑛 , 𝑚 } ) ) → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ { 𝑛 , 𝑚 } ∧ 𝑣 ∈ { 𝑛 , 𝑚 } ) ∨ { 𝑛 , 𝑚 } = { 𝑁 } ) )
52 51 ex ⊢ ( 𝑚 ≠ 𝑛 → ( ( 𝑁 ∈ 𝑉 ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ) ∧ 𝑁 ∈ { 𝑛 , 𝑚 } ) → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ { 𝑛 , 𝑚 } ∧ 𝑣 ∈ { 𝑛 , 𝑚 } ) ∨ { 𝑛 , 𝑚 } = { 𝑁 } ) ) )
53 42 52 pm2.61ine ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ) ∧ 𝑁 ∈ { 𝑛 , 𝑚 } ) → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ { 𝑛 , 𝑚 } ∧ 𝑣 ∈ { 𝑛 , 𝑚 } ) ∨ { 𝑛 , 𝑚 } = { 𝑁 } ) )
54 53 3exp ⊢ ( 𝑁 ∈ 𝑉 → ( ( 𝑛 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ) → ( 𝑁 ∈ { 𝑛 , 𝑚 } → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ { 𝑛 , 𝑚 } ∧ 𝑣 ∈ { 𝑛 , 𝑚 } ) ∨ { 𝑛 , 𝑚 } = { 𝑁 } ) ) ) )
55 54 ad2antlr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑖 ∈ dom 𝐸 ) → ( ( 𝑛 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ) → ( 𝑁 ∈ { 𝑛 , 𝑚 } → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ { 𝑛 , 𝑚 } ∧ 𝑣 ∈ { 𝑛 , 𝑚 } ) ∨ { 𝑛 , 𝑚 } = { 𝑁 } ) ) ) )
56 55 imp ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑖 ∈ dom 𝐸 ) ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ) ) → ( 𝑁 ∈ { 𝑛 , 𝑚 } → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ { 𝑛 , 𝑚 } ∧ 𝑣 ∈ { 𝑛 , 𝑚 } ) ∨ { 𝑛 , 𝑚 } = { 𝑁 } ) ) )
57 eleq2 ⊢ ( ( 𝐸 ‘ 𝑖 ) = { 𝑛 , 𝑚 } → ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ↔ 𝑁 ∈ { 𝑛 , 𝑚 } ) )
58 eleq2 ⊢ ( ( 𝐸 ‘ 𝑖 ) = { 𝑛 , 𝑚 } → ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ↔ 𝑣 ∈ { 𝑛 , 𝑚 } ) )
59 57 58 anbi12d ⊢ ( ( 𝐸 ‘ 𝑖 ) = { 𝑛 , 𝑚 } → ( ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ↔ ( 𝑁 ∈ { 𝑛 , 𝑚 } ∧ 𝑣 ∈ { 𝑛 , 𝑚 } ) ) )
60 59 rexbidv ⊢ ( ( 𝐸 ‘ 𝑖 ) = { 𝑛 , 𝑚 } → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ↔ ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ { 𝑛 , 𝑚 } ∧ 𝑣 ∈ { 𝑛 , 𝑚 } ) ) )
61 eqeq1 ⊢ ( ( 𝐸 ‘ 𝑖 ) = { 𝑛 , 𝑚 } → ( ( 𝐸 ‘ 𝑖 ) = { 𝑁 } ↔ { 𝑛 , 𝑚 } = { 𝑁 } ) )
62 60 61 orbi12d ⊢ ( ( 𝐸 ‘ 𝑖 ) = { 𝑛 , 𝑚 } → ( ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∨ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } ) ↔ ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ { 𝑛 , 𝑚 } ∧ 𝑣 ∈ { 𝑛 , 𝑚 } ) ∨ { 𝑛 , 𝑚 } = { 𝑁 } ) ) )
63 57 62 imbi12d ⊢ ( ( 𝐸 ‘ 𝑖 ) = { 𝑛 , 𝑚 } → ( ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∨ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } ) ) ↔ ( 𝑁 ∈ { 𝑛 , 𝑚 } → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ { 𝑛 , 𝑚 } ∧ 𝑣 ∈ { 𝑛 , 𝑚 } ) ∨ { 𝑛 , 𝑚 } = { 𝑁 } ) ) ) )
64 56 63 syl5ibrcom ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑖 ∈ dom 𝐸 ) ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ) ) → ( ( 𝐸 ‘ 𝑖 ) = { 𝑛 , 𝑚 } → ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∨ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } ) ) ) )
65 64 rexlimdvva ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑖 ∈ dom 𝐸 ) → ( ∃ 𝑛 ∈ 𝑉 ∃ 𝑚 ∈ 𝑉 ( 𝐸 ‘ 𝑖 ) = { 𝑛 , 𝑚 } → ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∨ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } ) ) ) )
66 24 65 syld ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑖 ∈ dom 𝐸 ) → ( ( 𝐸 ‘ 𝑖 ) ∈ ( Edg ‘ 𝐺 ) → ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∨ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } ) ) ) )
67 20 66 mpd ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑖 ∈ dom 𝐸 ) → ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∨ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } ) ) )
68 14 67 impbid ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑖 ∈ dom 𝐸 ) → ( ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∨ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } ) ↔ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ) )
69 68 rabbidva ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → { 𝑖 ∈ dom 𝐸 ∣ ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∨ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } ) } = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } )
70 6 69 syl5eq ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( { 𝑖 ∈ dom 𝐸 ∣ ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∪ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } )
71 5 70 eqtrd ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∪ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } )