Proof of Theorem structiedg0val
Step | Hyp | Ref
| Expression |
1 | | structvtxvallem.s |
. . . . . 6
⊢ 𝑆 ∈ ℕ |
2 | | structvtxvallem.b |
. . . . . 6
⊢
(Base‘ndx) < 𝑆 |
3 | | structvtxvallem.g |
. . . . . 6
⊢ 𝐺 = {〈(Base‘ndx),
𝑉〉, 〈𝑆, 𝐸〉} |
4 | 1, 2, 3 | structvtxvallem 25697 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐺 ∈ V ∧ Fun 𝐺 ∧ {(Base‘ndx), 𝑆} ⊆ dom 𝐺)) |
5 | 4 | 3adant3 1074 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) → (𝐺 ∈ V ∧ Fun 𝐺 ∧ {(Base‘ndx), 𝑆} ⊆ dom 𝐺)) |
6 | | fundif 5849 |
. . . . . . . 8
⊢ (Fun
𝐺 → Fun (𝐺 ∖
{∅})) |
7 | 6 | anim2i 591 |
. . . . . . 7
⊢ ((𝐺 ∈ V ∧ Fun 𝐺) → (𝐺 ∈ V ∧ Fun (𝐺 ∖ {∅}))) |
8 | 7 | 3adant3 1074 |
. . . . . 6
⊢ ((𝐺 ∈ V ∧ Fun 𝐺 ∧ {(Base‘ndx), 𝑆} ⊆ dom 𝐺) → (𝐺 ∈ V ∧ Fun (𝐺 ∖ {∅}))) |
9 | 8 | adantl 481 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) ∧ (𝐺 ∈ V ∧ Fun 𝐺 ∧ {(Base‘ndx), 𝑆} ⊆ dom 𝐺)) → (𝐺 ∈ V ∧ Fun (𝐺 ∖ {∅}))) |
10 | | basendxnn 15752 |
. . . . . . . 8
⊢
(Base‘ndx) ∈ ℕ |
11 | 10 | nnrei 10906 |
. . . . . . 7
⊢
(Base‘ndx) ∈ ℝ |
12 | 11, 2 | ltneii 10029 |
. . . . . 6
⊢
(Base‘ndx) ≠ 𝑆 |
13 | 12 | a1i 11 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) ∧ (𝐺 ∈ V ∧ Fun 𝐺 ∧ {(Base‘ndx), 𝑆} ⊆ dom 𝐺)) → (Base‘ndx) ≠ 𝑆) |
14 | | simpr3 1062 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) ∧ (𝐺 ∈ V ∧ Fun 𝐺 ∧ {(Base‘ndx), 𝑆} ⊆ dom 𝐺)) → {(Base‘ndx), 𝑆} ⊆ dom 𝐺) |
15 | 9, 13, 14 | 3jca 1235 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) ∧ (𝐺 ∈ V ∧ Fun 𝐺 ∧ {(Base‘ndx), 𝑆} ⊆ dom 𝐺)) → ((𝐺 ∈ V ∧ Fun (𝐺 ∖ {∅})) ∧ (Base‘ndx)
≠ 𝑆 ∧
{(Base‘ndx), 𝑆}
⊆ dom 𝐺)) |
16 | 5, 15 | mpdan 699 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) → ((𝐺 ∈ V ∧ Fun (𝐺 ∖ {∅})) ∧
(Base‘ndx) ≠ 𝑆
∧ {(Base‘ndx), 𝑆}
⊆ dom 𝐺)) |
17 | | fvex 6113 |
. . . 4
⊢
(Base‘ndx) ∈ V |
18 | 1 | elexi 3186 |
. . . 4
⊢ 𝑆 ∈ V |
19 | 17, 18 | funiedgdm2val 25689 |
. . 3
⊢ (((𝐺 ∈ V ∧ Fun (𝐺 ∖ {∅})) ∧
(Base‘ndx) ≠ 𝑆
∧ {(Base‘ndx), 𝑆}
⊆ dom 𝐺) →
(iEdg‘𝐺) =
(.ef‘𝐺)) |
20 | 16, 19 | syl 17 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) →
(iEdg‘𝐺) =
(.ef‘𝐺)) |
21 | | prex 4836 |
. . . . . 6
⊢
{〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉} ∈ V |
22 | 21 | a1i 11 |
. . . . 5
⊢ (𝐺 = {〈(Base‘ndx),
𝑉〉, 〈𝑆, 𝐸〉} → {〈(Base‘ndx),
𝑉〉, 〈𝑆, 𝐸〉} ∈ V) |
23 | 3, 22 | syl5eqel 2692 |
. . . 4
⊢ (𝐺 = {〈(Base‘ndx),
𝑉〉, 〈𝑆, 𝐸〉} → 𝐺 ∈ V) |
24 | | edgfndxid 25670 |
. . . 4
⊢ (𝐺 ∈ V →
(.ef‘𝐺) = (𝐺‘(.ef‘ndx))) |
25 | 3, 23, 24 | mp2b 10 |
. . 3
⊢
(.ef‘𝐺) =
(𝐺‘(.ef‘ndx)) |
26 | | slotsbaseefdif 25672 |
. . . . . . . . 9
⊢
(Base‘ndx) ≠ (.ef‘ndx) |
27 | 26 | nesymi 2839 |
. . . . . . . 8
⊢ ¬
(.ef‘ndx) = (Base‘ndx) |
28 | 27 | a1i 11 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) → ¬
(.ef‘ndx) = (Base‘ndx)) |
29 | | neneq 2788 |
. . . . . . . . 9
⊢ (𝑆 ≠ (.ef‘ndx) →
¬ 𝑆 =
(.ef‘ndx)) |
30 | | eqcom 2617 |
. . . . . . . . 9
⊢
((.ef‘ndx) = 𝑆
↔ 𝑆 =
(.ef‘ndx)) |
31 | 29, 30 | sylnibr 318 |
. . . . . . . 8
⊢ (𝑆 ≠ (.ef‘ndx) →
¬ (.ef‘ndx) = 𝑆) |
32 | 31 | 3ad2ant3 1077 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) → ¬
(.ef‘ndx) = 𝑆) |
33 | | ioran 510 |
. . . . . . 7
⊢ (¬
((.ef‘ndx) = (Base‘ndx) ∨ (.ef‘ndx) = 𝑆) ↔ (¬ (.ef‘ndx) =
(Base‘ndx) ∧ ¬ (.ef‘ndx) = 𝑆)) |
34 | 28, 32, 33 | sylanbrc 695 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) → ¬
((.ef‘ndx) = (Base‘ndx) ∨ (.ef‘ndx) = 𝑆)) |
35 | | fvex 6113 |
. . . . . . 7
⊢
(.ef‘ndx) ∈ V |
36 | 35 | elpr 4146 |
. . . . . 6
⊢
((.ef‘ndx) ∈ {(Base‘ndx), 𝑆} ↔ ((.ef‘ndx) = (Base‘ndx)
∨ (.ef‘ndx) = 𝑆)) |
37 | 34, 36 | sylnibr 318 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) → ¬
(.ef‘ndx) ∈ {(Base‘ndx), 𝑆}) |
38 | 3 | dmeqi 5247 |
. . . . . 6
⊢ dom 𝐺 = dom {〈(Base‘ndx),
𝑉〉, 〈𝑆, 𝐸〉} |
39 | | dmpropg 5526 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → dom {〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉} = {(Base‘ndx), 𝑆}) |
40 | 39 | 3adant3 1074 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) → dom
{〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉} = {(Base‘ndx), 𝑆}) |
41 | 38, 40 | syl5eq 2656 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) → dom 𝐺 = {(Base‘ndx), 𝑆}) |
42 | 37, 41 | neleqtrrd 2710 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) → ¬
(.ef‘ndx) ∈ dom 𝐺) |
43 | | ndmfv 6128 |
. . . 4
⊢ (¬
(.ef‘ndx) ∈ dom 𝐺 → (𝐺‘(.ef‘ndx)) =
∅) |
44 | 42, 43 | syl 17 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) → (𝐺‘(.ef‘ndx)) =
∅) |
45 | 25, 44 | syl5eq 2656 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) →
(.ef‘𝐺) =
∅) |
46 | 20, 45 | eqtrd 2644 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) →
(iEdg‘𝐺) =
∅) |