Proof of Theorem lfuhgr
| Step | Hyp | Ref
| Expression |
| 1 | | edgval 29066 |
. . . . 5
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
| 2 | | lfuhgr.2 |
. . . . . 6
⊢ 𝐼 = (iEdg‘𝐺) |
| 3 | 2 | rneqi 5948 |
. . . . 5
⊢ ran 𝐼 = ran (iEdg‘𝐺) |
| 4 | 1, 3 | eqtr4i 2768 |
. . . 4
⊢
(Edg‘𝐺) = ran
𝐼 |
| 5 | 4 | sseq1i 4012 |
. . 3
⊢
((Edg‘𝐺)
⊆ {𝑥 ∈ 𝒫
𝑉 ∣ 2 ≤
(♯‘𝑥)} ↔
ran 𝐼 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤
(♯‘𝑥)}) |
| 6 | 2 | uhgrfun 29083 |
. . . . 5
⊢ (𝐺 ∈ UHGraph → Fun 𝐼) |
| 7 | | fdmrn 6767 |
. . . . . 6
⊢ (Fun
𝐼 ↔ 𝐼:dom 𝐼⟶ran 𝐼) |
| 8 | | fss 6752 |
. . . . . . 7
⊢ ((𝐼:dom 𝐼⟶ran 𝐼 ∧ ran 𝐼 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) → 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) |
| 9 | 8 | ex 412 |
. . . . . 6
⊢ (𝐼:dom 𝐼⟶ran 𝐼 → (ran 𝐼 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} → 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)})) |
| 10 | 7, 9 | sylbi 217 |
. . . . 5
⊢ (Fun
𝐼 → (ran 𝐼 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} → 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)})) |
| 11 | 6, 10 | syl 17 |
. . . 4
⊢ (𝐺 ∈ UHGraph → (ran
𝐼 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤
(♯‘𝑥)} →
𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)})) |
| 12 | | frn 6743 |
. . . 4
⊢ (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} → ran 𝐼 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) |
| 13 | 11, 12 | impbid1 225 |
. . 3
⊢ (𝐺 ∈ UHGraph → (ran
𝐼 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤
(♯‘𝑥)} ↔
𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)})) |
| 14 | 5, 13 | bitrid 283 |
. 2
⊢ (𝐺 ∈ UHGraph →
((Edg‘𝐺) ⊆
{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤
(♯‘𝑥)} ↔
𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)})) |
| 15 | | uhgredgss 29148 |
. . . . 5
⊢ (𝐺 ∈ UHGraph →
(Edg‘𝐺) ⊆
(𝒫 (Vtx‘𝐺)
∖ {∅})) |
| 16 | 15 | difss2d 4139 |
. . . 4
⊢ (𝐺 ∈ UHGraph →
(Edg‘𝐺) ⊆
𝒫 (Vtx‘𝐺)) |
| 17 | | lfuhgr.1 |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
| 18 | 17 | pweqi 4616 |
. . . 4
⊢ 𝒫
𝑉 = 𝒫
(Vtx‘𝐺) |
| 19 | 16, 18 | sseqtrrdi 4025 |
. . 3
⊢ (𝐺 ∈ UHGraph →
(Edg‘𝐺) ⊆
𝒫 𝑉) |
| 20 | | ssrab 4073 |
. . . 4
⊢
((Edg‘𝐺)
⊆ {𝑥 ∈ 𝒫
𝑉 ∣ 2 ≤
(♯‘𝑥)} ↔
((Edg‘𝐺) ⊆
𝒫 𝑉 ∧
∀𝑥 ∈
(Edg‘𝐺)2 ≤
(♯‘𝑥))) |
| 21 | 20 | baib 535 |
. . 3
⊢
((Edg‘𝐺)
⊆ 𝒫 𝑉 →
((Edg‘𝐺) ⊆
{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤
(♯‘𝑥)} ↔
∀𝑥 ∈
(Edg‘𝐺)2 ≤
(♯‘𝑥))) |
| 22 | 19, 21 | syl 17 |
. 2
⊢ (𝐺 ∈ UHGraph →
((Edg‘𝐺) ⊆
{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤
(♯‘𝑥)} ↔
∀𝑥 ∈
(Edg‘𝐺)2 ≤
(♯‘𝑥))) |
| 23 | 14, 22 | bitr3d 281 |
1
⊢ (𝐺 ∈ UHGraph → (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ↔ ∀𝑥 ∈ (Edg‘𝐺)2 ≤ (♯‘𝑥))) |