Proof of Theorem frgrawopreglem3
Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = 𝑋 → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑋)) |
2 | 1 | eqeq1d 2612 |
. . . 4
⊢ (𝑥 = 𝑋 → (((𝑉 VDeg 𝐸)‘𝑥) = 𝐾 ↔ ((𝑉 VDeg 𝐸)‘𝑋) = 𝐾)) |
3 | | frgrawopreg.a |
. . . 4
⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑥) = 𝐾} |
4 | 2, 3 | elrab2 3333 |
. . 3
⊢ (𝑋 ∈ 𝐴 ↔ (𝑋 ∈ 𝑉 ∧ ((𝑉 VDeg 𝐸)‘𝑋) = 𝐾)) |
5 | | frgrawopreg.b |
. . . . . 6
⊢ 𝐵 = (𝑉 ∖ 𝐴) |
6 | 5 | eleq2i 2680 |
. . . . 5
⊢ (𝑌 ∈ 𝐵 ↔ 𝑌 ∈ (𝑉 ∖ 𝐴)) |
7 | | eldif 3550 |
. . . . 5
⊢ (𝑌 ∈ (𝑉 ∖ 𝐴) ↔ (𝑌 ∈ 𝑉 ∧ ¬ 𝑌 ∈ 𝐴)) |
8 | 6, 7 | bitri 263 |
. . . 4
⊢ (𝑌 ∈ 𝐵 ↔ (𝑌 ∈ 𝑉 ∧ ¬ 𝑌 ∈ 𝐴)) |
9 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = 𝑌 → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑌)) |
10 | 9 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑥 = 𝑌 → (((𝑉 VDeg 𝐸)‘𝑥) = 𝐾 ↔ ((𝑉 VDeg 𝐸)‘𝑌) = 𝐾)) |
11 | 10, 3 | elrab2 3333 |
. . . . . . 7
⊢ (𝑌 ∈ 𝐴 ↔ (𝑌 ∈ 𝑉 ∧ ((𝑉 VDeg 𝐸)‘𝑌) = 𝐾)) |
12 | | ianor 508 |
. . . . . . . 8
⊢ (¬
(𝑌 ∈ 𝑉 ∧ ((𝑉 VDeg 𝐸)‘𝑌) = 𝐾) ↔ (¬ 𝑌 ∈ 𝑉 ∨ ¬ ((𝑉 VDeg 𝐸)‘𝑌) = 𝐾)) |
13 | | pm2.21 119 |
. . . . . . . . 9
⊢ (¬
𝑌 ∈ 𝑉 → (𝑌 ∈ 𝑉 → ((𝑋 ∈ 𝑉 ∧ ((𝑉 VDeg 𝐸)‘𝑋) = 𝐾) → ((𝑉 VDeg 𝐸)‘𝑋) ≠ ((𝑉 VDeg 𝐸)‘𝑌)))) |
14 | | nesym 2838 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ≠ ((𝑉 VDeg 𝐸)‘𝑌) ↔ ¬ ((𝑉 VDeg 𝐸)‘𝑌) = 𝐾) |
15 | 14 | biimpri 217 |
. . . . . . . . . . . . 13
⊢ (¬
((𝑉 VDeg 𝐸)‘𝑌) = 𝐾 → 𝐾 ≠ ((𝑉 VDeg 𝐸)‘𝑌)) |
16 | | neeq1 2844 |
. . . . . . . . . . . . 13
⊢ (((𝑉 VDeg 𝐸)‘𝑋) = 𝐾 → (((𝑉 VDeg 𝐸)‘𝑋) ≠ ((𝑉 VDeg 𝐸)‘𝑌) ↔ 𝐾 ≠ ((𝑉 VDeg 𝐸)‘𝑌))) |
17 | 15, 16 | syl5ibr 235 |
. . . . . . . . . . . 12
⊢ (((𝑉 VDeg 𝐸)‘𝑋) = 𝐾 → (¬ ((𝑉 VDeg 𝐸)‘𝑌) = 𝐾 → ((𝑉 VDeg 𝐸)‘𝑋) ≠ ((𝑉 VDeg 𝐸)‘𝑌))) |
18 | 17 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ ((𝑉 VDeg 𝐸)‘𝑋) = 𝐾) → (¬ ((𝑉 VDeg 𝐸)‘𝑌) = 𝐾 → ((𝑉 VDeg 𝐸)‘𝑋) ≠ ((𝑉 VDeg 𝐸)‘𝑌))) |
19 | 18 | com12 32 |
. . . . . . . . . 10
⊢ (¬
((𝑉 VDeg 𝐸)‘𝑌) = 𝐾 → ((𝑋 ∈ 𝑉 ∧ ((𝑉 VDeg 𝐸)‘𝑋) = 𝐾) → ((𝑉 VDeg 𝐸)‘𝑋) ≠ ((𝑉 VDeg 𝐸)‘𝑌))) |
20 | 19 | a1d 25 |
. . . . . . . . 9
⊢ (¬
((𝑉 VDeg 𝐸)‘𝑌) = 𝐾 → (𝑌 ∈ 𝑉 → ((𝑋 ∈ 𝑉 ∧ ((𝑉 VDeg 𝐸)‘𝑋) = 𝐾) → ((𝑉 VDeg 𝐸)‘𝑋) ≠ ((𝑉 VDeg 𝐸)‘𝑌)))) |
21 | 13, 20 | jaoi 393 |
. . . . . . . 8
⊢ ((¬
𝑌 ∈ 𝑉 ∨ ¬ ((𝑉 VDeg 𝐸)‘𝑌) = 𝐾) → (𝑌 ∈ 𝑉 → ((𝑋 ∈ 𝑉 ∧ ((𝑉 VDeg 𝐸)‘𝑋) = 𝐾) → ((𝑉 VDeg 𝐸)‘𝑋) ≠ ((𝑉 VDeg 𝐸)‘𝑌)))) |
22 | 12, 21 | sylbi 206 |
. . . . . . 7
⊢ (¬
(𝑌 ∈ 𝑉 ∧ ((𝑉 VDeg 𝐸)‘𝑌) = 𝐾) → (𝑌 ∈ 𝑉 → ((𝑋 ∈ 𝑉 ∧ ((𝑉 VDeg 𝐸)‘𝑋) = 𝐾) → ((𝑉 VDeg 𝐸)‘𝑋) ≠ ((𝑉 VDeg 𝐸)‘𝑌)))) |
23 | 11, 22 | sylnbi 319 |
. . . . . 6
⊢ (¬
𝑌 ∈ 𝐴 → (𝑌 ∈ 𝑉 → ((𝑋 ∈ 𝑉 ∧ ((𝑉 VDeg 𝐸)‘𝑋) = 𝐾) → ((𝑉 VDeg 𝐸)‘𝑋) ≠ ((𝑉 VDeg 𝐸)‘𝑌)))) |
24 | 23 | impcom 445 |
. . . . 5
⊢ ((𝑌 ∈ 𝑉 ∧ ¬ 𝑌 ∈ 𝐴) → ((𝑋 ∈ 𝑉 ∧ ((𝑉 VDeg 𝐸)‘𝑋) = 𝐾) → ((𝑉 VDeg 𝐸)‘𝑋) ≠ ((𝑉 VDeg 𝐸)‘𝑌))) |
25 | 24 | com12 32 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ ((𝑉 VDeg 𝐸)‘𝑋) = 𝐾) → ((𝑌 ∈ 𝑉 ∧ ¬ 𝑌 ∈ 𝐴) → ((𝑉 VDeg 𝐸)‘𝑋) ≠ ((𝑉 VDeg 𝐸)‘𝑌))) |
26 | 8, 25 | syl5bi 231 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ((𝑉 VDeg 𝐸)‘𝑋) = 𝐾) → (𝑌 ∈ 𝐵 → ((𝑉 VDeg 𝐸)‘𝑋) ≠ ((𝑉 VDeg 𝐸)‘𝑌))) |
27 | 4, 26 | sylbi 206 |
. 2
⊢ (𝑋 ∈ 𝐴 → (𝑌 ∈ 𝐵 → ((𝑉 VDeg 𝐸)‘𝑋) ≠ ((𝑉 VDeg 𝐸)‘𝑌))) |
28 | 27 | imp 444 |
1
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → ((𝑉 VDeg 𝐸)‘𝑋) ≠ ((𝑉 VDeg 𝐸)‘𝑌)) |