Proof of Theorem uhgraeq12d
Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . 4
⊢ ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → 𝐸 = 𝐹) |
2 | | dmeq 5246 |
. . . . 5
⊢ (𝐸 = 𝐹 → dom 𝐸 = dom 𝐹) |
3 | 2 | adantl 481 |
. . . 4
⊢ ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → dom 𝐸 = dom 𝐹) |
4 | | pweq 4111 |
. . . . . 6
⊢ (𝑉 = 𝑊 → 𝒫 𝑉 = 𝒫 𝑊) |
5 | 4 | difeq1d 3689 |
. . . . 5
⊢ (𝑉 = 𝑊 → (𝒫 𝑉 ∖ {∅}) = (𝒫 𝑊 ∖
{∅})) |
6 | 5 | adantr 480 |
. . . 4
⊢ ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → (𝒫 𝑉 ∖ {∅}) = (𝒫 𝑊 ∖
{∅})) |
7 | 1, 3, 6 | feq123d 5947 |
. . 3
⊢ ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → (𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}) ↔ 𝐹:dom 𝐹⟶(𝒫 𝑊 ∖ {∅}))) |
8 | 7 | adantl 481 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → (𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}) ↔ 𝐹:dom 𝐹⟶(𝒫 𝑊 ∖ {∅}))) |
9 | | isuhgra 25827 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 UHGrph 𝐸 ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))) |
10 | 9 | adantr 480 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → (𝑉 UHGrph 𝐸 ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))) |
11 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑉 = 𝑊 → (𝑉 ∈ 𝑋 ↔ 𝑊 ∈ 𝑋)) |
12 | 11 | biimpd 218 |
. . . . . . 7
⊢ (𝑉 = 𝑊 → (𝑉 ∈ 𝑋 → 𝑊 ∈ 𝑋)) |
13 | 12 | adantr 480 |
. . . . . 6
⊢ ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → (𝑉 ∈ 𝑋 → 𝑊 ∈ 𝑋)) |
14 | 13 | com12 32 |
. . . . 5
⊢ (𝑉 ∈ 𝑋 → ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → 𝑊 ∈ 𝑋)) |
15 | 14 | adantr 480 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → 𝑊 ∈ 𝑋)) |
16 | 15 | imp 444 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → 𝑊 ∈ 𝑋) |
17 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝐸 = 𝐹 → (𝐸 ∈ 𝑌 ↔ 𝐹 ∈ 𝑌)) |
18 | 17 | biimpd 218 |
. . . . . . 7
⊢ (𝐸 = 𝐹 → (𝐸 ∈ 𝑌 → 𝐹 ∈ 𝑌)) |
19 | 18 | adantl 481 |
. . . . . 6
⊢ ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → (𝐸 ∈ 𝑌 → 𝐹 ∈ 𝑌)) |
20 | 19 | com12 32 |
. . . . 5
⊢ (𝐸 ∈ 𝑌 → ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → 𝐹 ∈ 𝑌)) |
21 | 20 | adantl 481 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → 𝐹 ∈ 𝑌)) |
22 | 21 | imp 444 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → 𝐹 ∈ 𝑌) |
23 | | isuhgra 25827 |
. . 3
⊢ ((𝑊 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌) → (𝑊 UHGrph 𝐹 ↔ 𝐹:dom 𝐹⟶(𝒫 𝑊 ∖ {∅}))) |
24 | 16, 22, 23 | syl2anc 691 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → (𝑊 UHGrph 𝐹 ↔ 𝐹:dom 𝐹⟶(𝒫 𝑊 ∖ {∅}))) |
25 | 8, 10, 24 | 3bitr4d 299 |
1
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → (𝑉 UHGrph 𝐸 ↔ 𝑊 UHGrph 𝐹)) |