Step | Hyp | Ref
| Expression |
1 | | simprr 792 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → 𝐸 = 𝐹) |
2 | | dmeq 5246 |
. . . . 5
⊢ (𝐸 = 𝐹 → dom 𝐸 = dom 𝐹) |
3 | 2 | adantl 481 |
. . . 4
⊢ ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → dom 𝐸 = dom 𝐹) |
4 | 3 | adantl 481 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → dom 𝐸 = dom 𝐹) |
5 | | pweq 4111 |
. . . . . . 7
⊢ (𝑉 = 𝑊 → 𝒫 𝑉 = 𝒫 𝑊) |
6 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → 𝒫 𝑉 = 𝒫 𝑊) |
7 | 6 | adantl 481 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → 𝒫 𝑉 = 𝒫 𝑊) |
8 | 7 | difeq1d 3689 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → (𝒫 𝑉 ∖ {∅}) = (𝒫 𝑊 ∖
{∅})) |
9 | 8 | rabeqdv 3167 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) = 2} = {𝑥 ∈ (𝒫 𝑊 ∖ {∅}) ∣ (#‘𝑥) = 2}) |
10 | 1, 4, 9 | f1eq123d 6044 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → (𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) = 2} ↔ 𝐹:dom 𝐹–1-1→{𝑥 ∈ (𝒫 𝑊 ∖ {∅}) ∣ (#‘𝑥) = 2})) |
11 | | isusgra 25873 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 USGrph 𝐸 ↔ 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) = 2})) |
12 | 11 | adantr 480 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → (𝑉 USGrph 𝐸 ↔ 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) = 2})) |
13 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑉 = 𝑊 → (𝑉 ∈ 𝑋 ↔ 𝑊 ∈ 𝑋)) |
14 | 13 | biimpd 218 |
. . . . . . 7
⊢ (𝑉 = 𝑊 → (𝑉 ∈ 𝑋 → 𝑊 ∈ 𝑋)) |
15 | 14 | adantr 480 |
. . . . . 6
⊢ ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → (𝑉 ∈ 𝑋 → 𝑊 ∈ 𝑋)) |
16 | 15 | com12 32 |
. . . . 5
⊢ (𝑉 ∈ 𝑋 → ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → 𝑊 ∈ 𝑋)) |
17 | 16 | adantr 480 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → 𝑊 ∈ 𝑋)) |
18 | 17 | imp 444 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → 𝑊 ∈ 𝑋) |
19 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝐸 = 𝐹 → (𝐸 ∈ 𝑌 ↔ 𝐹 ∈ 𝑌)) |
20 | 19 | biimpd 218 |
. . . . . . 7
⊢ (𝐸 = 𝐹 → (𝐸 ∈ 𝑌 → 𝐹 ∈ 𝑌)) |
21 | 20 | adantl 481 |
. . . . . 6
⊢ ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → (𝐸 ∈ 𝑌 → 𝐹 ∈ 𝑌)) |
22 | 21 | com12 32 |
. . . . 5
⊢ (𝐸 ∈ 𝑌 → ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → 𝐹 ∈ 𝑌)) |
23 | 22 | adantl 481 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → 𝐹 ∈ 𝑌)) |
24 | 23 | imp 444 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → 𝐹 ∈ 𝑌) |
25 | | isusgra 25873 |
. . 3
⊢ ((𝑊 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌) → (𝑊 USGrph 𝐹 ↔ 𝐹:dom 𝐹–1-1→{𝑥 ∈ (𝒫 𝑊 ∖ {∅}) ∣ (#‘𝑥) = 2})) |
26 | 18, 24, 25 | syl2anc 691 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → (𝑊 USGrph 𝐹 ↔ 𝐹:dom 𝐹–1-1→{𝑥 ∈ (𝒫 𝑊 ∖ {∅}) ∣ (#‘𝑥) = 2})) |
27 | 10, 12, 26 | 3bitr4d 299 |
1
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → (𝑉 USGrph 𝐸 ↔ 𝑊 USGrph 𝐹)) |