Step |
Hyp |
Ref |
Expression |
1 |
|
snstrvtxval.v |
⊢ 𝑉 ∈ V |
2 |
|
snstrvtxval.g |
⊢ 𝐺 = { 〈 ( Base ‘ ndx ) , 𝑉 〉 } |
3 |
|
iedgval |
⊢ ( iEdg ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) ) |
4 |
3
|
a1i |
⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ( iEdg ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) ) ) |
5 |
|
necom |
⊢ ( 𝑉 ≠ ( Base ‘ ndx ) ↔ ( Base ‘ ndx ) ≠ 𝑉 ) |
6 |
|
fvex |
⊢ ( Base ‘ ndx ) ∈ V |
7 |
6 1 2
|
funsndifnop |
⊢ ( ( Base ‘ ndx ) ≠ 𝑉 → ¬ 𝐺 ∈ ( V × V ) ) |
8 |
5 7
|
sylbi |
⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ¬ 𝐺 ∈ ( V × V ) ) |
9 |
8
|
iffalsed |
⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) ) = ( .ef ‘ 𝐺 ) ) |
10 |
|
snex |
⊢ { 〈 ( Base ‘ ndx ) , 𝑉 〉 } ∈ V |
11 |
10
|
a1i |
⊢ ( 𝐺 = { 〈 ( Base ‘ ndx ) , 𝑉 〉 } → { 〈 ( Base ‘ ndx ) , 𝑉 〉 } ∈ V ) |
12 |
2 11
|
eqeltrid |
⊢ ( 𝐺 = { 〈 ( Base ‘ ndx ) , 𝑉 〉 } → 𝐺 ∈ V ) |
13 |
|
edgfndxid |
⊢ ( 𝐺 ∈ V → ( .ef ‘ 𝐺 ) = ( 𝐺 ‘ ( .ef ‘ ndx ) ) ) |
14 |
2 12 13
|
mp2b |
⊢ ( .ef ‘ 𝐺 ) = ( 𝐺 ‘ ( .ef ‘ ndx ) ) |
15 |
|
slotsbaseefdif |
⊢ ( Base ‘ ndx ) ≠ ( .ef ‘ ndx ) |
16 |
15
|
nesymi |
⊢ ¬ ( .ef ‘ ndx ) = ( Base ‘ ndx ) |
17 |
16
|
a1i |
⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ¬ ( .ef ‘ ndx ) = ( Base ‘ ndx ) ) |
18 |
|
fvex |
⊢ ( .ef ‘ ndx ) ∈ V |
19 |
18
|
elsn |
⊢ ( ( .ef ‘ ndx ) ∈ { ( Base ‘ ndx ) } ↔ ( .ef ‘ ndx ) = ( Base ‘ ndx ) ) |
20 |
17 19
|
sylnibr |
⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ¬ ( .ef ‘ ndx ) ∈ { ( Base ‘ ndx ) } ) |
21 |
2
|
dmeqi |
⊢ dom 𝐺 = dom { 〈 ( Base ‘ ndx ) , 𝑉 〉 } |
22 |
|
dmsnopg |
⊢ ( 𝑉 ∈ V → dom { 〈 ( Base ‘ ndx ) , 𝑉 〉 } = { ( Base ‘ ndx ) } ) |
23 |
1 22
|
mp1i |
⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → dom { 〈 ( Base ‘ ndx ) , 𝑉 〉 } = { ( Base ‘ ndx ) } ) |
24 |
21 23
|
syl5eq |
⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → dom 𝐺 = { ( Base ‘ ndx ) } ) |
25 |
20 24
|
neleqtrrd |
⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ¬ ( .ef ‘ ndx ) ∈ dom 𝐺 ) |
26 |
|
ndmfv |
⊢ ( ¬ ( .ef ‘ ndx ) ∈ dom 𝐺 → ( 𝐺 ‘ ( .ef ‘ ndx ) ) = ∅ ) |
27 |
25 26
|
syl |
⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ( 𝐺 ‘ ( .ef ‘ ndx ) ) = ∅ ) |
28 |
14 27
|
syl5eq |
⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ( .ef ‘ 𝐺 ) = ∅ ) |
29 |
4 9 28
|
3eqtrd |
⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ( iEdg ‘ 𝐺 ) = ∅ ) |