Step | Hyp | Ref
| Expression |
1 | | eldif 3802 |
. . 3
⊢ (𝑄 ∈ (𝑃 ∖ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿}) ↔ (𝑄 ∈ 𝑃 ∧ ¬ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿})) |
2 | | ianor 967 |
. . . . 5
⊢ (¬
(𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ↔ (¬ 𝑄 ∈ 𝑃 ∨ ¬ (𝑄‘𝐾) = 𝐿)) |
3 | | fveq1 6447 |
. . . . . . 7
⊢ (𝑞 = 𝑄 → (𝑞‘𝐾) = (𝑄‘𝐾)) |
4 | 3 | eqeq1d 2780 |
. . . . . 6
⊢ (𝑞 = 𝑄 → ((𝑞‘𝐾) = 𝐿 ↔ (𝑄‘𝐾) = 𝐿)) |
5 | 4 | elrab 3572 |
. . . . 5
⊢ (𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿} ↔ (𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿)) |
6 | 2, 5 | xchnxbir 325 |
. . . 4
⊢ (¬
𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿} ↔ (¬ 𝑄 ∈ 𝑃 ∨ ¬ (𝑄‘𝐾) = 𝐿)) |
7 | 6 | anbi2i 616 |
. . 3
⊢ ((𝑄 ∈ 𝑃 ∧ ¬ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿}) ↔ (𝑄 ∈ 𝑃 ∧ (¬ 𝑄 ∈ 𝑃 ∨ ¬ (𝑄‘𝐾) = 𝐿))) |
8 | 1, 7 | bitri 267 |
. 2
⊢ (𝑄 ∈ (𝑃 ∖ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿}) ↔ (𝑄 ∈ 𝑃 ∧ (¬ 𝑄 ∈ 𝑃 ∨ ¬ (𝑄‘𝐾) = 𝐿))) |
9 | | pm2.21 121 |
. . . . 5
⊢ (¬
𝑄 ∈ 𝑃 → (𝑄 ∈ 𝑃 → (𝐿 ∈ 𝑁 → ∃𝑘 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿))) |
10 | | symgfix2.p |
. . . . . . 7
⊢ 𝑃 =
(Base‘(SymGrp‘𝑁)) |
11 | 10 | symgmov2 18207 |
. . . . . 6
⊢ (𝑄 ∈ 𝑃 → ∀𝑙 ∈ 𝑁 ∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝑙) |
12 | | eqeq2 2789 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝐿 → ((𝑄‘𝑘) = 𝑙 ↔ (𝑄‘𝑘) = 𝐿)) |
13 | 12 | rexbidv 3237 |
. . . . . . . . . 10
⊢ (𝑙 = 𝐿 → (∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝑙 ↔ ∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝐿)) |
14 | 13 | rspcva 3509 |
. . . . . . . . 9
⊢ ((𝐿 ∈ 𝑁 ∧ ∀𝑙 ∈ 𝑁 ∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝑙) → ∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝐿) |
15 | | eqeq2 2789 |
. . . . . . . . . . . . . . . 16
⊢ (𝐿 = (𝑄‘𝑘) → ((𝑄‘𝐾) = 𝐿 ↔ (𝑄‘𝐾) = (𝑄‘𝑘))) |
16 | 15 | eqcoms 2786 |
. . . . . . . . . . . . . . 15
⊢ ((𝑄‘𝑘) = 𝐿 → ((𝑄‘𝐾) = 𝐿 ↔ (𝑄‘𝐾) = (𝑄‘𝑘))) |
17 | 16 | notbid 310 |
. . . . . . . . . . . . . 14
⊢ ((𝑄‘𝑘) = 𝐿 → (¬ (𝑄‘𝐾) = 𝐿 ↔ ¬ (𝑄‘𝐾) = (𝑄‘𝑘))) |
18 | | fveq2 6448 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 = 𝑘 → (𝑄‘𝐾) = (𝑄‘𝑘)) |
19 | 18 | eqcoms 2786 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝐾 → (𝑄‘𝐾) = (𝑄‘𝑘)) |
20 | 19 | necon3bi 2995 |
. . . . . . . . . . . . . 14
⊢ (¬
(𝑄‘𝐾) = (𝑄‘𝑘) → 𝑘 ≠ 𝐾) |
21 | 17, 20 | syl6bi 245 |
. . . . . . . . . . . . 13
⊢ ((𝑄‘𝑘) = 𝐿 → (¬ (𝑄‘𝐾) = 𝐿 → 𝑘 ≠ 𝐾)) |
22 | 21 | com12 32 |
. . . . . . . . . . . 12
⊢ (¬
(𝑄‘𝐾) = 𝐿 → ((𝑄‘𝑘) = 𝐿 → 𝑘 ≠ 𝐾)) |
23 | 22 | pm4.71rd 558 |
. . . . . . . . . . 11
⊢ (¬
(𝑄‘𝐾) = 𝐿 → ((𝑄‘𝑘) = 𝐿 ↔ (𝑘 ≠ 𝐾 ∧ (𝑄‘𝑘) = 𝐿))) |
24 | 23 | rexbidv 3237 |
. . . . . . . . . 10
⊢ (¬
(𝑄‘𝐾) = 𝐿 → (∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝐿 ↔ ∃𝑘 ∈ 𝑁 (𝑘 ≠ 𝐾 ∧ (𝑄‘𝑘) = 𝐿))) |
25 | | rexdifsn 4558 |
. . . . . . . . . 10
⊢
(∃𝑘 ∈
(𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿 ↔ ∃𝑘 ∈ 𝑁 (𝑘 ≠ 𝐾 ∧ (𝑄‘𝑘) = 𝐿)) |
26 | 24, 25 | syl6bbr 281 |
. . . . . . . . 9
⊢ (¬
(𝑄‘𝐾) = 𝐿 → (∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝐿 ↔ ∃𝑘 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿)) |
27 | 14, 26 | syl5ibcom 237 |
. . . . . . . 8
⊢ ((𝐿 ∈ 𝑁 ∧ ∀𝑙 ∈ 𝑁 ∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝑙) → (¬ (𝑄‘𝐾) = 𝐿 → ∃𝑘 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿)) |
28 | 27 | ex 403 |
. . . . . . 7
⊢ (𝐿 ∈ 𝑁 → (∀𝑙 ∈ 𝑁 ∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝑙 → (¬ (𝑄‘𝐾) = 𝐿 → ∃𝑘 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿))) |
29 | 28 | com13 88 |
. . . . . 6
⊢ (¬
(𝑄‘𝐾) = 𝐿 → (∀𝑙 ∈ 𝑁 ∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝑙 → (𝐿 ∈ 𝑁 → ∃𝑘 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿))) |
30 | 11, 29 | syl5 34 |
. . . . 5
⊢ (¬
(𝑄‘𝐾) = 𝐿 → (𝑄 ∈ 𝑃 → (𝐿 ∈ 𝑁 → ∃𝑘 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿))) |
31 | 9, 30 | jaoi 846 |
. . . 4
⊢ ((¬
𝑄 ∈ 𝑃 ∨ ¬ (𝑄‘𝐾) = 𝐿) → (𝑄 ∈ 𝑃 → (𝐿 ∈ 𝑁 → ∃𝑘 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿))) |
32 | 31 | com13 88 |
. . 3
⊢ (𝐿 ∈ 𝑁 → (𝑄 ∈ 𝑃 → ((¬ 𝑄 ∈ 𝑃 ∨ ¬ (𝑄‘𝐾) = 𝐿) → ∃𝑘 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿))) |
33 | 32 | impd 400 |
. 2
⊢ (𝐿 ∈ 𝑁 → ((𝑄 ∈ 𝑃 ∧ (¬ 𝑄 ∈ 𝑃 ∨ ¬ (𝑄‘𝐾) = 𝐿)) → ∃𝑘 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿)) |
34 | 8, 33 | syl5bi 234 |
1
⊢ (𝐿 ∈ 𝑁 → (𝑄 ∈ (𝑃 ∖ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿}) → ∃𝑘 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿)) |