| Step | Hyp | Ref
| Expression |
| 1 | | 0ss 4400 |
. . 3
⊢ ∅
⊆ (Vtx‘𝐺) |
| 2 | | eqid 2737 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 3 | | eqid 2737 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
| 4 | 2, 3 | isisubgr 47848 |
. . 3
⊢ ((𝐺 ∈ UHGraph ∧ ∅
⊆ (Vtx‘𝐺))
→ (𝐺 ISubGr ∅) =
〈∅, ((iEdg‘𝐺) ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ ∅})〉) |
| 5 | 1, 4 | mpan2 691 |
. 2
⊢ (𝐺 ∈ UHGraph → (𝐺 ISubGr ∅) =
〈∅, ((iEdg‘𝐺) ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ ∅})〉) |
| 6 | | inrab2 4317 |
. . . . . . 7
⊢ ({𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ ∅} ∩ dom
(iEdg‘𝐺)) = {𝑥 ∈ (dom (iEdg‘𝐺) ∩ dom (iEdg‘𝐺)) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ ∅} |
| 7 | | inidm 4227 |
. . . . . . . . 9
⊢ (dom
(iEdg‘𝐺) ∩ dom
(iEdg‘𝐺)) = dom
(iEdg‘𝐺) |
| 8 | 7 | rabeqi 3450 |
. . . . . . . 8
⊢ {𝑥 ∈ (dom (iEdg‘𝐺) ∩ dom (iEdg‘𝐺)) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ ∅} = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ ∅} |
| 9 | | ss0b 4401 |
. . . . . . . 8
⊢
(((iEdg‘𝐺)‘𝑥) ⊆ ∅ ↔ ((iEdg‘𝐺)‘𝑥) = ∅) |
| 10 | 8, 9 | rabbieq 3445 |
. . . . . . 7
⊢ {𝑥 ∈ (dom (iEdg‘𝐺) ∩ dom (iEdg‘𝐺)) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ ∅} = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) = ∅} |
| 11 | 6, 10 | eqtri 2765 |
. . . . . 6
⊢ ({𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ ∅} ∩ dom
(iEdg‘𝐺)) = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) = ∅} |
| 12 | 11 | ineqcomi 4211 |
. . . . 5
⊢ (dom
(iEdg‘𝐺) ∩ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ ∅}) = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) = ∅} |
| 13 | 2, 3 | uhgrf 29079 |
. . . . . . . 8
⊢ (𝐺 ∈ UHGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖
{∅})) |
| 14 | | ffvelcdm 7101 |
. . . . . . . . . 10
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅}) ∧ 𝑥 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑥) ∈ (𝒫 (Vtx‘𝐺) ∖
{∅})) |
| 15 | | eldifsni 4790 |
. . . . . . . . . 10
⊢
(((iEdg‘𝐺)‘𝑥) ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) →
((iEdg‘𝐺)‘𝑥) ≠ ∅) |
| 16 | 14, 15 | syl 17 |
. . . . . . . . 9
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅}) ∧ 𝑥 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑥) ≠ ∅) |
| 17 | 16 | neneqd 2945 |
. . . . . . . 8
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅}) ∧ 𝑥 ∈ dom (iEdg‘𝐺)) → ¬
((iEdg‘𝐺)‘𝑥) = ∅) |
| 18 | 13, 17 | sylan 580 |
. . . . . . 7
⊢ ((𝐺 ∈ UHGraph ∧ 𝑥 ∈ dom (iEdg‘𝐺)) → ¬
((iEdg‘𝐺)‘𝑥) = ∅) |
| 19 | 18 | ralrimiva 3146 |
. . . . . 6
⊢ (𝐺 ∈ UHGraph →
∀𝑥 ∈ dom
(iEdg‘𝐺) ¬
((iEdg‘𝐺)‘𝑥) = ∅) |
| 20 | | rabeq0 4388 |
. . . . . 6
⊢ ({𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) = ∅} = ∅ ↔ ∀𝑥 ∈ dom (iEdg‘𝐺) ¬ ((iEdg‘𝐺)‘𝑥) = ∅) |
| 21 | 19, 20 | sylibr 234 |
. . . . 5
⊢ (𝐺 ∈ UHGraph → {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) = ∅} = ∅) |
| 22 | 12, 21 | eqtrid 2789 |
. . . 4
⊢ (𝐺 ∈ UHGraph → (dom
(iEdg‘𝐺) ∩ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ ∅}) =
∅) |
| 23 | 3 | uhgrfun 29083 |
. . . . . 6
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
| 24 | 23 | funfnd 6597 |
. . . . 5
⊢ (𝐺 ∈ UHGraph →
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
| 25 | | fnresdisj 6688 |
. . . . 5
⊢
((iEdg‘𝐺) Fn
dom (iEdg‘𝐺) →
((dom (iEdg‘𝐺) ∩
{𝑥 ∈ dom
(iEdg‘𝐺) ∣
((iEdg‘𝐺)‘𝑥) ⊆ ∅}) = ∅
↔ ((iEdg‘𝐺)
↾ {𝑥 ∈ dom
(iEdg‘𝐺) ∣
((iEdg‘𝐺)‘𝑥) ⊆ ∅}) =
∅)) |
| 26 | 24, 25 | syl 17 |
. . . 4
⊢ (𝐺 ∈ UHGraph → ((dom
(iEdg‘𝐺) ∩ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ ∅}) = ∅ ↔
((iEdg‘𝐺) ↾
{𝑥 ∈ dom
(iEdg‘𝐺) ∣
((iEdg‘𝐺)‘𝑥) ⊆ ∅}) =
∅)) |
| 27 | 22, 26 | mpbid 232 |
. . 3
⊢ (𝐺 ∈ UHGraph →
((iEdg‘𝐺) ↾
{𝑥 ∈ dom
(iEdg‘𝐺) ∣
((iEdg‘𝐺)‘𝑥) ⊆ ∅}) =
∅) |
| 28 | 27 | opeq2d 4880 |
. 2
⊢ (𝐺 ∈ UHGraph →
〈∅, ((iEdg‘𝐺) ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ ∅})〉 = 〈∅,
∅〉) |
| 29 | 5, 28 | eqtrd 2777 |
1
⊢ (𝐺 ∈ UHGraph → (𝐺 ISubGr ∅) =
〈∅, ∅〉) |