Proof of Theorem pmtrcnelor
| Step | Hyp | Ref
| Expression |
| 1 | | pmtrcnel.s |
. . . . . . 7
⊢ 𝑆 = (SymGrp‘𝐷) |
| 2 | | pmtrcnel.t |
. . . . . . 7
⊢ 𝑇 = (pmTrsp‘𝐷) |
| 3 | | pmtrcnel.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑆) |
| 4 | | pmtrcnel.j |
. . . . . . 7
⊢ 𝐽 = (𝐹‘𝐼) |
| 5 | | pmtrcnel.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
| 6 | | pmtrcnel.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
| 7 | | pmtrcnel.i |
. . . . . . 7
⊢ (𝜑 → 𝐼 ∈ dom (𝐹 ∖ I )) |
| 8 | 1, 2, 3, 4, 5, 6, 7 | pmtrcnel 33109 |
. . . . . 6
⊢ (𝜑 → dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ) ⊆ (dom (𝐹 ∖ I ) ∖ {𝐼})) |
| 9 | | pmtrcnel.a |
. . . . . 6
⊢ 𝐴 = dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ) |
| 10 | | pmtrcnel.e |
. . . . . . 7
⊢ 𝐸 = dom (𝐹 ∖ I ) |
| 11 | 10 | difeq1i 4122 |
. . . . . 6
⊢ (𝐸 ∖ {𝐼}) = (dom (𝐹 ∖ I ) ∖ {𝐼}) |
| 12 | 8, 9, 11 | 3sstr4g 4037 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ (𝐸 ∖ {𝐼})) |
| 13 | 12 | ssdifd 4145 |
. . . 4
⊢ (𝜑 → (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) ⊆ ((𝐸 ∖ {𝐼}) ∖ (𝐸 ∖ {𝐼, 𝐽}))) |
| 14 | | difpr 4803 |
. . . . . 6
⊢ (𝐸 ∖ {𝐼, 𝐽}) = ((𝐸 ∖ {𝐼}) ∖ {𝐽}) |
| 15 | 14 | difeq2i 4123 |
. . . . 5
⊢ ((𝐸 ∖ {𝐼}) ∖ (𝐸 ∖ {𝐼, 𝐽})) = ((𝐸 ∖ {𝐼}) ∖ ((𝐸 ∖ {𝐼}) ∖ {𝐽})) |
| 16 | 1, 3 | symgbasf1o 19392 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐷–1-1-onto→𝐷) |
| 17 | 6, 16 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝐷–1-1-onto→𝐷) |
| 18 | | f1omvdmvd 19461 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐷–1-1-onto→𝐷 ∧ 𝐼 ∈ dom (𝐹 ∖ I )) → (𝐹‘𝐼) ∈ (dom (𝐹 ∖ I ) ∖ {𝐼})) |
| 19 | 17, 7, 18 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘𝐼) ∈ (dom (𝐹 ∖ I ) ∖ {𝐼})) |
| 20 | 4, 19 | eqeltrid 2845 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ (dom (𝐹 ∖ I ) ∖ {𝐼})) |
| 21 | 20 | eldifad 3963 |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ dom (𝐹 ∖ I )) |
| 22 | 21, 10 | eleqtrrdi 2852 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ 𝐸) |
| 23 | 4 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 = (𝐹‘𝐼)) |
| 24 | | f1of 6848 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐷–1-1-onto→𝐷 → 𝐹:𝐷⟶𝐷) |
| 25 | 17, 24 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐷⟶𝐷) |
| 26 | 25 | ffnd 6737 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 Fn 𝐷) |
| 27 | | difss 4136 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∖ I ) ⊆ 𝐹 |
| 28 | | dmss 5913 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∖ I ) ⊆ 𝐹 → dom (𝐹 ∖ I ) ⊆ dom 𝐹) |
| 29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ dom
(𝐹 ∖ I ) ⊆ dom
𝐹 |
| 30 | 29, 7 | sselid 3981 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ dom 𝐹) |
| 31 | 25 | fdmd 6746 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐹 = 𝐷) |
| 32 | 30, 31 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ 𝐷) |
| 33 | | fnelnfp 7197 |
. . . . . . . . . . 11
⊢ ((𝐹 Fn 𝐷 ∧ 𝐼 ∈ 𝐷) → (𝐼 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝐼) ≠ 𝐼)) |
| 34 | 33 | biimpa 476 |
. . . . . . . . . 10
⊢ (((𝐹 Fn 𝐷 ∧ 𝐼 ∈ 𝐷) ∧ 𝐼 ∈ dom (𝐹 ∖ I )) → (𝐹‘𝐼) ≠ 𝐼) |
| 35 | 26, 32, 7, 34 | syl21anc 838 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝐼) ≠ 𝐼) |
| 36 | 23, 35 | eqnetrd 3008 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ≠ 𝐼) |
| 37 | | eldifsn 4786 |
. . . . . . . 8
⊢ (𝐽 ∈ (𝐸 ∖ {𝐼}) ↔ (𝐽 ∈ 𝐸 ∧ 𝐽 ≠ 𝐼)) |
| 38 | 22, 36, 37 | sylanbrc 583 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ (𝐸 ∖ {𝐼})) |
| 39 | 38 | snssd 4809 |
. . . . . 6
⊢ (𝜑 → {𝐽} ⊆ (𝐸 ∖ {𝐼})) |
| 40 | | dfss4 4269 |
. . . . . 6
⊢ ({𝐽} ⊆ (𝐸 ∖ {𝐼}) ↔ ((𝐸 ∖ {𝐼}) ∖ ((𝐸 ∖ {𝐼}) ∖ {𝐽})) = {𝐽}) |
| 41 | 39, 40 | sylib 218 |
. . . . 5
⊢ (𝜑 → ((𝐸 ∖ {𝐼}) ∖ ((𝐸 ∖ {𝐼}) ∖ {𝐽})) = {𝐽}) |
| 42 | 15, 41 | eqtrid 2789 |
. . . 4
⊢ (𝜑 → ((𝐸 ∖ {𝐼}) ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) |
| 43 | 13, 42 | sseqtrd 4020 |
. . 3
⊢ (𝜑 → (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) ⊆ {𝐽}) |
| 44 | | sssn 4826 |
. . 3
⊢ ((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) ⊆ {𝐽} ↔ ((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅ ∨ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽})) |
| 45 | 43, 44 | sylib 218 |
. 2
⊢ (𝜑 → ((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅ ∨ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽})) |
| 46 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅) → (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅) |
| 47 | 1, 2, 3, 4, 5, 6, 7 | pmtrcnel2 33110 |
. . . . . . . 8
⊢ (𝜑 → (dom (𝐹 ∖ I ) ∖ {𝐼, 𝐽}) ⊆ dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I )) |
| 48 | 10 | difeq1i 4122 |
. . . . . . . 8
⊢ (𝐸 ∖ {𝐼, 𝐽}) = (dom (𝐹 ∖ I ) ∖ {𝐼, 𝐽}) |
| 49 | 47, 48, 9 | 3sstr4g 4037 |
. . . . . . 7
⊢ (𝜑 → (𝐸 ∖ {𝐼, 𝐽}) ⊆ 𝐴) |
| 50 | | ssdif0 4366 |
. . . . . . 7
⊢ ((𝐸 ∖ {𝐼, 𝐽}) ⊆ 𝐴 ↔ ((𝐸 ∖ {𝐼, 𝐽}) ∖ 𝐴) = ∅) |
| 51 | 49, 50 | sylib 218 |
. . . . . 6
⊢ (𝜑 → ((𝐸 ∖ {𝐼, 𝐽}) ∖ 𝐴) = ∅) |
| 52 | 51 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅) → ((𝐸 ∖ {𝐼, 𝐽}) ∖ 𝐴) = ∅) |
| 53 | | eqdif 32538 |
. . . . 5
⊢ (((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅ ∧ ((𝐸 ∖ {𝐼, 𝐽}) ∖ 𝐴) = ∅) → 𝐴 = (𝐸 ∖ {𝐼, 𝐽})) |
| 54 | 46, 52, 53 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅) → 𝐴 = (𝐸 ∖ {𝐼, 𝐽})) |
| 55 | 54 | ex 412 |
. . 3
⊢ (𝜑 → ((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅ → 𝐴 = (𝐸 ∖ {𝐼, 𝐽}))) |
| 56 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → 𝐴 ⊆ (𝐸 ∖ {𝐼})) |
| 57 | 14, 49 | eqsstrrid 4023 |
. . . . . . . 8
⊢ (𝜑 → ((𝐸 ∖ {𝐼}) ∖ {𝐽}) ⊆ 𝐴) |
| 58 | 57 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → ((𝐸 ∖ {𝐼}) ∖ {𝐽}) ⊆ 𝐴) |
| 59 | | ssundif 4488 |
. . . . . . 7
⊢ ((𝐸 ∖ {𝐼}) ⊆ ({𝐽} ∪ 𝐴) ↔ ((𝐸 ∖ {𝐼}) ∖ {𝐽}) ⊆ 𝐴) |
| 60 | 58, 59 | sylibr 234 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → (𝐸 ∖ {𝐼}) ⊆ ({𝐽} ∪ 𝐴)) |
| 61 | | ssidd 4007 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → {𝐽} ⊆ {𝐽}) |
| 62 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) |
| 63 | 61, 62 | sseqtrrd 4021 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → {𝐽} ⊆ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽}))) |
| 64 | 63 | difss2d 4139 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → {𝐽} ⊆ 𝐴) |
| 65 | | ssequn1 4186 |
. . . . . . 7
⊢ ({𝐽} ⊆ 𝐴 ↔ ({𝐽} ∪ 𝐴) = 𝐴) |
| 66 | 64, 65 | sylib 218 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → ({𝐽} ∪ 𝐴) = 𝐴) |
| 67 | 60, 66 | sseqtrd 4020 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → (𝐸 ∖ {𝐼}) ⊆ 𝐴) |
| 68 | 56, 67 | eqssd 4001 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → 𝐴 = (𝐸 ∖ {𝐼})) |
| 69 | 68 | ex 412 |
. . 3
⊢ (𝜑 → ((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽} → 𝐴 = (𝐸 ∖ {𝐼}))) |
| 70 | 55, 69 | orim12d 967 |
. 2
⊢ (𝜑 → (((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅ ∨ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → (𝐴 = (𝐸 ∖ {𝐼, 𝐽}) ∨ 𝐴 = (𝐸 ∖ {𝐼})))) |
| 71 | 45, 70 | mpd 15 |
1
⊢ (𝜑 → (𝐴 = (𝐸 ∖ {𝐼, 𝐽}) ∨ 𝐴 = (𝐸 ∖ {𝐼}))) |