Proof of Theorem ausgrusgri
| Step | Hyp | Ref
| Expression |
| 1 | | fvex 6919 |
. . . . 5
⊢
(Vtx‘𝐻) ∈
V |
| 2 | | fvex 6919 |
. . . . 5
⊢
(Edg‘𝐻) ∈
V |
| 3 | | ausgr.1 |
. . . . . 6
⊢ 𝐺 = {〈𝑣, 𝑒〉 ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (♯‘𝑥) = 2}} |
| 4 | 3 | isausgr 29181 |
. . . . 5
⊢
(((Vtx‘𝐻)
∈ V ∧ (Edg‘𝐻) ∈ V) → ((Vtx‘𝐻)𝐺(Edg‘𝐻) ↔ (Edg‘𝐻) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (♯‘𝑥) = 2})) |
| 5 | 1, 2, 4 | mp2an 692 |
. . . 4
⊢
((Vtx‘𝐻)𝐺(Edg‘𝐻) ↔ (Edg‘𝐻) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (♯‘𝑥) = 2}) |
| 6 | | edgval 29066 |
. . . . . . 7
⊢
(Edg‘𝐻) = ran
(iEdg‘𝐻) |
| 7 | 6 | a1i 11 |
. . . . . 6
⊢ (𝐻 ∈ 𝑊 → (Edg‘𝐻) = ran (iEdg‘𝐻)) |
| 8 | 7 | sseq1d 4015 |
. . . . 5
⊢ (𝐻 ∈ 𝑊 → ((Edg‘𝐻) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (♯‘𝑥) = 2} ↔ ran
(iEdg‘𝐻) ⊆
{𝑥 ∈ 𝒫
(Vtx‘𝐻) ∣
(♯‘𝑥) =
2})) |
| 9 | | ausgrusgri.1 |
. . . . . . . . . 10
⊢ 𝑂 = {𝑓 ∣ 𝑓:dom 𝑓–1-1→ran 𝑓} |
| 10 | 9 | eleq2i 2833 |
. . . . . . . . 9
⊢
((iEdg‘𝐻)
∈ 𝑂 ↔
(iEdg‘𝐻) ∈
{𝑓 ∣ 𝑓:dom 𝑓–1-1→ran 𝑓}) |
| 11 | | fvex 6919 |
. . . . . . . . . 10
⊢
(iEdg‘𝐻)
∈ V |
| 12 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑓 = (iEdg‘𝐻) → 𝑓 = (iEdg‘𝐻)) |
| 13 | | dmeq 5914 |
. . . . . . . . . . 11
⊢ (𝑓 = (iEdg‘𝐻) → dom 𝑓 = dom (iEdg‘𝐻)) |
| 14 | | rneq 5947 |
. . . . . . . . . . 11
⊢ (𝑓 = (iEdg‘𝐻) → ran 𝑓 = ran (iEdg‘𝐻)) |
| 15 | 12, 13, 14 | f1eq123d 6840 |
. . . . . . . . . 10
⊢ (𝑓 = (iEdg‘𝐻) → (𝑓:dom 𝑓–1-1→ran 𝑓 ↔ (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→ran (iEdg‘𝐻))) |
| 16 | 11, 15 | elab 3679 |
. . . . . . . . 9
⊢
((iEdg‘𝐻)
∈ {𝑓 ∣ 𝑓:dom 𝑓–1-1→ran 𝑓} ↔ (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→ran (iEdg‘𝐻)) |
| 17 | 10, 16 | sylbb 219 |
. . . . . . . 8
⊢
((iEdg‘𝐻)
∈ 𝑂 →
(iEdg‘𝐻):dom
(iEdg‘𝐻)–1-1→ran (iEdg‘𝐻)) |
| 18 | 17 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝐻 ∈ 𝑊 ∧ ran (iEdg‘𝐻) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (♯‘𝑥) = 2} ∧ (iEdg‘𝐻) ∈ 𝑂) → (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→ran (iEdg‘𝐻)) |
| 19 | | simp2 1138 |
. . . . . . 7
⊢ ((𝐻 ∈ 𝑊 ∧ ran (iEdg‘𝐻) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (♯‘𝑥) = 2} ∧ (iEdg‘𝐻) ∈ 𝑂) → ran (iEdg‘𝐻) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (♯‘𝑥) = 2}) |
| 20 | | f1ssr 6810 |
. . . . . . 7
⊢
(((iEdg‘𝐻):dom
(iEdg‘𝐻)–1-1→ran (iEdg‘𝐻) ∧ ran (iEdg‘𝐻) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (♯‘𝑥) = 2}) → (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (♯‘𝑥) = 2}) |
| 21 | 18, 19, 20 | syl2anc 584 |
. . . . . 6
⊢ ((𝐻 ∈ 𝑊 ∧ ran (iEdg‘𝐻) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (♯‘𝑥) = 2} ∧ (iEdg‘𝐻) ∈ 𝑂) → (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (♯‘𝑥) = 2}) |
| 22 | 21 | 3exp 1120 |
. . . . 5
⊢ (𝐻 ∈ 𝑊 → (ran (iEdg‘𝐻) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (♯‘𝑥) = 2} → ((iEdg‘𝐻) ∈ 𝑂 → (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (♯‘𝑥) = 2}))) |
| 23 | 8, 22 | sylbid 240 |
. . . 4
⊢ (𝐻 ∈ 𝑊 → ((Edg‘𝐻) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (♯‘𝑥) = 2} → ((iEdg‘𝐻) ∈ 𝑂 → (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (♯‘𝑥) = 2}))) |
| 24 | 5, 23 | biimtrid 242 |
. . 3
⊢ (𝐻 ∈ 𝑊 → ((Vtx‘𝐻)𝐺(Edg‘𝐻) → ((iEdg‘𝐻) ∈ 𝑂 → (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (♯‘𝑥) = 2}))) |
| 25 | 24 | 3imp 1111 |
. 2
⊢ ((𝐻 ∈ 𝑊 ∧ (Vtx‘𝐻)𝐺(Edg‘𝐻) ∧ (iEdg‘𝐻) ∈ 𝑂) → (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (♯‘𝑥) = 2}) |
| 26 | | eqid 2737 |
. . . 4
⊢
(Vtx‘𝐻) =
(Vtx‘𝐻) |
| 27 | | eqid 2737 |
. . . 4
⊢
(iEdg‘𝐻) =
(iEdg‘𝐻) |
| 28 | 26, 27 | isusgrs 29173 |
. . 3
⊢ (𝐻 ∈ 𝑊 → (𝐻 ∈ USGraph ↔ (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (♯‘𝑥) = 2})) |
| 29 | 28 | 3ad2ant1 1134 |
. 2
⊢ ((𝐻 ∈ 𝑊 ∧ (Vtx‘𝐻)𝐺(Edg‘𝐻) ∧ (iEdg‘𝐻) ∈ 𝑂) → (𝐻 ∈ USGraph ↔ (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (♯‘𝑥) = 2})) |
| 30 | 25, 29 | mpbird 257 |
1
⊢ ((𝐻 ∈ 𝑊 ∧ (Vtx‘𝐻)𝐺(Edg‘𝐻) ∧ (iEdg‘𝐻) ∈ 𝑂) → 𝐻 ∈ USGraph) |