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