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 𝐸𝑁 ∈ ( 𝐸𝑖 ) } )