Proof of Theorem lpvtx
Step | Hyp | Ref
| Expression |
1 | | simp1 1061 |
. . . 4
⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ (𝐼‘𝐽) = {𝐴}) → 𝐺 ∈ UHGraph ) |
2 | | lpvtx.i |
. . . . . . 7
⊢ 𝐼 = (iEdg‘𝐺) |
3 | 2 | uhgrfun 25961 |
. . . . . 6
⊢ (𝐺 ∈ UHGraph → Fun 𝐼) |
4 | | funfn 5918 |
. . . . . 6
⊢ (Fun
𝐼 ↔ 𝐼 Fn dom 𝐼) |
5 | 3, 4 | sylib 208 |
. . . . 5
⊢ (𝐺 ∈ UHGraph → 𝐼 Fn dom 𝐼) |
6 | 5 | 3ad2ant1 1082 |
. . . 4
⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ (𝐼‘𝐽) = {𝐴}) → 𝐼 Fn dom 𝐼) |
7 | | simp2 1062 |
. . . 4
⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ (𝐼‘𝐽) = {𝐴}) → 𝐽 ∈ dom 𝐼) |
8 | 2 | uhgrn0 25962 |
. . . 4
⊢ ((𝐺 ∈ UHGraph ∧ 𝐼 Fn dom 𝐼 ∧ 𝐽 ∈ dom 𝐼) → (𝐼‘𝐽) ≠ ∅) |
9 | 1, 6, 7, 8 | syl3anc 1326 |
. . 3
⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ (𝐼‘𝐽) = {𝐴}) → (𝐼‘𝐽) ≠ ∅) |
10 | | neeq1 2856 |
. . . . 5
⊢ ((𝐼‘𝐽) = {𝐴} → ((𝐼‘𝐽) ≠ ∅ ↔ {𝐴} ≠ ∅)) |
11 | 10 | biimpd 219 |
. . . 4
⊢ ((𝐼‘𝐽) = {𝐴} → ((𝐼‘𝐽) ≠ ∅ → {𝐴} ≠ ∅)) |
12 | 11 | 3ad2ant3 1084 |
. . 3
⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ (𝐼‘𝐽) = {𝐴}) → ((𝐼‘𝐽) ≠ ∅ → {𝐴} ≠ ∅)) |
13 | 9, 12 | mpd 15 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ (𝐼‘𝐽) = {𝐴}) → {𝐴} ≠ ∅) |
14 | | eqid 2622 |
. . . . . 6
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
15 | 14, 2 | uhgrss 25959 |
. . . . 5
⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼) → (𝐼‘𝐽) ⊆ (Vtx‘𝐺)) |
16 | 15 | 3adant3 1081 |
. . . 4
⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ (𝐼‘𝐽) = {𝐴}) → (𝐼‘𝐽) ⊆ (Vtx‘𝐺)) |
17 | | sseq1 3626 |
. . . . 5
⊢ ((𝐼‘𝐽) = {𝐴} → ((𝐼‘𝐽) ⊆ (Vtx‘𝐺) ↔ {𝐴} ⊆ (Vtx‘𝐺))) |
18 | 17 | 3ad2ant3 1084 |
. . . 4
⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ (𝐼‘𝐽) = {𝐴}) → ((𝐼‘𝐽) ⊆ (Vtx‘𝐺) ↔ {𝐴} ⊆ (Vtx‘𝐺))) |
19 | 16, 18 | mpbid 222 |
. . 3
⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ (𝐼‘𝐽) = {𝐴}) → {𝐴} ⊆ (Vtx‘𝐺)) |
20 | | snnzb 4254 |
. . . 4
⊢ (𝐴 ∈ V ↔ {𝐴} ≠ ∅) |
21 | | snssg 4327 |
. . . 4
⊢ (𝐴 ∈ V → (𝐴 ∈ (Vtx‘𝐺) ↔ {𝐴} ⊆ (Vtx‘𝐺))) |
22 | 20, 21 | sylbir 225 |
. . 3
⊢ ({𝐴} ≠ ∅ → (𝐴 ∈ (Vtx‘𝐺) ↔ {𝐴} ⊆ (Vtx‘𝐺))) |
23 | 19, 22 | syl5ibrcom 237 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ (𝐼‘𝐽) = {𝐴}) → ({𝐴} ≠ ∅ → 𝐴 ∈ (Vtx‘𝐺))) |
24 | 13, 23 | mpd 15 |
1
⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ (𝐼‘𝐽) = {𝐴}) → 𝐴 ∈ (Vtx‘𝐺)) |