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 31077 |
. . . . . 6
⊢ (𝜑 → dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ) ⊆ (dom (𝐹 ∖ I ) ∖ {𝐼})) |
9 | | pmtrcnel.a |
. . . . . 6
⊢ 𝐴 = dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ) |
10 | | pmtrcnel.e |
. . . . . . 7
⊢ 𝐸 = dom (𝐹 ∖ I ) |
11 | 10 | difeq1i 4033 |
. . . . . 6
⊢ (𝐸 ∖ {𝐼}) = (dom (𝐹 ∖ I ) ∖ {𝐼}) |
12 | 8, 9, 11 | 3sstr4g 3946 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ (𝐸 ∖ {𝐼})) |
13 | 12 | ssdifd 4055 |
. . . 4
⊢ (𝜑 → (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) ⊆ ((𝐸 ∖ {𝐼}) ∖ (𝐸 ∖ {𝐼, 𝐽}))) |
14 | | difpr 4716 |
. . . . . 6
⊢ (𝐸 ∖ {𝐼, 𝐽}) = ((𝐸 ∖ {𝐼}) ∖ {𝐽}) |
15 | 14 | difeq2i 4034 |
. . . . 5
⊢ ((𝐸 ∖ {𝐼}) ∖ (𝐸 ∖ {𝐼, 𝐽})) = ((𝐸 ∖ {𝐼}) ∖ ((𝐸 ∖ {𝐼}) ∖ {𝐽})) |
16 | 1, 3 | symgbasf1o 18767 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐷–1-1-onto→𝐷) |
17 | 6, 16 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝐷–1-1-onto→𝐷) |
18 | | f1omvdmvd 18835 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐷–1-1-onto→𝐷 ∧ 𝐼 ∈ dom (𝐹 ∖ I )) → (𝐹‘𝐼) ∈ (dom (𝐹 ∖ I ) ∖ {𝐼})) |
19 | 17, 7, 18 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘𝐼) ∈ (dom (𝐹 ∖ I ) ∖ {𝐼})) |
20 | 4, 19 | eqeltrid 2842 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ (dom (𝐹 ∖ I ) ∖ {𝐼})) |
21 | 20 | eldifad 3878 |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ dom (𝐹 ∖ I )) |
22 | 21, 10 | eleqtrrdi 2849 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ 𝐸) |
23 | 4 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 = (𝐹‘𝐼)) |
24 | | f1of 6661 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐷–1-1-onto→𝐷 → 𝐹:𝐷⟶𝐷) |
25 | 17, 24 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐷⟶𝐷) |
26 | 25 | ffnd 6546 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 Fn 𝐷) |
27 | | difss 4046 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∖ I ) ⊆ 𝐹 |
28 | | dmss 5771 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∖ I ) ⊆ 𝐹 → dom (𝐹 ∖ I ) ⊆ dom 𝐹) |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ dom
(𝐹 ∖ I ) ⊆ dom
𝐹 |
30 | 29, 7 | sseldi 3899 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ dom 𝐹) |
31 | 25 | fdmd 6556 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐹 = 𝐷) |
32 | 30, 31 | eleqtrd 2840 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ 𝐷) |
33 | | fnelnfp 6992 |
. . . . . . . . . . 11
⊢ ((𝐹 Fn 𝐷 ∧ 𝐼 ∈ 𝐷) → (𝐼 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝐼) ≠ 𝐼)) |
34 | 33 | biimpa 480 |
. . . . . . . . . 10
⊢ (((𝐹 Fn 𝐷 ∧ 𝐼 ∈ 𝐷) ∧ 𝐼 ∈ dom (𝐹 ∖ I )) → (𝐹‘𝐼) ≠ 𝐼) |
35 | 26, 32, 7, 34 | syl21anc 838 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝐼) ≠ 𝐼) |
36 | 23, 35 | eqnetrd 3008 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ≠ 𝐼) |
37 | | eldifsn 4700 |
. . . . . . . 8
⊢ (𝐽 ∈ (𝐸 ∖ {𝐼}) ↔ (𝐽 ∈ 𝐸 ∧ 𝐽 ≠ 𝐼)) |
38 | 22, 36, 37 | sylanbrc 586 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ (𝐸 ∖ {𝐼})) |
39 | 38 | snssd 4722 |
. . . . . 6
⊢ (𝜑 → {𝐽} ⊆ (𝐸 ∖ {𝐼})) |
40 | | dfss4 4173 |
. . . . . 6
⊢ ({𝐽} ⊆ (𝐸 ∖ {𝐼}) ↔ ((𝐸 ∖ {𝐼}) ∖ ((𝐸 ∖ {𝐼}) ∖ {𝐽})) = {𝐽}) |
41 | 39, 40 | sylib 221 |
. . . . 5
⊢ (𝜑 → ((𝐸 ∖ {𝐼}) ∖ ((𝐸 ∖ {𝐼}) ∖ {𝐽})) = {𝐽}) |
42 | 15, 41 | syl5eq 2790 |
. . . 4
⊢ (𝜑 → ((𝐸 ∖ {𝐼}) ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) |
43 | 13, 42 | sseqtrd 3941 |
. . 3
⊢ (𝜑 → (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) ⊆ {𝐽}) |
44 | | sssn 4739 |
. . 3
⊢ ((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) ⊆ {𝐽} ↔ ((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅ ∨ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽})) |
45 | 43, 44 | sylib 221 |
. 2
⊢ (𝜑 → ((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅ ∨ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽})) |
46 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅) → (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅) |
47 | 1, 2, 3, 4, 5, 6, 7 | pmtrcnel2 31078 |
. . . . . . . 8
⊢ (𝜑 → (dom (𝐹 ∖ I ) ∖ {𝐼, 𝐽}) ⊆ dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I )) |
48 | 10 | difeq1i 4033 |
. . . . . . . 8
⊢ (𝐸 ∖ {𝐼, 𝐽}) = (dom (𝐹 ∖ I ) ∖ {𝐼, 𝐽}) |
49 | 47, 48, 9 | 3sstr4g 3946 |
. . . . . . 7
⊢ (𝜑 → (𝐸 ∖ {𝐼, 𝐽}) ⊆ 𝐴) |
50 | | ssdif0 4278 |
. . . . . . 7
⊢ ((𝐸 ∖ {𝐼, 𝐽}) ⊆ 𝐴 ↔ ((𝐸 ∖ {𝐼, 𝐽}) ∖ 𝐴) = ∅) |
51 | 49, 50 | sylib 221 |
. . . . . 6
⊢ (𝜑 → ((𝐸 ∖ {𝐼, 𝐽}) ∖ 𝐴) = ∅) |
52 | 51 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅) → ((𝐸 ∖ {𝐼, 𝐽}) ∖ 𝐴) = ∅) |
53 | | eqdif 30585 |
. . . . 5
⊢ (((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅ ∧ ((𝐸 ∖ {𝐼, 𝐽}) ∖ 𝐴) = ∅) → 𝐴 = (𝐸 ∖ {𝐼, 𝐽})) |
54 | 46, 52, 53 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅) → 𝐴 = (𝐸 ∖ {𝐼, 𝐽})) |
55 | 54 | ex 416 |
. . 3
⊢ (𝜑 → ((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅ → 𝐴 = (𝐸 ∖ {𝐼, 𝐽}))) |
56 | 12 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → 𝐴 ⊆ (𝐸 ∖ {𝐼})) |
57 | 14, 49 | eqsstrrid 3950 |
. . . . . . . 8
⊢ (𝜑 → ((𝐸 ∖ {𝐼}) ∖ {𝐽}) ⊆ 𝐴) |
58 | 57 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → ((𝐸 ∖ {𝐼}) ∖ {𝐽}) ⊆ 𝐴) |
59 | | ssundif 4399 |
. . . . . . 7
⊢ ((𝐸 ∖ {𝐼}) ⊆ ({𝐽} ∪ 𝐴) ↔ ((𝐸 ∖ {𝐼}) ∖ {𝐽}) ⊆ 𝐴) |
60 | 58, 59 | sylibr 237 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → (𝐸 ∖ {𝐼}) ⊆ ({𝐽} ∪ 𝐴)) |
61 | | ssidd 3924 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → {𝐽} ⊆ {𝐽}) |
62 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) |
63 | 61, 62 | sseqtrrd 3942 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → {𝐽} ⊆ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽}))) |
64 | 63 | difss2d 4049 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → {𝐽} ⊆ 𝐴) |
65 | | ssequn1 4094 |
. . . . . . 7
⊢ ({𝐽} ⊆ 𝐴 ↔ ({𝐽} ∪ 𝐴) = 𝐴) |
66 | 64, 65 | sylib 221 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → ({𝐽} ∪ 𝐴) = 𝐴) |
67 | 60, 66 | sseqtrd 3941 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → (𝐸 ∖ {𝐼}) ⊆ 𝐴) |
68 | 56, 67 | eqssd 3918 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → 𝐴 = (𝐸 ∖ {𝐼})) |
69 | 68 | ex 416 |
. . 3
⊢ (𝜑 → ((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽} → 𝐴 = (𝐸 ∖ {𝐼}))) |
70 | 55, 69 | orim12d 965 |
. 2
⊢ (𝜑 → (((𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = ∅ ∨ (𝐴 ∖ (𝐸 ∖ {𝐼, 𝐽})) = {𝐽}) → (𝐴 = (𝐸 ∖ {𝐼, 𝐽}) ∨ 𝐴 = (𝐸 ∖ {𝐼})))) |
71 | 45, 70 | mpd 15 |
1
⊢ (𝜑 → (𝐴 = (𝐸 ∖ {𝐼, 𝐽}) ∨ 𝐴 = (𝐸 ∖ {𝐼}))) |