| Step | Hyp | Ref
| Expression |
| 1 | | pmtrdifel.t |
. . . 4
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) |
| 2 | | pmtrdifel.r |
. . . 4
⊢ 𝑅 = ran (pmTrsp‘𝑁) |
| 3 | | pmtrdifel.0 |
. . . 4
⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I )) |
| 4 | 1, 2, 3 | pmtrdifellem1 19494 |
. . 3
⊢ (𝑄 ∈ 𝑇 → 𝑆 ∈ 𝑅) |
| 5 | | eqid 2737 |
. . . 4
⊢
(pmTrsp‘𝑁) =
(pmTrsp‘𝑁) |
| 6 | | eqid 2737 |
. . . 4
⊢ dom
(𝑆 ∖ I ) = dom (𝑆 ∖ I ) |
| 7 | 5, 2, 6 | pmtrffv 19477 |
. . 3
⊢ ((𝑆 ∈ 𝑅 ∧ 𝐾 ∈ 𝑁) → (𝑆‘𝐾) = if(𝐾 ∈ dom (𝑆 ∖ I ), ∪
(dom (𝑆 ∖ I ) ∖
{𝐾}), 𝐾)) |
| 8 | 4, 7 | sylan 580 |
. 2
⊢ ((𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁) → (𝑆‘𝐾) = if(𝐾 ∈ dom (𝑆 ∖ I ), ∪
(dom (𝑆 ∖ I ) ∖
{𝐾}), 𝐾)) |
| 9 | | eqid 2737 |
. . . . . . . 8
⊢
(SymGrp‘(𝑁
∖ {𝐾})) =
(SymGrp‘(𝑁 ∖
{𝐾})) |
| 10 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) |
| 11 | 1, 9, 10 | symgtrf 19487 |
. . . . . . 7
⊢ 𝑇 ⊆
(Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) |
| 12 | 11 | sseli 3979 |
. . . . . 6
⊢ (𝑄 ∈ 𝑇 → 𝑄 ∈ (Base‘(SymGrp‘(𝑁 ∖ {𝐾})))) |
| 13 | 9, 10 | symgbasf 19393 |
. . . . . 6
⊢ (𝑄 ∈
(Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) → 𝑄:(𝑁 ∖ {𝐾})⟶(𝑁 ∖ {𝐾})) |
| 14 | | ffn 6736 |
. . . . . . 7
⊢ (𝑄:(𝑁 ∖ {𝐾})⟶(𝑁 ∖ {𝐾}) → 𝑄 Fn (𝑁 ∖ {𝐾})) |
| 15 | | fndifnfp 7196 |
. . . . . . 7
⊢ (𝑄 Fn (𝑁 ∖ {𝐾}) → dom (𝑄 ∖ I ) = {𝑥 ∈ (𝑁 ∖ {𝐾}) ∣ (𝑄‘𝑥) ≠ 𝑥}) |
| 16 | | ssrab2 4080 |
. . . . . . . . . 10
⊢ {𝑥 ∈ (𝑁 ∖ {𝐾}) ∣ (𝑄‘𝑥) ≠ 𝑥} ⊆ (𝑁 ∖ {𝐾}) |
| 17 | | ssel2 3978 |
. . . . . . . . . . 11
⊢ (({𝑥 ∈ (𝑁 ∖ {𝐾}) ∣ (𝑄‘𝑥) ≠ 𝑥} ⊆ (𝑁 ∖ {𝐾}) ∧ 𝐾 ∈ {𝑥 ∈ (𝑁 ∖ {𝐾}) ∣ (𝑄‘𝑥) ≠ 𝑥}) → 𝐾 ∈ (𝑁 ∖ {𝐾})) |
| 18 | | eldif 3961 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ (𝑁 ∖ {𝐾}) ↔ (𝐾 ∈ 𝑁 ∧ ¬ 𝐾 ∈ {𝐾})) |
| 19 | | elsng 4640 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ 𝑁 → (𝐾 ∈ {𝐾} ↔ 𝐾 = 𝐾)) |
| 20 | 19 | notbid 318 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ 𝑁 → (¬ 𝐾 ∈ {𝐾} ↔ ¬ 𝐾 = 𝐾)) |
| 21 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ 𝐾 = 𝐾 |
| 22 | 21 | pm2.24i 150 |
. . . . . . . . . . . . . 14
⊢ (¬
𝐾 = 𝐾 → ¬ 𝐾 ∈ 𝑁) |
| 23 | 20, 22 | biimtrdi 253 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ 𝑁 → (¬ 𝐾 ∈ {𝐾} → ¬ 𝐾 ∈ 𝑁)) |
| 24 | 23 | imp 406 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ 𝑁 ∧ ¬ 𝐾 ∈ {𝐾}) → ¬ 𝐾 ∈ 𝑁) |
| 25 | 18, 24 | sylbi 217 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ (𝑁 ∖ {𝐾}) → ¬ 𝐾 ∈ 𝑁) |
| 26 | 17, 25 | syl 17 |
. . . . . . . . . 10
⊢ (({𝑥 ∈ (𝑁 ∖ {𝐾}) ∣ (𝑄‘𝑥) ≠ 𝑥} ⊆ (𝑁 ∖ {𝐾}) ∧ 𝐾 ∈ {𝑥 ∈ (𝑁 ∖ {𝐾}) ∣ (𝑄‘𝑥) ≠ 𝑥}) → ¬ 𝐾 ∈ 𝑁) |
| 27 | 16, 26 | mpan 690 |
. . . . . . . . 9
⊢ (𝐾 ∈ {𝑥 ∈ (𝑁 ∖ {𝐾}) ∣ (𝑄‘𝑥) ≠ 𝑥} → ¬ 𝐾 ∈ 𝑁) |
| 28 | 27 | con2i 139 |
. . . . . . . 8
⊢ (𝐾 ∈ 𝑁 → ¬ 𝐾 ∈ {𝑥 ∈ (𝑁 ∖ {𝐾}) ∣ (𝑄‘𝑥) ≠ 𝑥}) |
| 29 | | eleq2 2830 |
. . . . . . . . 9
⊢ (dom
(𝑄 ∖ I ) = {𝑥 ∈ (𝑁 ∖ {𝐾}) ∣ (𝑄‘𝑥) ≠ 𝑥} → (𝐾 ∈ dom (𝑄 ∖ I ) ↔ 𝐾 ∈ {𝑥 ∈ (𝑁 ∖ {𝐾}) ∣ (𝑄‘𝑥) ≠ 𝑥})) |
| 30 | 29 | notbid 318 |
. . . . . . . 8
⊢ (dom
(𝑄 ∖ I ) = {𝑥 ∈ (𝑁 ∖ {𝐾}) ∣ (𝑄‘𝑥) ≠ 𝑥} → (¬ 𝐾 ∈ dom (𝑄 ∖ I ) ↔ ¬ 𝐾 ∈ {𝑥 ∈ (𝑁 ∖ {𝐾}) ∣ (𝑄‘𝑥) ≠ 𝑥})) |
| 31 | 28, 30 | imbitrrid 246 |
. . . . . . 7
⊢ (dom
(𝑄 ∖ I ) = {𝑥 ∈ (𝑁 ∖ {𝐾}) ∣ (𝑄‘𝑥) ≠ 𝑥} → (𝐾 ∈ 𝑁 → ¬ 𝐾 ∈ dom (𝑄 ∖ I ))) |
| 32 | 14, 15, 31 | 3syl 18 |
. . . . . 6
⊢ (𝑄:(𝑁 ∖ {𝐾})⟶(𝑁 ∖ {𝐾}) → (𝐾 ∈ 𝑁 → ¬ 𝐾 ∈ dom (𝑄 ∖ I ))) |
| 33 | 12, 13, 32 | 3syl 18 |
. . . . 5
⊢ (𝑄 ∈ 𝑇 → (𝐾 ∈ 𝑁 → ¬ 𝐾 ∈ dom (𝑄 ∖ I ))) |
| 34 | 33 | imp 406 |
. . . 4
⊢ ((𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁) → ¬ 𝐾 ∈ dom (𝑄 ∖ I )) |
| 35 | 1, 2, 3 | pmtrdifellem2 19495 |
. . . . . 6
⊢ (𝑄 ∈ 𝑇 → dom (𝑆 ∖ I ) = dom (𝑄 ∖ I )) |
| 36 | 35 | eleq2d 2827 |
. . . . 5
⊢ (𝑄 ∈ 𝑇 → (𝐾 ∈ dom (𝑆 ∖ I ) ↔ 𝐾 ∈ dom (𝑄 ∖ I ))) |
| 37 | 36 | adantr 480 |
. . . 4
⊢ ((𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁) → (𝐾 ∈ dom (𝑆 ∖ I ) ↔ 𝐾 ∈ dom (𝑄 ∖ I ))) |
| 38 | 34, 37 | mtbird 325 |
. . 3
⊢ ((𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁) → ¬ 𝐾 ∈ dom (𝑆 ∖ I )) |
| 39 | 38 | iffalsed 4536 |
. 2
⊢ ((𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁) → if(𝐾 ∈ dom (𝑆 ∖ I ), ∪
(dom (𝑆 ∖ I ) ∖
{𝐾}), 𝐾) = 𝐾) |
| 40 | 8, 39 | eqtrd 2777 |
1
⊢ ((𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁) → (𝑆‘𝐾) = 𝐾) |