| Step | Hyp | Ref
| Expression |
| 1 | | eldif 3961 |
. . 3
⊢ (𝑄 ∈ (𝑃 ∖ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿}) ↔ (𝑄 ∈ 𝑃 ∧ ¬ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿})) |
| 2 | | ianor 984 |
. . . . 5
⊢ (¬
(𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ↔ (¬ 𝑄 ∈ 𝑃 ∨ ¬ (𝑄‘𝐾) = 𝐿)) |
| 3 | | fveq1 6905 |
. . . . . . 7
⊢ (𝑞 = 𝑄 → (𝑞‘𝐾) = (𝑄‘𝐾)) |
| 4 | 3 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑞 = 𝑄 → ((𝑞‘𝐾) = 𝐿 ↔ (𝑄‘𝐾) = 𝐿)) |
| 5 | 4 | elrab 3692 |
. . . . 5
⊢ (𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿} ↔ (𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿)) |
| 6 | 2, 5 | xchnxbir 333 |
. . . 4
⊢ (¬
𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿} ↔ (¬ 𝑄 ∈ 𝑃 ∨ ¬ (𝑄‘𝐾) = 𝐿)) |
| 7 | 6 | anbi2i 623 |
. . 3
⊢ ((𝑄 ∈ 𝑃 ∧ ¬ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿}) ↔ (𝑄 ∈ 𝑃 ∧ (¬ 𝑄 ∈ 𝑃 ∨ ¬ (𝑄‘𝐾) = 𝐿))) |
| 8 | 1, 7 | bitri 275 |
. 2
⊢ (𝑄 ∈ (𝑃 ∖ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿}) ↔ (𝑄 ∈ 𝑃 ∧ (¬ 𝑄 ∈ 𝑃 ∨ ¬ (𝑄‘𝐾) = 𝐿))) |
| 9 | | pm2.21 123 |
. . . . 5
⊢ (¬
𝑄 ∈ 𝑃 → (𝑄 ∈ 𝑃 → (𝐿 ∈ 𝑁 → ∃𝑘 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿))) |
| 10 | | symgfix2.p |
. . . . . . 7
⊢ 𝑃 =
(Base‘(SymGrp‘𝑁)) |
| 11 | 10 | symgmov2 19405 |
. . . . . 6
⊢ (𝑄 ∈ 𝑃 → ∀𝑙 ∈ 𝑁 ∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝑙) |
| 12 | | eqeq2 2749 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝐿 → ((𝑄‘𝑘) = 𝑙 ↔ (𝑄‘𝑘) = 𝐿)) |
| 13 | 12 | rexbidv 3179 |
. . . . . . . . . 10
⊢ (𝑙 = 𝐿 → (∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝑙 ↔ ∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝐿)) |
| 14 | 13 | rspcva 3620 |
. . . . . . . . 9
⊢ ((𝐿 ∈ 𝑁 ∧ ∀𝑙 ∈ 𝑁 ∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝑙) → ∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝐿) |
| 15 | | eqeq2 2749 |
. . . . . . . . . . . . . . . 16
⊢ (𝐿 = (𝑄‘𝑘) → ((𝑄‘𝐾) = 𝐿 ↔ (𝑄‘𝐾) = (𝑄‘𝑘))) |
| 16 | 15 | eqcoms 2745 |
. . . . . . . . . . . . . . 15
⊢ ((𝑄‘𝑘) = 𝐿 → ((𝑄‘𝐾) = 𝐿 ↔ (𝑄‘𝐾) = (𝑄‘𝑘))) |
| 17 | 16 | notbid 318 |
. . . . . . . . . . . . . 14
⊢ ((𝑄‘𝑘) = 𝐿 → (¬ (𝑄‘𝐾) = 𝐿 ↔ ¬ (𝑄‘𝐾) = (𝑄‘𝑘))) |
| 18 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 = 𝑘 → (𝑄‘𝐾) = (𝑄‘𝑘)) |
| 19 | 18 | eqcoms 2745 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝐾 → (𝑄‘𝐾) = (𝑄‘𝑘)) |
| 20 | 19 | necon3bi 2967 |
. . . . . . . . . . . . . 14
⊢ (¬
(𝑄‘𝐾) = (𝑄‘𝑘) → 𝑘 ≠ 𝐾) |
| 21 | 17, 20 | biimtrdi 253 |
. . . . . . . . . . . . 13
⊢ ((𝑄‘𝑘) = 𝐿 → (¬ (𝑄‘𝐾) = 𝐿 → 𝑘 ≠ 𝐾)) |
| 22 | 21 | com12 32 |
. . . . . . . . . . . 12
⊢ (¬
(𝑄‘𝐾) = 𝐿 → ((𝑄‘𝑘) = 𝐿 → 𝑘 ≠ 𝐾)) |
| 23 | 22 | pm4.71rd 562 |
. . . . . . . . . . 11
⊢ (¬
(𝑄‘𝐾) = 𝐿 → ((𝑄‘𝑘) = 𝐿 ↔ (𝑘 ≠ 𝐾 ∧ (𝑄‘𝑘) = 𝐿))) |
| 24 | 23 | rexbidv 3179 |
. . . . . . . . . 10
⊢ (¬
(𝑄‘𝐾) = 𝐿 → (∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝐿 ↔ ∃𝑘 ∈ 𝑁 (𝑘 ≠ 𝐾 ∧ (𝑄‘𝑘) = 𝐿))) |
| 25 | | rexdifsn 4794 |
. . . . . . . . . 10
⊢
(∃𝑘 ∈
(𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿 ↔ ∃𝑘 ∈ 𝑁 (𝑘 ≠ 𝐾 ∧ (𝑄‘𝑘) = 𝐿)) |
| 26 | 24, 25 | bitr4di 289 |
. . . . . . . . 9
⊢ (¬
(𝑄‘𝐾) = 𝐿 → (∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝐿 ↔ ∃𝑘 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿)) |
| 27 | 14, 26 | syl5ibcom 245 |
. . . . . . . 8
⊢ ((𝐿 ∈ 𝑁 ∧ ∀𝑙 ∈ 𝑁 ∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝑙) → (¬ (𝑄‘𝐾) = 𝐿 → ∃𝑘 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿)) |
| 28 | 27 | ex 412 |
. . . . . . 7
⊢ (𝐿 ∈ 𝑁 → (∀𝑙 ∈ 𝑁 ∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝑙 → (¬ (𝑄‘𝐾) = 𝐿 → ∃𝑘 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿))) |
| 29 | 28 | com13 88 |
. . . . . 6
⊢ (¬
(𝑄‘𝐾) = 𝐿 → (∀𝑙 ∈ 𝑁 ∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝑙 → (𝐿 ∈ 𝑁 → ∃𝑘 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿))) |
| 30 | 11, 29 | syl5 34 |
. . . . 5
⊢ (¬
(𝑄‘𝐾) = 𝐿 → (𝑄 ∈ 𝑃 → (𝐿 ∈ 𝑁 → ∃𝑘 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿))) |
| 31 | 9, 30 | jaoi 858 |
. . . 4
⊢ ((¬
𝑄 ∈ 𝑃 ∨ ¬ (𝑄‘𝐾) = 𝐿) → (𝑄 ∈ 𝑃 → (𝐿 ∈ 𝑁 → ∃𝑘 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿))) |
| 32 | 31 | com13 88 |
. . 3
⊢ (𝐿 ∈ 𝑁 → (𝑄 ∈ 𝑃 → ((¬ 𝑄 ∈ 𝑃 ∨ ¬ (𝑄‘𝐾) = 𝐿) → ∃𝑘 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿))) |
| 33 | 32 | impd 410 |
. 2
⊢ (𝐿 ∈ 𝑁 → ((𝑄 ∈ 𝑃 ∧ (¬ 𝑄 ∈ 𝑃 ∨ ¬ (𝑄‘𝐾) = 𝐿)) → ∃𝑘 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿)) |
| 34 | 8, 33 | biimtrid 242 |
1
⊢ (𝐿 ∈ 𝑁 → (𝑄 ∈ (𝑃 ∖ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿}) → ∃𝑘 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑘) = 𝐿)) |