Step | Hyp | Ref
| Expression |
1 | | frgrwopreg.a |
. . . . . 6
⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} |
2 | 1 | rabeq2i 3197 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝑉 ∧ (𝐷‘𝑥) = 𝐾)) |
3 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = 𝑎 → (𝐷‘𝑥) = (𝐷‘𝑎)) |
4 | 3 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑥 = 𝑎 → ((𝐷‘𝑥) = 𝐾 ↔ (𝐷‘𝑎) = 𝐾)) |
5 | 4, 1 | elrab2 3366 |
. . . . . 6
⊢ (𝑎 ∈ 𝐴 ↔ (𝑎 ∈ 𝑉 ∧ (𝐷‘𝑎) = 𝐾)) |
6 | | eqtr3 2643 |
. . . . . . . . 9
⊢ (((𝐷‘𝑎) = 𝐾 ∧ (𝐷‘𝑥) = 𝐾) → (𝐷‘𝑎) = (𝐷‘𝑥)) |
7 | 6 | expcom 451 |
. . . . . . . 8
⊢ ((𝐷‘𝑥) = 𝐾 → ((𝐷‘𝑎) = 𝐾 → (𝐷‘𝑎) = (𝐷‘𝑥))) |
8 | 7 | adantl 482 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑉 ∧ (𝐷‘𝑥) = 𝐾) → ((𝐷‘𝑎) = 𝐾 → (𝐷‘𝑎) = (𝐷‘𝑥))) |
9 | 8 | com12 32 |
. . . . . 6
⊢ ((𝐷‘𝑎) = 𝐾 → ((𝑥 ∈ 𝑉 ∧ (𝐷‘𝑥) = 𝐾) → (𝐷‘𝑎) = (𝐷‘𝑥))) |
10 | 5, 9 | simplbiim 659 |
. . . . 5
⊢ (𝑎 ∈ 𝐴 → ((𝑥 ∈ 𝑉 ∧ (𝐷‘𝑥) = 𝐾) → (𝐷‘𝑎) = (𝐷‘𝑥))) |
11 | 2, 10 | syl5bi 232 |
. . . 4
⊢ (𝑎 ∈ 𝐴 → (𝑥 ∈ 𝐴 → (𝐷‘𝑎) = (𝐷‘𝑥))) |
12 | 11 | imp 445 |
. . 3
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐷‘𝑎) = (𝐷‘𝑥)) |
13 | 12 | adantr 481 |
. 2
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐷‘𝑎) = (𝐷‘𝑥)) |
14 | | frgrwopreg.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
15 | | frgrwopreg.d |
. . . 4
⊢ 𝐷 = (VtxDeg‘𝐺) |
16 | | frgrwopreg.b |
. . . 4
⊢ 𝐵 = (𝑉 ∖ 𝐴) |
17 | 14, 15, 1, 16 | frgrwopreglem3 27178 |
. . 3
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐷‘𝑎) ≠ (𝐷‘𝑏)) |
18 | 17 | ad2ant2r 783 |
. 2
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐷‘𝑎) ≠ (𝐷‘𝑏)) |
19 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝐷‘𝑥) = (𝐷‘𝑧)) |
20 | 19 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑥 = 𝑧 → ((𝐷‘𝑥) = 𝐾 ↔ (𝐷‘𝑧) = 𝐾)) |
21 | 20 | cbvrabv 3199 |
. . . . 5
⊢ {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} = {𝑧 ∈ 𝑉 ∣ (𝐷‘𝑧) = 𝐾} |
22 | 1, 21 | eqtri 2644 |
. . . 4
⊢ 𝐴 = {𝑧 ∈ 𝑉 ∣ (𝐷‘𝑧) = 𝐾} |
23 | 14, 15, 22, 16 | frgrwopreglem3 27178 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝐷‘𝑥) ≠ (𝐷‘𝑦)) |
24 | 23 | ad2ant2l 782 |
. 2
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐷‘𝑥) ≠ (𝐷‘𝑦)) |
25 | 13, 18, 24 | 3jca 1242 |
1
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐷‘𝑎) = (𝐷‘𝑥) ∧ (𝐷‘𝑎) ≠ (𝐷‘𝑏) ∧ (𝐷‘𝑥) ≠ (𝐷‘𝑦))) |