Proof of Theorem ausisusgra
Step | Hyp | Ref
| Expression |
1 | | ausgra.1 |
. . 3
⊢ 𝐺 = {〈𝑣, 𝑒〉 ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (#‘𝑥) = 2}} |
2 | 1 | isausgra 25883 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉𝐺𝐸 ↔ 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
3 | | f1oi 6086 |
. . . 4
⊢ ( I
↾ 𝐸):𝐸–1-1-onto→𝐸 |
4 | | dff1o5 6059 |
. . . . 5
⊢ (( I
↾ 𝐸):𝐸–1-1-onto→𝐸 ↔ (( I ↾ 𝐸):𝐸–1-1→𝐸 ∧ ran ( I ↾ 𝐸) = 𝐸)) |
5 | | f1ss 6019 |
. . . . . . . . 9
⊢ ((( I
↾ 𝐸):𝐸–1-1→𝐸 ∧ 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) → ( I ↾ 𝐸):𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
6 | | dmresi 5376 |
. . . . . . . . . . 11
⊢ dom ( I
↾ 𝐸) = 𝐸 |
7 | 6 | eqcomi 2619 |
. . . . . . . . . 10
⊢ 𝐸 = dom ( I ↾ 𝐸) |
8 | | f1eq2 6010 |
. . . . . . . . . 10
⊢ (𝐸 = dom ( I ↾ 𝐸) → (( I ↾ 𝐸):𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ↔ ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . 9
⊢ (( I
↾ 𝐸):𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ↔ ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
10 | 5, 9 | sylib 207 |
. . . . . . . 8
⊢ ((( I
↾ 𝐸):𝐸–1-1→𝐸 ∧ 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) → ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
11 | 10 | ex 449 |
. . . . . . 7
⊢ (( I
↾ 𝐸):𝐸–1-1→𝐸 → (𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
12 | 11 | a1d 25 |
. . . . . 6
⊢ (( I
↾ 𝐸):𝐸–1-1→𝐸 → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}))) |
13 | 12 | adantr 480 |
. . . . 5
⊢ ((( I
↾ 𝐸):𝐸–1-1→𝐸 ∧ ran ( I ↾ 𝐸) = 𝐸) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}))) |
14 | 4, 13 | sylbi 206 |
. . . 4
⊢ (( I
↾ 𝐸):𝐸–1-1-onto→𝐸 → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}))) |
15 | 3, 14 | ax-mp 5 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
16 | | f1f 6014 |
. . . . 5
⊢ (( I
↾ 𝐸):dom ( I ↾
𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → ( I ↾ 𝐸):dom ( I ↾ 𝐸)⟶{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
17 | | df-f 5808 |
. . . . . 6
⊢ (( I
↾ 𝐸):dom ( I ↾
𝐸)⟶{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ↔ (( I ↾ 𝐸) Fn dom ( I ↾ 𝐸) ∧ ran ( I ↾ 𝐸) ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
18 | | rnresi 5398 |
. . . . . . . . . 10
⊢ ran ( I
↾ 𝐸) = 𝐸 |
19 | 18 | sseq1i 3592 |
. . . . . . . . 9
⊢ (ran ( I
↾ 𝐸) ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ↔ 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
20 | 19 | biimpi 205 |
. . . . . . . 8
⊢ (ran ( I
↾ 𝐸) ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
21 | 20 | a1d 25 |
. . . . . . 7
⊢ (ran ( I
↾ 𝐸) ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
22 | 21 | adantl 481 |
. . . . . 6
⊢ ((( I
↾ 𝐸) Fn dom ( I
↾ 𝐸) ∧ ran ( I
↾ 𝐸) ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
23 | 17, 22 | sylbi 206 |
. . . . 5
⊢ (( I
↾ 𝐸):dom ( I ↾
𝐸)⟶{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
24 | 16, 23 | syl 17 |
. . . 4
⊢ (( I
↾ 𝐸):dom ( I ↾
𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
25 | 24 | com12 32 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
26 | 15, 25 | impbid 201 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ↔ ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
27 | | resiexg 6994 |
. . 3
⊢ (𝐸 ∈ 𝑌 → ( I ↾ 𝐸) ∈ V) |
28 | | isusgra0 25876 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ ( I ↾ 𝐸) ∈ V) → (𝑉 USGrph ( I ↾ 𝐸) ↔ ( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
29 | 28 | bicomd 212 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ ( I ↾ 𝐸) ∈ V) → (( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ↔ 𝑉 USGrph ( I ↾ 𝐸))) |
30 | 27, 29 | sylan2 490 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (( I ↾ 𝐸):dom ( I ↾ 𝐸)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ↔ 𝑉 USGrph ( I ↾ 𝐸))) |
31 | 2, 26, 30 | 3bitrd 293 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉𝐺𝐸 ↔ 𝑉 USGrph ( I ↾ 𝐸))) |