Metamath Proof Explorer

Theorem numedglnl

Description: The number of edges incident with a vertex N is the number of edges joining N with other vertices and the number of loops on N in a pseudograph of finite size. (Contributed by AV, 19-Dec-2021)

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

Proof

Step Hyp Ref Expression
1 edglnl.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 edglnl.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3 diffi ⊢ ( 𝑉 ∈ Fin → ( 𝑉 ∖ { 𝑁 } ) ∈ Fin )
4 3 adantr ⊢ ( ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) → ( 𝑉 ∖ { 𝑁 } ) ∈ Fin )
5 4 3ad2ant2 ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → ( 𝑉 ∖ { 𝑁 } ) ∈ Fin )
6 dmfi ⊢ ( 𝐸 ∈ Fin → dom 𝐸 ∈ Fin )
7 rabfi ⊢ ( dom 𝐸 ∈ Fin → { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∈ Fin )
8 6 7 syl ⊢ ( 𝐸 ∈ Fin → { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∈ Fin )
9 8 adantl ⊢ ( ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) → { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∈ Fin )
10 9 3ad2ant2 ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∈ Fin )
11 10 adantr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∈ Fin )
12 notnotb ⊢ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ↔ ¬ ¬ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) )
13 notnotb ⊢ ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ↔ ¬ ¬ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) )
14 upgruhgr ⊢ ( 𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph )
15 2 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun 𝐸 )
16 14 15 syl ⊢ ( 𝐺 ∈ UPGraph → Fun 𝐸 )
17 2 iedgedg ⊢ ( ( Fun 𝐸 ∧ 𝑖 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑖 ) ∈ ( Edg ‘ 𝐺 ) )
18 16 17 sylan ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑖 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑖 ) ∈ ( Edg ‘ 𝐺 ) )
19 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
20 1 19 upgredg ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝐸 ‘ 𝑖 ) ∈ ( Edg ‘ 𝐺 ) ) → ∃ 𝑚 ∈ 𝑉 ∃ 𝑛 ∈ 𝑉 ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } )
21 18 20 syldan ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑖 ∈ dom 𝐸 ) → ∃ 𝑚 ∈ 𝑉 ∃ 𝑛 ∈ 𝑉 ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } )
22 21 ex ⊢ ( 𝐺 ∈ UPGraph → ( 𝑖 ∈ dom 𝐸 → ∃ 𝑚 ∈ 𝑉 ∃ 𝑛 ∈ 𝑉 ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } ) )
23 22 3ad2ant1 ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → ( 𝑖 ∈ dom 𝐸 → ∃ 𝑚 ∈ 𝑉 ∃ 𝑛 ∈ 𝑉 ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } ) )
24 23 adantr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ) → ( 𝑖 ∈ dom 𝐸 → ∃ 𝑚 ∈ 𝑉 ∃ 𝑛 ∈ 𝑉 ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } ) )
25 24 adantr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ) ∧ ¬ 𝑣 = 𝑤 ) → ( 𝑖 ∈ dom 𝐸 → ∃ 𝑚 ∈ 𝑉 ∃ 𝑛 ∈ 𝑉 ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } ) )
26 25 imp ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ) ∧ ¬ 𝑣 = 𝑤 ) ∧ 𝑖 ∈ dom 𝐸 ) → ∃ 𝑚 ∈ 𝑉 ∃ 𝑛 ∈ 𝑉 ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } )
27 eldifsni ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → 𝑣 ≠ 𝑁 )
28 eldifsni ⊢ ( 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) → 𝑤 ≠ 𝑁 )
29 3elpr2eq ⊢ ( ( ( 𝑁 ∈ { 𝑚 , 𝑛 } ∧ 𝑣 ∈ { 𝑚 , 𝑛 } ∧ 𝑤 ∈ { 𝑚 , 𝑛 } ) ∧ ( 𝑣 ≠ 𝑁 ∧ 𝑤 ≠ 𝑁 ) ) → 𝑣 = 𝑤 )
30 29 expcom ⊢ ( ( 𝑣 ≠ 𝑁 ∧ 𝑤 ≠ 𝑁 ) → ( ( 𝑁 ∈ { 𝑚 , 𝑛 } ∧ 𝑣 ∈ { 𝑚 , 𝑛 } ∧ 𝑤 ∈ { 𝑚 , 𝑛 } ) → 𝑣 = 𝑤 ) )
31 30 3expd ⊢ ( ( 𝑣 ≠ 𝑁 ∧ 𝑤 ≠ 𝑁 ) → ( 𝑁 ∈ { 𝑚 , 𝑛 } → ( 𝑣 ∈ { 𝑚 , 𝑛 } → ( 𝑤 ∈ { 𝑚 , 𝑛 } → 𝑣 = 𝑤 ) ) ) )
32 31 com23 ⊢ ( ( 𝑣 ≠ 𝑁 ∧ 𝑤 ≠ 𝑁 ) → ( 𝑣 ∈ { 𝑚 , 𝑛 } → ( 𝑁 ∈ { 𝑚 , 𝑛 } → ( 𝑤 ∈ { 𝑚 , 𝑛 } → 𝑣 = 𝑤 ) ) ) )
33 32 3imp ⊢ ( ( ( 𝑣 ≠ 𝑁 ∧ 𝑤 ≠ 𝑁 ) ∧ 𝑣 ∈ { 𝑚 , 𝑛 } ∧ 𝑁 ∈ { 𝑚 , 𝑛 } ) → ( 𝑤 ∈ { 𝑚 , 𝑛 } → 𝑣 = 𝑤 ) )
34 33 con3d ⊢ ( ( ( 𝑣 ≠ 𝑁 ∧ 𝑤 ≠ 𝑁 ) ∧ 𝑣 ∈ { 𝑚 , 𝑛 } ∧ 𝑁 ∈ { 𝑚 , 𝑛 } ) → ( ¬ 𝑣 = 𝑤 → ¬ 𝑤 ∈ { 𝑚 , 𝑛 } ) )
35 34 3exp ⊢ ( ( 𝑣 ≠ 𝑁 ∧ 𝑤 ≠ 𝑁 ) → ( 𝑣 ∈ { 𝑚 , 𝑛 } → ( 𝑁 ∈ { 𝑚 , 𝑛 } → ( ¬ 𝑣 = 𝑤 → ¬ 𝑤 ∈ { 𝑚 , 𝑛 } ) ) ) )
36 35 com24 ⊢ ( ( 𝑣 ≠ 𝑁 ∧ 𝑤 ≠ 𝑁 ) → ( ¬ 𝑣 = 𝑤 → ( 𝑁 ∈ { 𝑚 , 𝑛 } → ( 𝑣 ∈ { 𝑚 , 𝑛 } → ¬ 𝑤 ∈ { 𝑚 , 𝑛 } ) ) ) )
37 36 imp ⊢ ( ( ( 𝑣 ≠ 𝑁 ∧ 𝑤 ≠ 𝑁 ) ∧ ¬ 𝑣 = 𝑤 ) → ( 𝑁 ∈ { 𝑚 , 𝑛 } → ( 𝑣 ∈ { 𝑚 , 𝑛 } → ¬ 𝑤 ∈ { 𝑚 , 𝑛 } ) ) )
38 eleq2 ⊢ ( ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } → ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ↔ 𝑁 ∈ { 𝑚 , 𝑛 } ) )
39 eleq2 ⊢ ( ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } → ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ↔ 𝑣 ∈ { 𝑚 , 𝑛 } ) )
40 eleq2 ⊢ ( ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } → ( 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ↔ 𝑤 ∈ { 𝑚 , 𝑛 } ) )
41 40 notbid ⊢ ( ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } → ( ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ↔ ¬ 𝑤 ∈ { 𝑚 , 𝑛 } ) )
42 39 41 imbi12d ⊢ ( ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } → ( ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) → ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ↔ ( 𝑣 ∈ { 𝑚 , 𝑛 } → ¬ 𝑤 ∈ { 𝑚 , 𝑛 } ) ) )
43 38 42 imbi12d ⊢ ( ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } → ( ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) → ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) → ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ↔ ( 𝑁 ∈ { 𝑚 , 𝑛 } → ( 𝑣 ∈ { 𝑚 , 𝑛 } → ¬ 𝑤 ∈ { 𝑚 , 𝑛 } ) ) ) )
44 37 43 syl5ibrcom ⊢ ( ( ( 𝑣 ≠ 𝑁 ∧ 𝑤 ≠ 𝑁 ) ∧ ¬ 𝑣 = 𝑤 ) → ( ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } → ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) → ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) → ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ) )
45 44 adantr ⊢ ( ( ( ( 𝑣 ≠ 𝑁 ∧ 𝑤 ≠ 𝑁 ) ∧ ¬ 𝑣 = 𝑤 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → ( ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } → ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) → ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) → ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ) )
46 45 rexlimdvva ⊢ ( ( ( 𝑣 ≠ 𝑁 ∧ 𝑤 ≠ 𝑁 ) ∧ ¬ 𝑣 = 𝑤 ) → ( ∃ 𝑚 ∈ 𝑉 ∃ 𝑛 ∈ 𝑉 ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } → ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) → ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) → ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ) )
47 46 ex ⊢ ( ( 𝑣 ≠ 𝑁 ∧ 𝑤 ≠ 𝑁 ) → ( ¬ 𝑣 = 𝑤 → ( ∃ 𝑚 ∈ 𝑉 ∃ 𝑛 ∈ 𝑉 ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } → ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) → ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) → ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ) ) )
48 27 28 47 syl2an ⊢ ( ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ¬ 𝑣 = 𝑤 → ( ∃ 𝑚 ∈ 𝑉 ∃ 𝑛 ∈ 𝑉 ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } → ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) → ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) → ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ) ) )
49 48 adantl ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ) → ( ¬ 𝑣 = 𝑤 → ( ∃ 𝑚 ∈ 𝑉 ∃ 𝑛 ∈ 𝑉 ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } → ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) → ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) → ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ) ) )
50 49 imp ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ) ∧ ¬ 𝑣 = 𝑤 ) → ( ∃ 𝑚 ∈ 𝑉 ∃ 𝑛 ∈ 𝑉 ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } → ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) → ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) → ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ) )
51 50 adantr ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ) ∧ ¬ 𝑣 = 𝑤 ) ∧ 𝑖 ∈ dom 𝐸 ) → ( ∃ 𝑚 ∈ 𝑉 ∃ 𝑛 ∈ 𝑉 ( 𝐸 ‘ 𝑖 ) = { 𝑚 , 𝑛 } → ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) → ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) → ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ) )
52 26 51 mpd ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ) ∧ ¬ 𝑣 = 𝑤 ) ∧ 𝑖 ∈ dom 𝐸 ) → ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) → ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) → ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) )
53 52 imp ⊢ ( ( ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ) ∧ ¬ 𝑣 = 𝑤 ) ∧ 𝑖 ∈ dom 𝐸 ) ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ) → ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) → ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) )
54 13 53 biimtrrid ⊢ ( ( ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ) ∧ ¬ 𝑣 = 𝑤 ) ∧ 𝑖 ∈ dom 𝐸 ) ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ) → ( ¬ ¬ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) → ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) )
55 54 orrd ⊢ ( ( ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ) ∧ ¬ 𝑣 = 𝑤 ) ∧ 𝑖 ∈ dom 𝐸 ) ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ) → ( ¬ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ∨ ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) )
56 55 ex ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ) ∧ ¬ 𝑣 = 𝑤 ) ∧ 𝑖 ∈ dom 𝐸 ) → ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) → ( ¬ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ∨ ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) )
57 12 56 biimtrrid ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ) ∧ ¬ 𝑣 = 𝑤 ) ∧ 𝑖 ∈ dom 𝐸 ) → ( ¬ ¬ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) → ( ¬ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ∨ ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) )
58 57 orrd ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ) ∧ ¬ 𝑣 = 𝑤 ) ∧ 𝑖 ∈ dom 𝐸 ) → ( ¬ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∨ ( ¬ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ∨ ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) )
59 anandi ⊢ ( ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ↔ ( ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) )
60 59 bicomi ⊢ ( ( ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ↔ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) )
61 60 notbii ⊢ ( ¬ ( ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ↔ ¬ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) )
62 ianor ⊢ ( ¬ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ↔ ( ¬ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∨ ¬ ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) )
63 ianor ⊢ ( ¬ ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ↔ ( ¬ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ∨ ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) )
64 63 orbi2i ⊢ ( ( ¬ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∨ ¬ ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ↔ ( ¬ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∨ ( ¬ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ∨ ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) )
65 61 62 64 3bitri ⊢ ( ¬ ( ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ↔ ( ¬ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∨ ( ¬ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ∨ ¬ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) )
66 58 65 sylibr ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ) ∧ ¬ 𝑣 = 𝑤 ) ∧ 𝑖 ∈ dom 𝐸 ) → ¬ ( ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) )
67 66 ralrimiva ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ) ∧ ¬ 𝑣 = 𝑤 ) → ∀ 𝑖 ∈ dom 𝐸 ¬ ( ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) )
68 inrab ⊢ ( { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∩ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) = { 𝑖 ∈ dom 𝐸 ∣ ( ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) }
69 68 eqeq1i ⊢ ( ( { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∩ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) = ∅ ↔ { 𝑖 ∈ dom 𝐸 ∣ ( ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) } = ∅ )
70 rabeq0 ⊢ ( { 𝑖 ∈ dom 𝐸 ∣ ( ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) } = ∅ ↔ ∀ 𝑖 ∈ dom 𝐸 ¬ ( ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) )
71 69 70 bitri ⊢ ( ( { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∩ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) = ∅ ↔ ∀ 𝑖 ∈ dom 𝐸 ¬ ( ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) )
72 67 71 sylibr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ) ∧ ¬ 𝑣 = 𝑤 ) → ( { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∩ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) = ∅ )
73 72 ex ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ) → ( ¬ 𝑣 = 𝑤 → ( { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∩ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) = ∅ ) )
74 73 orrd ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ) → ( 𝑣 = 𝑤 ∨ ( { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∩ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) = ∅ ) )
75 74 ralrimivva ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑣 = 𝑤 ∨ ( { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∩ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) = ∅ ) )
76 eleq1w ⊢ ( 𝑣 = 𝑤 → ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ↔ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) )
77 76 anbi2d ⊢ ( 𝑣 = 𝑤 → ( ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ↔ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) ) )
78 77 rabbidv ⊢ ( 𝑣 = 𝑤 → { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } = { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) } )
79 78 disjor ⊢ ( Disj 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ↔ ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑁 } ) ( 𝑣 = 𝑤 ∨ ( { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∩ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑤 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) = ∅ ) )
80 75 79 sylibr ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → Disj 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } )
81 5 11 80 hashiun ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → ( ♯ ‘ ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) = Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) )
82 81 eqcomd ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) = ( ♯ ‘ ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) )
83 82 oveq1d ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) = ( ( ♯ ‘ ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) )
84 11 ralrimiva ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∈ Fin )
85 iunfi ⊢ ( ( ( 𝑉 ∖ { 𝑁 } ) ∈ Fin ∧ ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∈ Fin ) → ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∈ Fin )
86 5 84 85 syl2anc ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∈ Fin )
87 rabfi ⊢ ( dom 𝐸 ∈ Fin → { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ∈ Fin )
88 6 87 syl ⊢ ( 𝐸 ∈ Fin → { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ∈ Fin )
89 88 adantl ⊢ ( ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) → { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ∈ Fin )
90 89 3ad2ant2 ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ∈ Fin )
91 fveqeq2 ⊢ ( 𝑖 = 𝑗 → ( ( 𝐸 ‘ 𝑖 ) = { 𝑁 } ↔ ( 𝐸 ‘ 𝑗 ) = { 𝑁 } ) )
92 91 elrab ⊢ ( 𝑗 ∈ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ↔ ( 𝑗 ∈ dom 𝐸 ∧ ( 𝐸 ‘ 𝑗 ) = { 𝑁 } ) )
93 eldifn ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ¬ 𝑣 ∈ { 𝑁 } )
94 eleq2 ⊢ ( ( 𝐸 ‘ 𝑗 ) = { 𝑁 } → ( 𝑣 ∈ ( 𝐸 ‘ 𝑗 ) ↔ 𝑣 ∈ { 𝑁 } ) )
95 94 notbid ⊢ ( ( 𝐸 ‘ 𝑗 ) = { 𝑁 } → ( ¬ 𝑣 ∈ ( 𝐸 ‘ 𝑗 ) ↔ ¬ 𝑣 ∈ { 𝑁 } ) )
96 93 95 imbitrrid ⊢ ( ( 𝐸 ‘ 𝑗 ) = { 𝑁 } → ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ¬ 𝑣 ∈ ( 𝐸 ‘ 𝑗 ) ) )
97 96 adantl ⊢ ( ( 𝑗 ∈ dom 𝐸 ∧ ( 𝐸 ‘ 𝑗 ) = { 𝑁 } ) → ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ¬ 𝑣 ∈ ( 𝐸 ‘ 𝑗 ) ) )
98 97 adantl ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑗 ∈ dom 𝐸 ∧ ( 𝐸 ‘ 𝑗 ) = { 𝑁 } ) ) → ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ¬ 𝑣 ∈ ( 𝐸 ‘ 𝑗 ) ) )
99 98 imp ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑗 ∈ dom 𝐸 ∧ ( 𝐸 ‘ 𝑗 ) = { 𝑁 } ) ) ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ¬ 𝑣 ∈ ( 𝐸 ‘ 𝑗 ) )
100 99 intnand ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑗 ∈ dom 𝐸 ∧ ( 𝐸 ‘ 𝑗 ) = { 𝑁 } ) ) ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ¬ ( 𝑁 ∈ ( 𝐸 ‘ 𝑗 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑗 ) ) )
101 100 intnand ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑗 ∈ dom 𝐸 ∧ ( 𝐸 ‘ 𝑗 ) = { 𝑁 } ) ) ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ¬ ( 𝑗 ∈ dom 𝐸 ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑗 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑗 ) ) ) )
102 101 ralrimiva ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑗 ∈ dom 𝐸 ∧ ( 𝐸 ‘ 𝑗 ) = { 𝑁 } ) ) → ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ¬ ( 𝑗 ∈ dom 𝐸 ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑗 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑗 ) ) ) )
103 eliun ⊢ ( 𝑗 ∈ ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ↔ ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑗 ∈ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } )
104 103 notbii ⊢ ( ¬ 𝑗 ∈ ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ↔ ¬ ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑗 ∈ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } )
105 ralnex ⊢ ( ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ¬ 𝑗 ∈ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ↔ ¬ ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑗 ∈ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } )
106 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐸 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑗 ) )
107 106 eleq2d ⊢ ( 𝑖 = 𝑗 → ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ↔ 𝑁 ∈ ( 𝐸 ‘ 𝑗 ) ) )
108 106 eleq2d ⊢ ( 𝑖 = 𝑗 → ( 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ↔ 𝑣 ∈ ( 𝐸 ‘ 𝑗 ) ) )
109 107 108 anbi12d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ↔ ( 𝑁 ∈ ( 𝐸 ‘ 𝑗 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑗 ) ) ) )
110 109 elrab ⊢ ( 𝑗 ∈ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ↔ ( 𝑗 ∈ dom 𝐸 ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑗 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑗 ) ) ) )
111 110 notbii ⊢ ( ¬ 𝑗 ∈ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ↔ ¬ ( 𝑗 ∈ dom 𝐸 ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑗 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑗 ) ) ) )
112 111 ralbii ⊢ ( ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ¬ 𝑗 ∈ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ↔ ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ¬ ( 𝑗 ∈ dom 𝐸 ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑗 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑗 ) ) ) )
113 104 105 112 3bitr2i ⊢ ( ¬ 𝑗 ∈ ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ↔ ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ¬ ( 𝑗 ∈ dom 𝐸 ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑗 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑗 ) ) ) )
114 102 113 sylibr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑗 ∈ dom 𝐸 ∧ ( 𝐸 ‘ 𝑗 ) = { 𝑁 } ) ) → ¬ 𝑗 ∈ ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } )
115 114 ex ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑗 ∈ dom 𝐸 ∧ ( 𝐸 ‘ 𝑗 ) = { 𝑁 } ) → ¬ 𝑗 ∈ ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) )
116 92 115 biimtrid ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → ( 𝑗 ∈ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } → ¬ 𝑗 ∈ ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) )
117 116 ralrimiv ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → ∀ 𝑗 ∈ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ¬ 𝑗 ∈ ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } )
118 disjr ⊢ ( ( ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∩ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) = ∅ ↔ ∀ 𝑗 ∈ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ¬ 𝑗 ∈ ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } )
119 117 118 sylibr ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → ( ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∩ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) = ∅ )
120 hashun ⊢ ( ( ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∈ Fin ∧ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ∈ Fin ∧ ( ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∩ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) = ∅ ) → ( ♯ ‘ ( ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∪ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) = ( ( ♯ ‘ ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) )
121 86 90 119 120 syl3anc ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → ( ♯ ‘ ( ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∪ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) = ( ( ♯ ‘ ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) )
122 1 2 edglnl ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∪ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } )
123 122 3adant2 ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → ( ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∪ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } )
124 123 fveq2d ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → ( ♯ ‘ ( ∪ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ∪ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) = ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) )
125 83 121 124 3eqtr2d ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) = ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) )