| Step | Hyp | Ref
| Expression |
| 1 | | isubgrvtx.v |
. . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) |
| 2 | | eqid 2737 |
. . . . . . 7
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
| 3 | 1, 2 | uhgrf 29079 |
. . . . . 6
⊢ (𝐺 ∈ UHGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅})) |
| 4 | 3 | adantr 480 |
. . . . 5
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅})) |
| 5 | | dmresss 6029 |
. . . . . 6
⊢ dom
((iEdg‘𝐺) ↾
{𝑥 ∈ dom
(iEdg‘𝐺) ∣
((iEdg‘𝐺)‘𝑥) ⊆ 𝑆}) ⊆ dom (iEdg‘𝐺) |
| 6 | 5 | a1i 11 |
. . . . 5
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → dom ((iEdg‘𝐺) ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆}) ⊆ dom (iEdg‘𝐺)) |
| 7 | | imadmres 6254 |
. . . . . 6
⊢
((iEdg‘𝐺)
“ dom ((iEdg‘𝐺)
↾ {𝑥 ∈ dom
(iEdg‘𝐺) ∣
((iEdg‘𝐺)‘𝑥) ⊆ 𝑆})) = ((iEdg‘𝐺) “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆}) |
| 8 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . 17
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}) ∧ 𝑦 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑦) ∈ (𝒫 𝑉 ∖ {∅})) |
| 9 | | eldifsni 4790 |
. . . . . . . . . . . . . . . . 17
⊢
(((iEdg‘𝐺)‘𝑦) ∈ (𝒫 𝑉 ∖ {∅}) →
((iEdg‘𝐺)‘𝑦) ≠ ∅) |
| 10 | 8, 9 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}) ∧ 𝑦 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑦) ≠ ∅) |
| 11 | 10 | ex 412 |
. . . . . . . . . . . . . . 15
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}) → (𝑦 ∈ dom (iEdg‘𝐺) → ((iEdg‘𝐺)‘𝑦) ≠ ∅)) |
| 12 | 3, 11 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ UHGraph → (𝑦 ∈ dom (iEdg‘𝐺) → ((iEdg‘𝐺)‘𝑦) ≠ ∅)) |
| 13 | 12 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (𝑦 ∈ dom (iEdg‘𝐺) → ((iEdg‘𝐺)‘𝑦) ≠ ∅)) |
| 14 | 13 | imp 406 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) ∧ 𝑦 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑦) ≠ ∅) |
| 15 | | fvexd 6921 |
. . . . . . . . . . . . 13
⊢
(((iEdg‘𝐺)‘𝑦) ⊆ 𝑆 → ((iEdg‘𝐺)‘𝑦) ∈ V) |
| 16 | | id 22 |
. . . . . . . . . . . . 13
⊢
(((iEdg‘𝐺)‘𝑦) ⊆ 𝑆 → ((iEdg‘𝐺)‘𝑦) ⊆ 𝑆) |
| 17 | 15, 16 | elpwd 4606 |
. . . . . . . . . . . 12
⊢
(((iEdg‘𝐺)‘𝑦) ⊆ 𝑆 → ((iEdg‘𝐺)‘𝑦) ∈ 𝒫 𝑆) |
| 18 | 14, 17 | anim12ci 614 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) ∧ 𝑦 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐺)‘𝑦) ⊆ 𝑆) → (((iEdg‘𝐺)‘𝑦) ∈ 𝒫 𝑆 ∧ ((iEdg‘𝐺)‘𝑦) ≠ ∅)) |
| 19 | | eldifsn 4786 |
. . . . . . . . . . 11
⊢
(((iEdg‘𝐺)‘𝑦) ∈ (𝒫 𝑆 ∖ {∅}) ↔
(((iEdg‘𝐺)‘𝑦) ∈ 𝒫 𝑆 ∧ ((iEdg‘𝐺)‘𝑦) ≠ ∅)) |
| 20 | 18, 19 | sylibr 234 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) ∧ 𝑦 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐺)‘𝑦) ⊆ 𝑆) → ((iEdg‘𝐺)‘𝑦) ∈ (𝒫 𝑆 ∖ {∅})) |
| 21 | 20 | ex 412 |
. . . . . . . . 9
⊢ (((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) ∧ 𝑦 ∈ dom (iEdg‘𝐺)) → (((iEdg‘𝐺)‘𝑦) ⊆ 𝑆 → ((iEdg‘𝐺)‘𝑦) ∈ (𝒫 𝑆 ∖ {∅}))) |
| 22 | 21 | ralrimiva 3146 |
. . . . . . . 8
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → ∀𝑦 ∈ dom (iEdg‘𝐺)(((iEdg‘𝐺)‘𝑦) ⊆ 𝑆 → ((iEdg‘𝐺)‘𝑦) ∈ (𝒫 𝑆 ∖ {∅}))) |
| 23 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝐺)‘𝑦)) |
| 24 | 23 | sseq1d 4015 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (((iEdg‘𝐺)‘𝑥) ⊆ 𝑆 ↔ ((iEdg‘𝐺)‘𝑦) ⊆ 𝑆)) |
| 25 | 24 | ralrab 3699 |
. . . . . . . 8
⊢
(∀𝑦 ∈
{𝑥 ∈ dom
(iEdg‘𝐺) ∣
((iEdg‘𝐺)‘𝑥) ⊆ 𝑆} ((iEdg‘𝐺)‘𝑦) ∈ (𝒫 𝑆 ∖ {∅}) ↔ ∀𝑦 ∈ dom (iEdg‘𝐺)(((iEdg‘𝐺)‘𝑦) ⊆ 𝑆 → ((iEdg‘𝐺)‘𝑦) ∈ (𝒫 𝑆 ∖ {∅}))) |
| 26 | 22, 25 | sylibr 234 |
. . . . . . 7
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → ∀𝑦 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆} ((iEdg‘𝐺)‘𝑦) ∈ (𝒫 𝑆 ∖ {∅})) |
| 27 | | ffun 6739 |
. . . . . . . . . . 11
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}) → Fun
(iEdg‘𝐺)) |
| 28 | | ssrab2 4080 |
. . . . . . . . . . 11
⊢ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆} ⊆ dom (iEdg‘𝐺) |
| 29 | 27, 28 | jctir 520 |
. . . . . . . . . 10
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}) → (Fun
(iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆} ⊆ dom (iEdg‘𝐺))) |
| 30 | 3, 29 | syl 17 |
. . . . . . . . 9
⊢ (𝐺 ∈ UHGraph → (Fun
(iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆} ⊆ dom (iEdg‘𝐺))) |
| 31 | 30 | adantr 480 |
. . . . . . . 8
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (Fun (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆} ⊆ dom (iEdg‘𝐺))) |
| 32 | | funimass4 6973 |
. . . . . . . 8
⊢ ((Fun
(iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆} ⊆ dom (iEdg‘𝐺)) → (((iEdg‘𝐺) “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆}) ⊆ (𝒫 𝑆 ∖ {∅}) ↔ ∀𝑦 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆} ((iEdg‘𝐺)‘𝑦) ∈ (𝒫 𝑆 ∖ {∅}))) |
| 33 | 31, 32 | syl 17 |
. . . . . . 7
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (((iEdg‘𝐺) “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆}) ⊆ (𝒫 𝑆 ∖ {∅}) ↔ ∀𝑦 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆} ((iEdg‘𝐺)‘𝑦) ∈ (𝒫 𝑆 ∖ {∅}))) |
| 34 | 26, 33 | mpbird 257 |
. . . . . 6
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → ((iEdg‘𝐺) “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆}) ⊆ (𝒫 𝑆 ∖ {∅})) |
| 35 | 7, 34 | eqsstrid 4022 |
. . . . 5
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → ((iEdg‘𝐺) “ dom ((iEdg‘𝐺) ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆})) ⊆ (𝒫 𝑆 ∖ {∅})) |
| 36 | 4, 6, 35 | fssrescdmd 7146 |
. . . 4
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → ((iEdg‘𝐺) ↾ dom ((iEdg‘𝐺) ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆})):dom ((iEdg‘𝐺) ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆})⟶(𝒫 𝑆 ∖ {∅})) |
| 37 | | resdmres 6252 |
. . . . . 6
⊢
((iEdg‘𝐺)
↾ dom ((iEdg‘𝐺)
↾ {𝑥 ∈ dom
(iEdg‘𝐺) ∣
((iEdg‘𝐺)‘𝑥) ⊆ 𝑆})) = ((iEdg‘𝐺) ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆}) |
| 38 | 37 | eqcomi 2746 |
. . . . 5
⊢
((iEdg‘𝐺)
↾ {𝑥 ∈ dom
(iEdg‘𝐺) ∣
((iEdg‘𝐺)‘𝑥) ⊆ 𝑆}) = ((iEdg‘𝐺) ↾ dom ((iEdg‘𝐺) ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆})) |
| 39 | 38 | feq1i 6727 |
. . . 4
⊢
(((iEdg‘𝐺)
↾ {𝑥 ∈ dom
(iEdg‘𝐺) ∣
((iEdg‘𝐺)‘𝑥) ⊆ 𝑆}):dom ((iEdg‘𝐺) ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆})⟶(𝒫 𝑆 ∖ {∅}) ↔
((iEdg‘𝐺) ↾ dom
((iEdg‘𝐺) ↾
{𝑥 ∈ dom
(iEdg‘𝐺) ∣
((iEdg‘𝐺)‘𝑥) ⊆ 𝑆})):dom ((iEdg‘𝐺) ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆})⟶(𝒫 𝑆 ∖ {∅})) |
| 40 | 36, 39 | sylibr 234 |
. . 3
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → ((iEdg‘𝐺) ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆}):dom ((iEdg‘𝐺) ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆})⟶(𝒫 𝑆 ∖ {∅})) |
| 41 | 1, 2 | isubgriedg 47849 |
. . . 4
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (iEdg‘(𝐺 ISubGr 𝑆)) = ((iEdg‘𝐺) ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆})) |
| 42 | 41 | dmeqd 5916 |
. . . 4
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → dom (iEdg‘(𝐺 ISubGr 𝑆)) = dom ((iEdg‘𝐺) ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆})) |
| 43 | 1 | isubgrvtx 47853 |
. . . . . 6
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (Vtx‘(𝐺 ISubGr 𝑆)) = 𝑆) |
| 44 | 43 | pweqd 4617 |
. . . . 5
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → 𝒫 (Vtx‘(𝐺 ISubGr 𝑆)) = 𝒫 𝑆) |
| 45 | 44 | difeq1d 4125 |
. . . 4
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (𝒫 (Vtx‘(𝐺 ISubGr 𝑆)) ∖ {∅}) = (𝒫 𝑆 ∖
{∅})) |
| 46 | 41, 42, 45 | feq123d 6725 |
. . 3
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → ((iEdg‘(𝐺 ISubGr 𝑆)):dom (iEdg‘(𝐺 ISubGr 𝑆))⟶(𝒫 (Vtx‘(𝐺 ISubGr 𝑆)) ∖ {∅}) ↔
((iEdg‘𝐺) ↾
{𝑥 ∈ dom
(iEdg‘𝐺) ∣
((iEdg‘𝐺)‘𝑥) ⊆ 𝑆}):dom ((iEdg‘𝐺) ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑆})⟶(𝒫 𝑆 ∖ {∅}))) |
| 47 | 40, 46 | mpbird 257 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (iEdg‘(𝐺 ISubGr 𝑆)):dom (iEdg‘(𝐺 ISubGr 𝑆))⟶(𝒫 (Vtx‘(𝐺 ISubGr 𝑆)) ∖ {∅})) |
| 48 | | ovexd 7466 |
. . 3
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ V) |
| 49 | | eqid 2737 |
. . . 4
⊢
(Vtx‘(𝐺 ISubGr
𝑆)) = (Vtx‘(𝐺 ISubGr 𝑆)) |
| 50 | | eqid 2737 |
. . . 4
⊢
(iEdg‘(𝐺
ISubGr 𝑆)) =
(iEdg‘(𝐺 ISubGr 𝑆)) |
| 51 | 49, 50 | isuhgr 29077 |
. . 3
⊢ ((𝐺 ISubGr 𝑆) ∈ V → ((𝐺 ISubGr 𝑆) ∈ UHGraph ↔ (iEdg‘(𝐺 ISubGr 𝑆)):dom (iEdg‘(𝐺 ISubGr 𝑆))⟶(𝒫 (Vtx‘(𝐺 ISubGr 𝑆)) ∖ {∅}))) |
| 52 | 48, 51 | syl 17 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → ((𝐺 ISubGr 𝑆) ∈ UHGraph ↔ (iEdg‘(𝐺 ISubGr 𝑆)):dom (iEdg‘(𝐺 ISubGr 𝑆))⟶(𝒫 (Vtx‘(𝐺 ISubGr 𝑆)) ∖ {∅}))) |
| 53 | 47, 52 | mpbird 257 |
1
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ UHGraph) |