| Step | Hyp | Ref
| Expression |
| 1 | | difssd 4137 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑉) → (𝑉 ∖ {𝑁}) ⊆ 𝑉) |
| 2 | | uhgrspan1.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
| 3 | | uhgrspan1.i |
. . . 4
⊢ 𝐼 = (iEdg‘𝐺) |
| 4 | | uhgrspan1.f |
. . . 4
⊢ 𝐹 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∉ (𝐼‘𝑖)} |
| 5 | | uhgrspan1.s |
. . . 4
⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), (𝐼 ↾ 𝐹)〉 |
| 6 | 2, 3, 4, 5 | uhgrspan1lem3 29319 |
. . 3
⊢
(iEdg‘𝑆) =
(𝐼 ↾ 𝐹) |
| 7 | | resresdm 6253 |
. . 3
⊢
((iEdg‘𝑆) =
(𝐼 ↾ 𝐹) → (iEdg‘𝑆) = (𝐼 ↾ dom (iEdg‘𝑆))) |
| 8 | 6, 7 | mp1i 13 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑉) → (iEdg‘𝑆) = (𝐼 ↾ dom (iEdg‘𝑆))) |
| 9 | 3 | uhgrfun 29083 |
. . . . . 6
⊢ (𝐺 ∈ UHGraph → Fun 𝐼) |
| 10 | | fvelima 6974 |
. . . . . . 7
⊢ ((Fun
𝐼 ∧ 𝑐 ∈ (𝐼 “ 𝐹)) → ∃𝑗 ∈ 𝐹 (𝐼‘𝑗) = 𝑐) |
| 11 | 10 | ex 412 |
. . . . . 6
⊢ (Fun
𝐼 → (𝑐 ∈ (𝐼 “ 𝐹) → ∃𝑗 ∈ 𝐹 (𝐼‘𝑗) = 𝑐)) |
| 12 | 9, 11 | syl 17 |
. . . . 5
⊢ (𝐺 ∈ UHGraph → (𝑐 ∈ (𝐼 “ 𝐹) → ∃𝑗 ∈ 𝐹 (𝐼‘𝑗) = 𝑐)) |
| 13 | 12 | adantr 480 |
. . . 4
⊢ ((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑉) → (𝑐 ∈ (𝐼 “ 𝐹) → ∃𝑗 ∈ 𝐹 (𝐼‘𝑗) = 𝑐)) |
| 14 | | eqidd 2738 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → 𝑁 = 𝑁) |
| 15 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → (𝐼‘𝑖) = (𝐼‘𝑗)) |
| 16 | 14, 15 | neleq12d 3051 |
. . . . . . 7
⊢ (𝑖 = 𝑗 → (𝑁 ∉ (𝐼‘𝑖) ↔ 𝑁 ∉ (𝐼‘𝑗))) |
| 17 | 16, 4 | elrab2 3695 |
. . . . . 6
⊢ (𝑗 ∈ 𝐹 ↔ (𝑗 ∈ dom 𝐼 ∧ 𝑁 ∉ (𝐼‘𝑗))) |
| 18 | | fvexd 6921 |
. . . . . . . . 9
⊢ (((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ 𝑁 ∉ (𝐼‘𝑗))) → (𝐼‘𝑗) ∈ V) |
| 19 | 2, 3 | uhgrss 29081 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UHGraph ∧ 𝑗 ∈ dom 𝐼) → (𝐼‘𝑗) ⊆ 𝑉) |
| 20 | 19 | ad2ant2r 747 |
. . . . . . . . 9
⊢ (((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ 𝑁 ∉ (𝐼‘𝑗))) → (𝐼‘𝑗) ⊆ 𝑉) |
| 21 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ 𝑁 ∉ (𝐼‘𝑗))) → 𝑁 ∉ (𝐼‘𝑗)) |
| 22 | | elpwdifsn 4789 |
. . . . . . . . 9
⊢ (((𝐼‘𝑗) ∈ V ∧ (𝐼‘𝑗) ⊆ 𝑉 ∧ 𝑁 ∉ (𝐼‘𝑗)) → (𝐼‘𝑗) ∈ 𝒫 (𝑉 ∖ {𝑁})) |
| 23 | 18, 20, 21, 22 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ 𝑁 ∉ (𝐼‘𝑗))) → (𝐼‘𝑗) ∈ 𝒫 (𝑉 ∖ {𝑁})) |
| 24 | | eleq1 2829 |
. . . . . . . . 9
⊢ (𝑐 = (𝐼‘𝑗) → (𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁}) ↔ (𝐼‘𝑗) ∈ 𝒫 (𝑉 ∖ {𝑁}))) |
| 25 | 24 | eqcoms 2745 |
. . . . . . . 8
⊢ ((𝐼‘𝑗) = 𝑐 → (𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁}) ↔ (𝐼‘𝑗) ∈ 𝒫 (𝑉 ∖ {𝑁}))) |
| 26 | 23, 25 | syl5ibrcom 247 |
. . . . . . 7
⊢ (((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ 𝑁 ∉ (𝐼‘𝑗))) → ((𝐼‘𝑗) = 𝑐 → 𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁}))) |
| 27 | 26 | ex 412 |
. . . . . 6
⊢ ((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑉) → ((𝑗 ∈ dom 𝐼 ∧ 𝑁 ∉ (𝐼‘𝑗)) → ((𝐼‘𝑗) = 𝑐 → 𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁})))) |
| 28 | 17, 27 | biimtrid 242 |
. . . . 5
⊢ ((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑉) → (𝑗 ∈ 𝐹 → ((𝐼‘𝑗) = 𝑐 → 𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁})))) |
| 29 | 28 | rexlimdv 3153 |
. . . 4
⊢ ((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑉) → (∃𝑗 ∈ 𝐹 (𝐼‘𝑗) = 𝑐 → 𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁}))) |
| 30 | 13, 29 | syld 47 |
. . 3
⊢ ((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑉) → (𝑐 ∈ (𝐼 “ 𝐹) → 𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁}))) |
| 31 | 30 | ssrdv 3989 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑉) → (𝐼 “ 𝐹) ⊆ 𝒫 (𝑉 ∖ {𝑁})) |
| 32 | | opex 5469 |
. . . . 5
⊢
〈(𝑉 ∖
{𝑁}), (𝐼 ↾ 𝐹)〉 ∈ V |
| 33 | 5, 32 | eqeltri 2837 |
. . . 4
⊢ 𝑆 ∈ V |
| 34 | 33 | a1i 11 |
. . 3
⊢ (𝑁 ∈ 𝑉 → 𝑆 ∈ V) |
| 35 | 2, 3, 4, 5 | uhgrspan1lem2 29318 |
. . . . 5
⊢
(Vtx‘𝑆) =
(𝑉 ∖ {𝑁}) |
| 36 | 35 | eqcomi 2746 |
. . . 4
⊢ (𝑉 ∖ {𝑁}) = (Vtx‘𝑆) |
| 37 | | eqid 2737 |
. . . 4
⊢
(iEdg‘𝑆) =
(iEdg‘𝑆) |
| 38 | 6 | rneqi 5948 |
. . . . 5
⊢ ran
(iEdg‘𝑆) = ran (𝐼 ↾ 𝐹) |
| 39 | | edgval 29066 |
. . . . 5
⊢
(Edg‘𝑆) = ran
(iEdg‘𝑆) |
| 40 | | df-ima 5698 |
. . . . 5
⊢ (𝐼 “ 𝐹) = ran (𝐼 ↾ 𝐹) |
| 41 | 38, 39, 40 | 3eqtr4ri 2776 |
. . . 4
⊢ (𝐼 “ 𝐹) = (Edg‘𝑆) |
| 42 | 36, 2, 37, 3, 41 | issubgr 29288 |
. . 3
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ∈ V) → (𝑆 SubGraph 𝐺 ↔ ((𝑉 ∖ {𝑁}) ⊆ 𝑉 ∧ (iEdg‘𝑆) = (𝐼 ↾ dom (iEdg‘𝑆)) ∧ (𝐼 “ 𝐹) ⊆ 𝒫 (𝑉 ∖ {𝑁})))) |
| 43 | 34, 42 | sylan2 593 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑉) → (𝑆 SubGraph 𝐺 ↔ ((𝑉 ∖ {𝑁}) ⊆ 𝑉 ∧ (iEdg‘𝑆) = (𝐼 ↾ dom (iEdg‘𝑆)) ∧ (𝐼 “ 𝐹) ⊆ 𝒫 (𝑉 ∖ {𝑁})))) |
| 44 | 1, 8, 31, 43 | mpbir3and 1343 |
1
⊢ ((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 SubGraph 𝐺) |