Proof of Theorem ausgrusgrb
| Step | Hyp | Ref
| Expression |
| 1 | | ausgr.1 |
. . 3
⊢ 𝐺 = {〈𝑣, 𝑒〉 ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (♯‘𝑥) = 2}} |
| 2 | 1 | isausgr 29181 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉𝐺𝐸 ↔ 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})) |
| 3 | | f1oi 6886 |
. . . . 5
⊢ ( I
↾ 𝐸):𝐸–1-1-onto→𝐸 |
| 4 | | dff1o5 6857 |
. . . . . 6
⊢ (( I
↾ 𝐸):𝐸–1-1-onto→𝐸 ↔ (( I ↾ 𝐸):𝐸–1-1→𝐸 ∧ ran ( I ↾ 𝐸) = 𝐸)) |
| 5 | | f1ss 6809 |
. . . . . . . . . 10
⊢ ((( I
↾ 𝐸):𝐸–1-1→𝐸 ∧ 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) → ( I ↾ 𝐸):𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) |
| 6 | | dmresi 6070 |
. . . . . . . . . . . 12
⊢ dom ( I
↾ 𝐸) = 𝐸 |
| 7 | 6 | eqcomi 2746 |
. . . . . . . . . . 11
⊢ 𝐸 = dom ( I ↾ 𝐸) |
| 8 | | f1eq2 6800 |
. . . . . . . . . . 11
⊢ (𝐸 = dom ( I ↾ 𝐸) → (( I ↾ 𝐸):𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ↔ ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})) |
| 9 | 7, 8 | ax-mp 5 |
. . . . . . . . . 10
⊢ (( I
↾ 𝐸):𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ↔ ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) |
| 10 | 5, 9 | sylib 218 |
. . . . . . . . 9
⊢ ((( I
↾ 𝐸):𝐸–1-1→𝐸 ∧ 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) → ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) |
| 11 | 10 | ex 412 |
. . . . . . . 8
⊢ (( I
↾ 𝐸):𝐸–1-1→𝐸 → (𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} → ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})) |
| 12 | 11 | a1d 25 |
. . . . . . 7
⊢ (( I
↾ 𝐸):𝐸–1-1→𝐸 → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} → ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}))) |
| 13 | 12 | adantr 480 |
. . . . . 6
⊢ ((( I
↾ 𝐸):𝐸–1-1→𝐸 ∧ ran ( I ↾ 𝐸) = 𝐸) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} → ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}))) |
| 14 | 4, 13 | sylbi 217 |
. . . . 5
⊢ (( I
↾ 𝐸):𝐸–1-1-onto→𝐸 → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} → ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}))) |
| 15 | 3, 14 | ax-mp 5 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} → ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})) |
| 16 | | df-f 6565 |
. . . . . 6
⊢ (( I
↾ 𝐸):dom ( I ↾
𝐸)⟶{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ↔ (( I ↾ 𝐸) Fn dom ( I ↾ 𝐸) ∧ ran ( I ↾ 𝐸) ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})) |
| 17 | | rnresi 6093 |
. . . . . . . . 9
⊢ ran ( I
↾ 𝐸) = 𝐸 |
| 18 | 17 | sseq1i 4012 |
. . . . . . . 8
⊢ (ran ( I
↾ 𝐸) ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ↔ 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) |
| 19 | 18 | biimpi 216 |
. . . . . . 7
⊢ (ran ( I
↾ 𝐸) ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} → 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) |
| 20 | 19 | a1d 25 |
. . . . . 6
⊢ (ran ( I
↾ 𝐸) ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})) |
| 21 | 16, 20 | simplbiim 504 |
. . . . 5
⊢ (( I
↾ 𝐸):dom ( I ↾
𝐸)⟶{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})) |
| 22 | | f1f 6804 |
. . . . 5
⊢ (( I
↾ 𝐸):dom ( I ↾
𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} → ( I ↾ 𝐸):dom ( I ↾ 𝐸)⟶{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) |
| 23 | 21, 22 | syl11 33 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} → 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})) |
| 24 | 15, 23 | impbid 212 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ↔ ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})) |
| 25 | | resiexg 7934 |
. . . . 5
⊢ (𝐸 ∈ 𝑌 → ( I ↾ 𝐸) ∈ V) |
| 26 | | opiedgfv 29024 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ ( I ↾ 𝐸) ∈ V) → (iEdg‘〈𝑉, ( I ↾ 𝐸)〉) = ( I ↾ 𝐸)) |
| 27 | 25, 26 | sylan2 593 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘〈𝑉, ( I ↾ 𝐸)〉) = ( I ↾ 𝐸)) |
| 28 | 27 | dmeqd 5916 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → dom (iEdg‘〈𝑉, ( I ↾ 𝐸)〉) = dom ( I ↾ 𝐸)) |
| 29 | | opvtxfv 29021 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑋 ∧ ( I ↾ 𝐸) ∈ V) → (Vtx‘〈𝑉, ( I ↾ 𝐸)〉) = 𝑉) |
| 30 | 25, 29 | sylan2 593 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘〈𝑉, ( I ↾ 𝐸)〉) = 𝑉) |
| 31 | 30 | pweqd 4617 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝒫 (Vtx‘〈𝑉, ( I ↾ 𝐸)〉) = 𝒫 𝑉) |
| 32 | 31 | rabeqdv 3452 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → {𝑥 ∈ 𝒫 (Vtx‘〈𝑉, ( I ↾ 𝐸)〉) ∣ (♯‘𝑥) = 2} = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) |
| 33 | 27, 28, 32 | f1eq123d 6840 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((iEdg‘〈𝑉, ( I ↾ 𝐸)〉):dom (iEdg‘〈𝑉, ( I ↾ 𝐸)〉)–1-1→{𝑥 ∈ 𝒫 (Vtx‘〈𝑉, ( I ↾ 𝐸)〉) ∣ (♯‘𝑥) = 2} ↔ ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})) |
| 34 | 24, 33 | bitr4d 282 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ↔ (iEdg‘〈𝑉, ( I ↾ 𝐸)〉):dom (iEdg‘〈𝑉, ( I ↾ 𝐸)〉)–1-1→{𝑥 ∈ 𝒫 (Vtx‘〈𝑉, ( I ↾ 𝐸)〉) ∣ (♯‘𝑥) = 2})) |
| 35 | | opex 5469 |
. . . . 5
⊢
〈𝑉, ( I ↾
𝐸)〉 ∈
V |
| 36 | | eqid 2737 |
. . . . . 6
⊢
(Vtx‘〈𝑉,
( I ↾ 𝐸)〉) =
(Vtx‘〈𝑉, ( I
↾ 𝐸)〉) |
| 37 | | eqid 2737 |
. . . . . 6
⊢
(iEdg‘〈𝑉,
( I ↾ 𝐸)〉) =
(iEdg‘〈𝑉, ( I
↾ 𝐸)〉) |
| 38 | 36, 37 | isusgrs 29173 |
. . . . 5
⊢
(〈𝑉, ( I
↾ 𝐸)〉 ∈ V
→ (〈𝑉, ( I
↾ 𝐸)〉 ∈
USGraph ↔ (iEdg‘〈𝑉, ( I ↾ 𝐸)〉):dom (iEdg‘〈𝑉, ( I ↾ 𝐸)〉)–1-1→{𝑥 ∈ 𝒫 (Vtx‘〈𝑉, ( I ↾ 𝐸)〉) ∣ (♯‘𝑥) = 2})) |
| 39 | 35, 38 | ax-mp 5 |
. . . 4
⊢
(〈𝑉, ( I
↾ 𝐸)〉 ∈
USGraph ↔ (iEdg‘〈𝑉, ( I ↾ 𝐸)〉):dom (iEdg‘〈𝑉, ( I ↾ 𝐸)〉)–1-1→{𝑥 ∈ 𝒫 (Vtx‘〈𝑉, ( I ↾ 𝐸)〉) ∣ (♯‘𝑥) = 2}) |
| 40 | 39 | bicomi 224 |
. . 3
⊢
((iEdg‘〈𝑉, ( I ↾ 𝐸)〉):dom (iEdg‘〈𝑉, ( I ↾ 𝐸)〉)–1-1→{𝑥 ∈ 𝒫 (Vtx‘〈𝑉, ( I ↾ 𝐸)〉) ∣ (♯‘𝑥) = 2} ↔ 〈𝑉, ( I ↾ 𝐸)〉 ∈ USGraph) |
| 41 | 40 | a1i 11 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((iEdg‘〈𝑉, ( I ↾ 𝐸)〉):dom (iEdg‘〈𝑉, ( I ↾ 𝐸)〉)–1-1→{𝑥 ∈ 𝒫 (Vtx‘〈𝑉, ( I ↾ 𝐸)〉) ∣ (♯‘𝑥) = 2} ↔ 〈𝑉, ( I ↾ 𝐸)〉 ∈ USGraph)) |
| 42 | 2, 34, 41 | 3bitrd 305 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉𝐺𝐸 ↔ 〈𝑉, ( I ↾ 𝐸)〉 ∈ USGraph)) |