Proof of Theorem ausgrusgri
Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . . . 5
⊢
(Vtx‘𝐻) ∈
V |
2 | | fvex 6113 |
. . . . 5
⊢
(Edg‘𝐻) ∈
V |
3 | | ausgr.1 |
. . . . . 6
⊢ 𝐺 = {〈𝑣, 𝑒〉 ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (#‘𝑥) = 2}} |
4 | 3 | isausgr 40394 |
. . . . 5
⊢
(((Vtx‘𝐻)
∈ V ∧ (Edg‘𝐻) ∈ V) → ((Vtx‘𝐻)𝐺(Edg‘𝐻) ↔ (Edg‘𝐻) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (#‘𝑥) = 2})) |
5 | 1, 2, 4 | mp2an 704 |
. . . 4
⊢
((Vtx‘𝐻)𝐺(Edg‘𝐻) ↔ (Edg‘𝐻) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (#‘𝑥) = 2}) |
6 | | edgaval 25794 |
. . . . . 6
⊢ (𝐻 ∈ 𝑊 → (Edg‘𝐻) = ran (iEdg‘𝐻)) |
7 | 6 | sseq1d 3595 |
. . . . 5
⊢ (𝐻 ∈ 𝑊 → ((Edg‘𝐻) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (#‘𝑥) = 2} ↔ ran
(iEdg‘𝐻) ⊆
{𝑥 ∈ 𝒫
(Vtx‘𝐻) ∣
(#‘𝑥) =
2})) |
8 | | ausgrusgri.1 |
. . . . . . . . . 10
⊢ 𝑂 = {𝑓 ∣ 𝑓:dom 𝑓–1-1→ran 𝑓} |
9 | 8 | eleq2i 2680 |
. . . . . . . . 9
⊢
((iEdg‘𝐻)
∈ 𝑂 ↔
(iEdg‘𝐻) ∈
{𝑓 ∣ 𝑓:dom 𝑓–1-1→ran 𝑓}) |
10 | | fvex 6113 |
. . . . . . . . . 10
⊢
(iEdg‘𝐻)
∈ V |
11 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑓 = (iEdg‘𝐻) → 𝑓 = (iEdg‘𝐻)) |
12 | | dmeq 5246 |
. . . . . . . . . . 11
⊢ (𝑓 = (iEdg‘𝐻) → dom 𝑓 = dom (iEdg‘𝐻)) |
13 | | rneq 5272 |
. . . . . . . . . . 11
⊢ (𝑓 = (iEdg‘𝐻) → ran 𝑓 = ran (iEdg‘𝐻)) |
14 | 11, 12, 13 | f1eq123d 6044 |
. . . . . . . . . 10
⊢ (𝑓 = (iEdg‘𝐻) → (𝑓:dom 𝑓–1-1→ran 𝑓 ↔ (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→ran (iEdg‘𝐻))) |
15 | 10, 14 | elab 3319 |
. . . . . . . . 9
⊢
((iEdg‘𝐻)
∈ {𝑓 ∣ 𝑓:dom 𝑓–1-1→ran 𝑓} ↔ (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→ran (iEdg‘𝐻)) |
16 | 9, 15 | sylbb 208 |
. . . . . . . 8
⊢
((iEdg‘𝐻)
∈ 𝑂 →
(iEdg‘𝐻):dom
(iEdg‘𝐻)–1-1→ran (iEdg‘𝐻)) |
17 | 16 | 3ad2ant3 1077 |
. . . . . . 7
⊢ ((𝐻 ∈ 𝑊 ∧ ran (iEdg‘𝐻) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (#‘𝑥) = 2} ∧ (iEdg‘𝐻) ∈ 𝑂) → (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→ran (iEdg‘𝐻)) |
18 | | simp2 1055 |
. . . . . . 7
⊢ ((𝐻 ∈ 𝑊 ∧ ran (iEdg‘𝐻) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (#‘𝑥) = 2} ∧ (iEdg‘𝐻) ∈ 𝑂) → ran (iEdg‘𝐻) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (#‘𝑥) = 2}) |
19 | | f1ssr 6020 |
. . . . . . 7
⊢
(((iEdg‘𝐻):dom
(iEdg‘𝐻)–1-1→ran (iEdg‘𝐻) ∧ ran (iEdg‘𝐻) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (#‘𝑥) = 2}) → (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (#‘𝑥) = 2}) |
20 | 17, 18, 19 | syl2anc 691 |
. . . . . 6
⊢ ((𝐻 ∈ 𝑊 ∧ ran (iEdg‘𝐻) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (#‘𝑥) = 2} ∧ (iEdg‘𝐻) ∈ 𝑂) → (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (#‘𝑥) = 2}) |
21 | 20 | 3exp 1256 |
. . . . 5
⊢ (𝐻 ∈ 𝑊 → (ran (iEdg‘𝐻) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (#‘𝑥) = 2} → ((iEdg‘𝐻) ∈ 𝑂 → (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (#‘𝑥) = 2}))) |
22 | 7, 21 | sylbid 229 |
. . . 4
⊢ (𝐻 ∈ 𝑊 → ((Edg‘𝐻) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (#‘𝑥) = 2} → ((iEdg‘𝐻) ∈ 𝑂 → (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (#‘𝑥) = 2}))) |
23 | 5, 22 | syl5bi 231 |
. . 3
⊢ (𝐻 ∈ 𝑊 → ((Vtx‘𝐻)𝐺(Edg‘𝐻) → ((iEdg‘𝐻) ∈ 𝑂 → (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (#‘𝑥) = 2}))) |
24 | 23 | 3imp 1249 |
. 2
⊢ ((𝐻 ∈ 𝑊 ∧ (Vtx‘𝐻)𝐺(Edg‘𝐻) ∧ (iEdg‘𝐻) ∈ 𝑂) → (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (#‘𝑥) = 2}) |
25 | | eqid 2610 |
. . . 4
⊢
(Vtx‘𝐻) =
(Vtx‘𝐻) |
26 | | eqid 2610 |
. . . 4
⊢
(iEdg‘𝐻) =
(iEdg‘𝐻) |
27 | 25, 26 | isusgrs 40386 |
. . 3
⊢ (𝐻 ∈ 𝑊 → (𝐻 ∈ USGraph ↔ (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (#‘𝑥) = 2})) |
28 | 27 | 3ad2ant1 1075 |
. 2
⊢ ((𝐻 ∈ 𝑊 ∧ (Vtx‘𝐻)𝐺(Edg‘𝐻) ∧ (iEdg‘𝐻) ∈ 𝑂) → (𝐻 ∈ USGraph ↔ (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐻) ∣ (#‘𝑥) = 2})) |
29 | 24, 28 | mpbird 246 |
1
⊢ ((𝐻 ∈ 𝑊 ∧ (Vtx‘𝐻)𝐺(Edg‘𝐻) ∧ (iEdg‘𝐻) ∈ 𝑂) → 𝐻 ∈ USGraph ) |