Proof of Theorem pmtrcnel2
| Step | Hyp | Ref
| Expression |
| 1 | | mvdco 19463 |
. . . . 5
⊢ dom
((◡(𝑇‘{𝐼, 𝐽}) ∘ ((𝑇‘{𝐼, 𝐽}) ∘ 𝐹)) ∖ I ) ⊆ (dom (◡(𝑇‘{𝐼, 𝐽}) ∖ I ) ∪ dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I )) |
| 2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → dom ((◡(𝑇‘{𝐼, 𝐽}) ∘ ((𝑇‘{𝐼, 𝐽}) ∘ 𝐹)) ∖ I ) ⊆ (dom (◡(𝑇‘{𝐼, 𝐽}) ∖ I ) ∪ dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ))) |
| 3 | | coass 6285 |
. . . . . . . 8
⊢ ((◡(𝑇‘{𝐼, 𝐽}) ∘ (𝑇‘{𝐼, 𝐽})) ∘ 𝐹) = (◡(𝑇‘{𝐼, 𝐽}) ∘ ((𝑇‘{𝐼, 𝐽}) ∘ 𝐹)) |
| 4 | | pmtrcnel.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
| 5 | | difss 4136 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∖ I ) ⊆ 𝐹 |
| 6 | | dmss 5913 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∖ I ) ⊆ 𝐹 → dom (𝐹 ∖ I ) ⊆ dom 𝐹) |
| 7 | 5, 6 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ dom
(𝐹 ∖ I ) ⊆ dom
𝐹 |
| 8 | | pmtrcnel.i |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐼 ∈ dom (𝐹 ∖ I )) |
| 9 | 7, 8 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐼 ∈ dom 𝐹) |
| 10 | | pmtrcnel.f |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
| 11 | | pmtrcnel.s |
. . . . . . . . . . . . . . . 16
⊢ 𝑆 = (SymGrp‘𝐷) |
| 12 | | pmtrcnel.b |
. . . . . . . . . . . . . . . 16
⊢ 𝐵 = (Base‘𝑆) |
| 13 | 11, 12 | symgbasf1o 19392 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐷–1-1-onto→𝐷) |
| 14 | | f1of 6848 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:𝐷–1-1-onto→𝐷 → 𝐹:𝐷⟶𝐷) |
| 15 | 10, 13, 14 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:𝐷⟶𝐷) |
| 16 | 15 | fdmd 6746 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom 𝐹 = 𝐷) |
| 17 | 9, 16 | eleqtrd 2843 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ∈ 𝐷) |
| 18 | | pmtrcnel.j |
. . . . . . . . . . . . 13
⊢ 𝐽 = (𝐹‘𝐼) |
| 19 | 15, 17 | ffvelcdmd 7105 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘𝐼) ∈ 𝐷) |
| 20 | 18, 19 | eqeltrid 2845 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ 𝐷) |
| 21 | 17, 20 | prssd 4822 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝐼, 𝐽} ⊆ 𝐷) |
| 22 | 15 | ffnd 6737 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 Fn 𝐷) |
| 23 | | fnelnfp 7197 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 Fn 𝐷 ∧ 𝐼 ∈ 𝐷) → (𝐼 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝐼) ≠ 𝐼)) |
| 24 | 23 | biimpa 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 Fn 𝐷 ∧ 𝐼 ∈ 𝐷) ∧ 𝐼 ∈ dom (𝐹 ∖ I )) → (𝐹‘𝐼) ≠ 𝐼) |
| 25 | 22, 17, 8, 24 | syl21anc 838 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹‘𝐼) ≠ 𝐼) |
| 26 | 25 | necomd 2996 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐼 ≠ (𝐹‘𝐼)) |
| 27 | 18 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 = (𝐹‘𝐼)) |
| 28 | 26, 27 | neeqtrrd 3015 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ≠ 𝐽) |
| 29 | | enpr2 10042 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽) → {𝐼, 𝐽} ≈ 2o) |
| 30 | 17, 20, 28, 29 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝐼, 𝐽} ≈ 2o) |
| 31 | | pmtrcnel.t |
. . . . . . . . . . . 12
⊢ 𝑇 = (pmTrsp‘𝐷) |
| 32 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ ran 𝑇 = ran 𝑇 |
| 33 | 31, 32 | pmtrrn 19475 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ 𝑉 ∧ {𝐼, 𝐽} ⊆ 𝐷 ∧ {𝐼, 𝐽} ≈ 2o) → (𝑇‘{𝐼, 𝐽}) ∈ ran 𝑇) |
| 34 | 4, 21, 30, 33 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑇‘{𝐼, 𝐽}) ∈ ran 𝑇) |
| 35 | 31, 32 | pmtrff1o 19481 |
. . . . . . . . . 10
⊢ ((𝑇‘{𝐼, 𝐽}) ∈ ran 𝑇 → (𝑇‘{𝐼, 𝐽}):𝐷–1-1-onto→𝐷) |
| 36 | | f1ococnv1 6877 |
. . . . . . . . . 10
⊢ ((𝑇‘{𝐼, 𝐽}):𝐷–1-1-onto→𝐷 → (◡(𝑇‘{𝐼, 𝐽}) ∘ (𝑇‘{𝐼, 𝐽})) = ( I ↾ 𝐷)) |
| 37 | 34, 35, 36 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (◡(𝑇‘{𝐼, 𝐽}) ∘ (𝑇‘{𝐼, 𝐽})) = ( I ↾ 𝐷)) |
| 38 | 37 | coeq1d 5872 |
. . . . . . . 8
⊢ (𝜑 → ((◡(𝑇‘{𝐼, 𝐽}) ∘ (𝑇‘{𝐼, 𝐽})) ∘ 𝐹) = (( I ↾ 𝐷) ∘ 𝐹)) |
| 39 | 3, 38 | eqtr3id 2791 |
. . . . . . 7
⊢ (𝜑 → (◡(𝑇‘{𝐼, 𝐽}) ∘ ((𝑇‘{𝐼, 𝐽}) ∘ 𝐹)) = (( I ↾ 𝐷) ∘ 𝐹)) |
| 40 | | fcoi2 6783 |
. . . . . . . 8
⊢ (𝐹:𝐷⟶𝐷 → (( I ↾ 𝐷) ∘ 𝐹) = 𝐹) |
| 41 | 15, 40 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (( I ↾ 𝐷) ∘ 𝐹) = 𝐹) |
| 42 | 39, 41 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → (◡(𝑇‘{𝐼, 𝐽}) ∘ ((𝑇‘{𝐼, 𝐽}) ∘ 𝐹)) = 𝐹) |
| 43 | 42 | difeq1d 4125 |
. . . . 5
⊢ (𝜑 → ((◡(𝑇‘{𝐼, 𝐽}) ∘ ((𝑇‘{𝐼, 𝐽}) ∘ 𝐹)) ∖ I ) = (𝐹 ∖ I )) |
| 44 | 43 | dmeqd 5916 |
. . . 4
⊢ (𝜑 → dom ((◡(𝑇‘{𝐼, 𝐽}) ∘ ((𝑇‘{𝐼, 𝐽}) ∘ 𝐹)) ∖ I ) = dom (𝐹 ∖ I )) |
| 45 | 31, 32 | pmtrfcnv 19482 |
. . . . . . . . . 10
⊢ ((𝑇‘{𝐼, 𝐽}) ∈ ran 𝑇 → ◡(𝑇‘{𝐼, 𝐽}) = (𝑇‘{𝐼, 𝐽})) |
| 46 | 34, 45 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ◡(𝑇‘{𝐼, 𝐽}) = (𝑇‘{𝐼, 𝐽})) |
| 47 | 46 | difeq1d 4125 |
. . . . . . . 8
⊢ (𝜑 → (◡(𝑇‘{𝐼, 𝐽}) ∖ I ) = ((𝑇‘{𝐼, 𝐽}) ∖ I )) |
| 48 | 47 | dmeqd 5916 |
. . . . . . 7
⊢ (𝜑 → dom (◡(𝑇‘{𝐼, 𝐽}) ∖ I ) = dom ((𝑇‘{𝐼, 𝐽}) ∖ I )) |
| 49 | 31 | pmtrmvd 19474 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ {𝐼, 𝐽} ⊆ 𝐷 ∧ {𝐼, 𝐽} ≈ 2o) → dom ((𝑇‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽}) |
| 50 | 4, 21, 30, 49 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → dom ((𝑇‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽}) |
| 51 | 48, 50 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → dom (◡(𝑇‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽}) |
| 52 | 51 | uneq1d 4167 |
. . . . 5
⊢ (𝜑 → (dom (◡(𝑇‘{𝐼, 𝐽}) ∖ I ) ∪ dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I )) = ({𝐼, 𝐽} ∪ dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ))) |
| 53 | | uncom 4158 |
. . . . 5
⊢ ({𝐼, 𝐽} ∪ dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I )) = (dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ) ∪ {𝐼, 𝐽}) |
| 54 | 52, 53 | eqtrdi 2793 |
. . . 4
⊢ (𝜑 → (dom (◡(𝑇‘{𝐼, 𝐽}) ∖ I ) ∪ dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I )) = (dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ) ∪ {𝐼, 𝐽})) |
| 55 | 2, 44, 54 | 3sstr3d 4038 |
. . 3
⊢ (𝜑 → dom (𝐹 ∖ I ) ⊆ (dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ) ∪ {𝐼, 𝐽})) |
| 56 | 55 | ssdifd 4145 |
. 2
⊢ (𝜑 → (dom (𝐹 ∖ I ) ∖ {𝐼, 𝐽}) ⊆ ((dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ) ∪ {𝐼, 𝐽}) ∖ {𝐼, 𝐽})) |
| 57 | | difun2 4481 |
. . 3
⊢ ((dom
(((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ) ∪ {𝐼, 𝐽}) ∖ {𝐼, 𝐽}) = (dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ) ∖ {𝐼, 𝐽}) |
| 58 | | difss 4136 |
. . 3
⊢ (dom
(((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ) ∖ {𝐼, 𝐽}) ⊆ dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ) |
| 59 | 57, 58 | eqsstri 4030 |
. 2
⊢ ((dom
(((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ) ∪ {𝐼, 𝐽}) ∖ {𝐼, 𝐽}) ⊆ dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ) |
| 60 | 56, 59 | sstrdi 3996 |
1
⊢ (𝜑 → (dom (𝐹 ∖ I ) ∖ {𝐼, 𝐽}) ⊆ dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I )) |