Proof of Theorem structvtxvallem
Step | Hyp | Ref
| Expression |
1 | | prex 4836 |
. . 3
⊢
{〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉} ∈ V |
2 | 1 | a1i 11 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → {〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉} ∈ V) |
3 | | fvex 6113 |
. . . . . 6
⊢
(Base‘ndx) ∈ V |
4 | | structvtxvallem.s |
. . . . . 6
⊢ 𝑆 ∈ ℕ |
5 | 3, 4 | pm3.2i 470 |
. . . . 5
⊢
((Base‘ndx) ∈ V ∧ 𝑆 ∈ ℕ) |
6 | 5 | a1i 11 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((Base‘ndx) ∈ V ∧
𝑆 ∈
ℕ)) |
7 | | id 22 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) |
8 | | structvtxvallem.b |
. . . . . 6
⊢
(Base‘ndx) < 𝑆 |
9 | | basendxnn 15752 |
. . . . . . . . 9
⊢
(Base‘ndx) ∈ ℕ |
10 | 9 | nnrei 10906 |
. . . . . . . 8
⊢
(Base‘ndx) ∈ ℝ |
11 | 4 | nnrei 10906 |
. . . . . . . 8
⊢ 𝑆 ∈ ℝ |
12 | 10, 11 | ltnei 10040 |
. . . . . . 7
⊢
((Base‘ndx) < 𝑆 → 𝑆 ≠ (Base‘ndx)) |
13 | 12 | necomd 2837 |
. . . . . 6
⊢
((Base‘ndx) < 𝑆 → (Base‘ndx) ≠ 𝑆) |
14 | 8, 13 | ax-mp 5 |
. . . . 5
⊢
(Base‘ndx) ≠ 𝑆 |
15 | 14 | a1i 11 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Base‘ndx) ≠ 𝑆) |
16 | 6, 7, 15 | 3jca 1235 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (((Base‘ndx) ∈ V ∧
𝑆 ∈ ℕ) ∧
(𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (Base‘ndx) ≠ 𝑆)) |
17 | | funprg 5854 |
. . 3
⊢
((((Base‘ndx) ∈ V ∧ 𝑆 ∈ ℕ) ∧ (𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (Base‘ndx) ≠ 𝑆) → Fun
{〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉}) |
18 | 16, 17 | syl 17 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → Fun {〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉}) |
19 | | dmpropg 5526 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → dom {〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉} = {(Base‘ndx), 𝑆}) |
20 | 7, 19 | syl 17 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → dom {〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉} = {(Base‘ndx), 𝑆}) |
21 | 20 | eqcomd 2616 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → {(Base‘ndx), 𝑆} = dom {〈(Base‘ndx),
𝑉〉, 〈𝑆, 𝐸〉}) |
22 | | eqimss 3620 |
. . 3
⊢
({(Base‘ndx), 𝑆} = dom {〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉} → {(Base‘ndx), 𝑆} ⊆ dom
{〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉}) |
23 | 21, 22 | syl 17 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → {(Base‘ndx), 𝑆} ⊆ dom
{〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉}) |
24 | | structvtxvallem.g |
. . 3
⊢ 𝐺 = {〈(Base‘ndx),
𝑉〉, 〈𝑆, 𝐸〉} |
25 | | eleq1 2676 |
. . . 4
⊢ (𝐺 = {〈(Base‘ndx),
𝑉〉, 〈𝑆, 𝐸〉} → (𝐺 ∈ V ↔ {〈(Base‘ndx),
𝑉〉, 〈𝑆, 𝐸〉} ∈ V)) |
26 | | funeq 5823 |
. . . 4
⊢ (𝐺 = {〈(Base‘ndx),
𝑉〉, 〈𝑆, 𝐸〉} → (Fun 𝐺 ↔ Fun {〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉})) |
27 | | dmeq 5246 |
. . . . 5
⊢ (𝐺 = {〈(Base‘ndx),
𝑉〉, 〈𝑆, 𝐸〉} → dom 𝐺 = dom {〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉}) |
28 | 27 | sseq2d 3596 |
. . . 4
⊢ (𝐺 = {〈(Base‘ndx),
𝑉〉, 〈𝑆, 𝐸〉} → ({(Base‘ndx), 𝑆} ⊆ dom 𝐺 ↔ {(Base‘ndx), 𝑆} ⊆ dom {〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉})) |
29 | 25, 26, 28 | 3anbi123d 1391 |
. . 3
⊢ (𝐺 = {〈(Base‘ndx),
𝑉〉, 〈𝑆, 𝐸〉} → ((𝐺 ∈ V ∧ Fun 𝐺 ∧ {(Base‘ndx), 𝑆} ⊆ dom 𝐺) ↔ ({〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉} ∈ V ∧ Fun
{〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉} ∧ {(Base‘ndx), 𝑆} ⊆ dom
{〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉}))) |
30 | 24, 29 | ax-mp 5 |
. 2
⊢ ((𝐺 ∈ V ∧ Fun 𝐺 ∧ {(Base‘ndx), 𝑆} ⊆ dom 𝐺) ↔ ({〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉} ∈ V ∧ Fun
{〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉} ∧ {(Base‘ndx), 𝑆} ⊆ dom
{〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉})) |
31 | 2, 18, 23, 30 | syl3anbrc 1239 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐺 ∈ V ∧ Fun 𝐺 ∧ {(Base‘ndx), 𝑆} ⊆ dom 𝐺)) |