Proof of Theorem ausgrusgrb
Step | Hyp | Ref
| Expression |
1 | | ausgr.1 |
. . 3
⊢ 𝐺 = {〈𝑣, 𝑒〉 ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (#‘𝑥) = 2}} |
2 | 1 | isausgr 40394 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉𝐺𝐸 ↔ 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
3 | | f1oi 6086 |
. . . . 5
⊢ ( I
↾ 𝐸):𝐸–1-1-onto→𝐸 |
4 | | dff1o5 6059 |
. . . . . 6
⊢ (( I
↾ 𝐸):𝐸–1-1-onto→𝐸 ↔ (( I ↾ 𝐸):𝐸–1-1→𝐸 ∧ ran ( I ↾ 𝐸) = 𝐸)) |
5 | | f1ss 6019 |
. . . . . . . . . 10
⊢ ((( I
↾ 𝐸):𝐸–1-1→𝐸 ∧ 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) → ( I ↾ 𝐸):𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
6 | | dmresi 5376 |
. . . . . . . . . . . 12
⊢ dom ( I
↾ 𝐸) = 𝐸 |
7 | 6 | eqcomi 2619 |
. . . . . . . . . . 11
⊢ 𝐸 = dom ( I ↾ 𝐸) |
8 | | f1eq2 6010 |
. . . . . . . . . . 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 207 |
. . . . . . . . 9
⊢ ((( I
↾ 𝐸):𝐸–1-1→𝐸 ∧ 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) → ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
11 | 10 | ex 449 |
. . . . . . . 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 206 |
. . . . 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 | | f1f 6014 |
. . . . . 6
⊢ (( I
↾ 𝐸):dom ( I ↾
𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → ( I ↾ 𝐸):dom ( I ↾ 𝐸)⟶{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
17 | | df-f 5808 |
. . . . . . 7
⊢ (( I
↾ 𝐸):dom ( I ↾
𝐸)⟶{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ↔ (( I ↾ 𝐸) Fn dom ( I ↾ 𝐸) ∧ ran ( I ↾ 𝐸) ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
18 | | rnresi 5398 |
. . . . . . . . . . 11
⊢ ran ( I
↾ 𝐸) = 𝐸 |
19 | 18 | sseq1i 3592 |
. . . . . . . . . 10
⊢ (ran ( I
↾ 𝐸) ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ↔ 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
20 | 19 | biimpi 205 |
. . . . . . . . 9
⊢ (ran ( I
↾ 𝐸) ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
21 | 20 | a1d 25 |
. . . . . . . 8
⊢ (ran ( I
↾ 𝐸) ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
22 | 21 | adantl 481 |
. . . . . . 7
⊢ ((( I
↾ 𝐸) Fn dom ( I
↾ 𝐸) ∧ ran ( I
↾ 𝐸) ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
23 | 17, 22 | sylbi 206 |
. . . . . 6
⊢ (( I
↾ 𝐸):dom ( I ↾
𝐸)⟶{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
24 | 16, 23 | syl 17 |
. . . . 5
⊢ (( I
↾ 𝐸):dom ( I ↾
𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
25 | 24 | com12 32 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
26 | 15, 25 | impbid 201 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ↔ ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
27 | | resiexg 6994 |
. . . . 5
⊢ (𝐸 ∈ 𝑌 → ( I ↾ 𝐸) ∈ V) |
28 | | opiedgfv 25684 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ ( I ↾ 𝐸) ∈ V) → (iEdg‘〈𝑉, ( I ↾ 𝐸)〉) = ( I ↾ 𝐸)) |
29 | 27, 28 | sylan2 490 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘〈𝑉, ( I ↾ 𝐸)〉) = ( I ↾ 𝐸)) |
30 | 29 | dmeqd 5248 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → dom (iEdg‘〈𝑉, ( I ↾ 𝐸)〉) = dom ( I ↾ 𝐸)) |
31 | | opvtxfv 25681 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑋 ∧ ( I ↾ 𝐸) ∈ V) → (Vtx‘〈𝑉, ( I ↾ 𝐸)〉) = 𝑉) |
32 | 27, 31 | sylan2 490 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘〈𝑉, ( I ↾ 𝐸)〉) = 𝑉) |
33 | 32 | pweqd 4113 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝒫 (Vtx‘〈𝑉, ( I ↾ 𝐸)〉) = 𝒫 𝑉) |
34 | 33 | rabeqdv 3167 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → {𝑥 ∈ 𝒫 (Vtx‘〈𝑉, ( I ↾ 𝐸)〉) ∣ (#‘𝑥) = 2} = {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
35 | 29, 30, 34 | f1eq123d 6044 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((iEdg‘〈𝑉, ( I ↾ 𝐸)〉):dom (iEdg‘〈𝑉, ( I ↾ 𝐸)〉)–1-1→{𝑥 ∈ 𝒫 (Vtx‘〈𝑉, ( I ↾ 𝐸)〉) ∣ (#‘𝑥) = 2} ↔ ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
36 | 26, 35 | bitr4d 270 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ↔ (iEdg‘〈𝑉, ( I ↾ 𝐸)〉):dom (iEdg‘〈𝑉, ( I ↾ 𝐸)〉)–1-1→{𝑥 ∈ 𝒫 (Vtx‘〈𝑉, ( I ↾ 𝐸)〉) ∣ (#‘𝑥) = 2})) |
37 | | opex 4859 |
. . . . 5
⊢
〈𝑉, ( I ↾
𝐸)〉 ∈
V |
38 | | eqid 2610 |
. . . . . 6
⊢
(Vtx‘〈𝑉,
( I ↾ 𝐸)〉) =
(Vtx‘〈𝑉, ( I
↾ 𝐸)〉) |
39 | | eqid 2610 |
. . . . . 6
⊢
(iEdg‘〈𝑉,
( I ↾ 𝐸)〉) =
(iEdg‘〈𝑉, ( I
↾ 𝐸)〉) |
40 | 38, 39 | isusgrs 40386 |
. . . . 5
⊢
(〈𝑉, ( I
↾ 𝐸)〉 ∈ V
→ (〈𝑉, ( I
↾ 𝐸)〉 ∈
USGraph ↔ (iEdg‘〈𝑉, ( I ↾ 𝐸)〉):dom (iEdg‘〈𝑉, ( I ↾ 𝐸)〉)–1-1→{𝑥 ∈ 𝒫 (Vtx‘〈𝑉, ( I ↾ 𝐸)〉) ∣ (#‘𝑥) = 2})) |
41 | 37, 40 | ax-mp 5 |
. . . 4
⊢
(〈𝑉, ( I
↾ 𝐸)〉 ∈
USGraph ↔ (iEdg‘〈𝑉, ( I ↾ 𝐸)〉):dom (iEdg‘〈𝑉, ( I ↾ 𝐸)〉)–1-1→{𝑥 ∈ 𝒫 (Vtx‘〈𝑉, ( I ↾ 𝐸)〉) ∣ (#‘𝑥) = 2}) |
42 | 41 | bicomi 213 |
. . 3
⊢
((iEdg‘〈𝑉, ( I ↾ 𝐸)〉):dom (iEdg‘〈𝑉, ( I ↾ 𝐸)〉)–1-1→{𝑥 ∈ 𝒫 (Vtx‘〈𝑉, ( I ↾ 𝐸)〉) ∣ (#‘𝑥) = 2} ↔ 〈𝑉, ( I ↾ 𝐸)〉 ∈ USGraph ) |
43 | 42 | a1i 11 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((iEdg‘〈𝑉, ( I ↾ 𝐸)〉):dom (iEdg‘〈𝑉, ( I ↾ 𝐸)〉)–1-1→{𝑥 ∈ 𝒫 (Vtx‘〈𝑉, ( I ↾ 𝐸)〉) ∣ (#‘𝑥) = 2} ↔ 〈𝑉, ( I ↾ 𝐸)〉 ∈ USGraph )) |
44 | 2, 36, 43 | 3bitrd 293 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉𝐺𝐸 ↔ 〈𝑉, ( I ↾ 𝐸)〉 ∈ USGraph )) |