Proof of Theorem frgrwopreglem3
Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝐷‘𝑥) = (𝐷‘𝑋)) |
2 | 1 | eqeq1d 2612 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝐷‘𝑥) = 𝐾 ↔ (𝐷‘𝑋) = 𝐾)) |
3 | | frgrwopreg.a |
. . . 4
⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} |
4 | 2, 3 | elrab2 3333 |
. . 3
⊢ (𝑋 ∈ 𝐴 ↔ (𝑋 ∈ 𝑉 ∧ (𝐷‘𝑋) = 𝐾)) |
5 | | frgrwopreg.b |
. . . . . 6
⊢ 𝐵 = (𝑉 ∖ 𝐴) |
6 | 5 | eleq2i 2680 |
. . . . 5
⊢ (𝑌 ∈ 𝐵 ↔ 𝑌 ∈ (𝑉 ∖ 𝐴)) |
7 | | eldif 3550 |
. . . . 5
⊢ (𝑌 ∈ (𝑉 ∖ 𝐴) ↔ (𝑌 ∈ 𝑉 ∧ ¬ 𝑌 ∈ 𝐴)) |
8 | 6, 7 | bitri 263 |
. . . 4
⊢ (𝑌 ∈ 𝐵 ↔ (𝑌 ∈ 𝑉 ∧ ¬ 𝑌 ∈ 𝐴)) |
9 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = 𝑌 → (𝐷‘𝑥) = (𝐷‘𝑌)) |
10 | 9 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑥 = 𝑌 → ((𝐷‘𝑥) = 𝐾 ↔ (𝐷‘𝑌) = 𝐾)) |
11 | 10, 3 | elrab2 3333 |
. . . . . . 7
⊢ (𝑌 ∈ 𝐴 ↔ (𝑌 ∈ 𝑉 ∧ (𝐷‘𝑌) = 𝐾)) |
12 | | ianor 508 |
. . . . . . . 8
⊢ (¬
(𝑌 ∈ 𝑉 ∧ (𝐷‘𝑌) = 𝐾) ↔ (¬ 𝑌 ∈ 𝑉 ∨ ¬ (𝐷‘𝑌) = 𝐾)) |
13 | | pm2.21 119 |
. . . . . . . . 9
⊢ (¬
𝑌 ∈ 𝑉 → (𝑌 ∈ 𝑉 → ((𝑋 ∈ 𝑉 ∧ (𝐷‘𝑋) = 𝐾) → (𝐷‘𝑋) ≠ (𝐷‘𝑌)))) |
14 | | neqne 2790 |
. . . . . . . . . . . . . 14
⊢ (¬
(𝐷‘𝑌) = 𝐾 → (𝐷‘𝑌) ≠ 𝐾) |
15 | 14 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((¬
(𝐷‘𝑌) = 𝐾 ∧ (𝑋 ∈ 𝑉 ∧ (𝐷‘𝑋) = 𝐾)) → (𝐷‘𝑌) ≠ 𝐾) |
16 | 15 | necomd 2837 |
. . . . . . . . . . . 12
⊢ ((¬
(𝐷‘𝑌) = 𝐾 ∧ (𝑋 ∈ 𝑉 ∧ (𝐷‘𝑋) = 𝐾)) → 𝐾 ≠ (𝐷‘𝑌)) |
17 | | neeq1 2844 |
. . . . . . . . . . . . 13
⊢ ((𝐷‘𝑋) = 𝐾 → ((𝐷‘𝑋) ≠ (𝐷‘𝑌) ↔ 𝐾 ≠ (𝐷‘𝑌))) |
18 | 17 | ad2antll 761 |
. . . . . . . . . . . 12
⊢ ((¬
(𝐷‘𝑌) = 𝐾 ∧ (𝑋 ∈ 𝑉 ∧ (𝐷‘𝑋) = 𝐾)) → ((𝐷‘𝑋) ≠ (𝐷‘𝑌) ↔ 𝐾 ≠ (𝐷‘𝑌))) |
19 | 16, 18 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((¬
(𝐷‘𝑌) = 𝐾 ∧ (𝑋 ∈ 𝑉 ∧ (𝐷‘𝑋) = 𝐾)) → (𝐷‘𝑋) ≠ (𝐷‘𝑌)) |
20 | 19 | ex 449 |
. . . . . . . . . 10
⊢ (¬
(𝐷‘𝑌) = 𝐾 → ((𝑋 ∈ 𝑉 ∧ (𝐷‘𝑋) = 𝐾) → (𝐷‘𝑋) ≠ (𝐷‘𝑌))) |
21 | 20 | a1d 25 |
. . . . . . . . 9
⊢ (¬
(𝐷‘𝑌) = 𝐾 → (𝑌 ∈ 𝑉 → ((𝑋 ∈ 𝑉 ∧ (𝐷‘𝑋) = 𝐾) → (𝐷‘𝑋) ≠ (𝐷‘𝑌)))) |
22 | 13, 21 | jaoi 393 |
. . . . . . . 8
⊢ ((¬
𝑌 ∈ 𝑉 ∨ ¬ (𝐷‘𝑌) = 𝐾) → (𝑌 ∈ 𝑉 → ((𝑋 ∈ 𝑉 ∧ (𝐷‘𝑋) = 𝐾) → (𝐷‘𝑋) ≠ (𝐷‘𝑌)))) |
23 | 12, 22 | sylbi 206 |
. . . . . . 7
⊢ (¬
(𝑌 ∈ 𝑉 ∧ (𝐷‘𝑌) = 𝐾) → (𝑌 ∈ 𝑉 → ((𝑋 ∈ 𝑉 ∧ (𝐷‘𝑋) = 𝐾) → (𝐷‘𝑋) ≠ (𝐷‘𝑌)))) |
24 | 11, 23 | sylnbi 319 |
. . . . . 6
⊢ (¬
𝑌 ∈ 𝐴 → (𝑌 ∈ 𝑉 → ((𝑋 ∈ 𝑉 ∧ (𝐷‘𝑋) = 𝐾) → (𝐷‘𝑋) ≠ (𝐷‘𝑌)))) |
25 | 24 | impcom 445 |
. . . . 5
⊢ ((𝑌 ∈ 𝑉 ∧ ¬ 𝑌 ∈ 𝐴) → ((𝑋 ∈ 𝑉 ∧ (𝐷‘𝑋) = 𝐾) → (𝐷‘𝑋) ≠ (𝐷‘𝑌))) |
26 | 25 | com12 32 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐷‘𝑋) = 𝐾) → ((𝑌 ∈ 𝑉 ∧ ¬ 𝑌 ∈ 𝐴) → (𝐷‘𝑋) ≠ (𝐷‘𝑌))) |
27 | 8, 26 | syl5bi 231 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐷‘𝑋) = 𝐾) → (𝑌 ∈ 𝐵 → (𝐷‘𝑋) ≠ (𝐷‘𝑌))) |
28 | 4, 27 | sylbi 206 |
. 2
⊢ (𝑋 ∈ 𝐴 → (𝑌 ∈ 𝐵 → (𝐷‘𝑋) ≠ (𝐷‘𝑌))) |
29 | 28 | imp 444 |
1
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝐷‘𝑋) ≠ (𝐷‘𝑌)) |