Proof of Theorem symgvalstruct
Step | Hyp | Ref
| Expression |
1 | | hashv01gt1 13702 |
. 2
⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 0 ∨ (♯‘𝐴) = 1 ∨ 1 < (♯‘𝐴))) |
2 | | hasheq0 13721 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅)) |
3 | | 0symgefmndeq 18517 |
. . . . . . . . 9
⊢
(EndoFMnd‘∅) = (SymGrp‘∅) |
4 | 3 | eqcomi 2829 |
. . . . . . . 8
⊢
(SymGrp‘∅) = (EndoFMnd‘∅) |
5 | | symgvalstruct.g |
. . . . . . . . 9
⊢ 𝐺 = (SymGrp‘𝐴) |
6 | | fveq2 6663 |
. . . . . . . . 9
⊢ (𝐴 = ∅ →
(SymGrp‘𝐴) =
(SymGrp‘∅)) |
7 | 5, 6 | syl5eq 2867 |
. . . . . . . 8
⊢ (𝐴 = ∅ → 𝐺 =
(SymGrp‘∅)) |
8 | | fveq2 6663 |
. . . . . . . 8
⊢ (𝐴 = ∅ →
(EndoFMnd‘𝐴) =
(EndoFMnd‘∅)) |
9 | 4, 7, 8 | 3eqtr4a 2881 |
. . . . . . 7
⊢ (𝐴 = ∅ → 𝐺 = (EndoFMnd‘𝐴)) |
10 | 9 | adantl 484 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = ∅) → 𝐺 = (EndoFMnd‘𝐴)) |
11 | | eqid 2820 |
. . . . . . . 8
⊢
(EndoFMnd‘𝐴) =
(EndoFMnd‘𝐴) |
12 | | symgvalstruct.m |
. . . . . . . 8
⊢ 𝑀 = (𝐴 ↑m 𝐴) |
13 | | symgvalstruct.p |
. . . . . . . 8
⊢ + = (𝑓 ∈ 𝑀, 𝑔 ∈ 𝑀 ↦ (𝑓 ∘ 𝑔)) |
14 | | symgvalstruct.j |
. . . . . . . 8
⊢ 𝐽 =
(∏t‘(𝐴 × {𝒫 𝐴})) |
15 | 11, 12, 13, 14 | efmnd 18030 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (EndoFMnd‘𝐴) = {〈(Base‘ndx), 𝑀〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
16 | 15 | adantr 483 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = ∅) → (EndoFMnd‘𝐴) = {〈(Base‘ndx),
𝑀〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
17 | | 0map0sn0 8442 |
. . . . . . . . . . 11
⊢ (∅
↑m ∅) = {∅} |
18 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∅ → 𝐴 = ∅) |
19 | 18, 18 | oveq12d 7167 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ → (𝐴 ↑m 𝐴) = (∅ ↑m
∅)) |
20 | | symgvalstruct.b |
. . . . . . . . . . . 12
⊢ 𝐵 = {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} |
21 | 7 | fveq2d 6667 |
. . . . . . . . . . . . 13
⊢ (𝐴 = ∅ →
(Base‘𝐺) =
(Base‘(SymGrp‘∅))) |
22 | | eqid 2820 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝐺) =
(Base‘𝐺) |
23 | 5, 22 | symgbas 18494 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐺) =
{𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} |
24 | | symgbas0 18512 |
. . . . . . . . . . . . 13
⊢
(Base‘(SymGrp‘∅)) = {∅} |
25 | 21, 23, 24 | 3eqtr3g 2878 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∅ → {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} = {∅}) |
26 | 20, 25 | syl5eq 2867 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ → 𝐵 = {∅}) |
27 | 17, 19, 26 | 3eqtr4a 2881 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ → (𝐴 ↑m 𝐴) = 𝐵) |
28 | 27 | adantl 484 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = ∅) → (𝐴 ↑m 𝐴) = 𝐵) |
29 | 12, 28 | syl5eq 2867 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = ∅) → 𝑀 = 𝐵) |
30 | 29 | opeq2d 4803 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = ∅) → 〈(Base‘ndx),
𝑀〉 =
〈(Base‘ndx), 𝐵〉) |
31 | 30 | tpeq1d 4674 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = ∅) → {〈(Base‘ndx),
𝑀〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉} = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
32 | 10, 16, 31 | 3eqtrd 2859 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = ∅) → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
33 | 32 | ex 415 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (𝐴 = ∅ → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉})) |
34 | 2, 33 | sylbid 242 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 0 → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉})) |
35 | | hash1snb 13777 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 1 ↔ ∃𝑥 𝐴 = {𝑥})) |
36 | | snex 5325 |
. . . . . . . 8
⊢ {𝑥} ∈ V |
37 | | eleq1 2899 |
. . . . . . . 8
⊢ (𝐴 = {𝑥} → (𝐴 ∈ V ↔ {𝑥} ∈ V)) |
38 | 36, 37 | mpbiri 260 |
. . . . . . 7
⊢ (𝐴 = {𝑥} → 𝐴 ∈ V) |
39 | 11, 12, 13, 14 | efmnd 18030 |
. . . . . . 7
⊢ (𝐴 ∈ V →
(EndoFMnd‘𝐴) =
{〈(Base‘ndx), 𝑀〉, 〈(+g‘ndx),
+ 〉,
〈(TopSet‘ndx), 𝐽〉}) |
40 | 38, 39 | syl 17 |
. . . . . 6
⊢ (𝐴 = {𝑥} → (EndoFMnd‘𝐴) = {〈(Base‘ndx), 𝑀〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
41 | | snsymgefmndeq 18518 |
. . . . . . 7
⊢ (𝐴 = {𝑥} → (EndoFMnd‘𝐴) = (SymGrp‘𝐴)) |
42 | 41, 5 | syl6eqr 2873 |
. . . . . 6
⊢ (𝐴 = {𝑥} → (EndoFMnd‘𝐴) = 𝐺) |
43 | 42 | fveq2d 6667 |
. . . . . . . . 9
⊢ (𝐴 = {𝑥} → (Base‘(EndoFMnd‘𝐴)) = (Base‘𝐺)) |
44 | | eqid 2820 |
. . . . . . . . . . 11
⊢
(Base‘(EndoFMnd‘𝐴)) = (Base‘(EndoFMnd‘𝐴)) |
45 | 11, 44 | efmndbas 18031 |
. . . . . . . . . 10
⊢
(Base‘(EndoFMnd‘𝐴)) = (𝐴 ↑m 𝐴) |
46 | 45, 12 | eqtr4i 2846 |
. . . . . . . . 9
⊢
(Base‘(EndoFMnd‘𝐴)) = 𝑀 |
47 | 23, 20 | eqtr4i 2846 |
. . . . . . . . 9
⊢
(Base‘𝐺) =
𝐵 |
48 | 43, 46, 47 | 3eqtr3g 2878 |
. . . . . . . 8
⊢ (𝐴 = {𝑥} → 𝑀 = 𝐵) |
49 | 48 | opeq2d 4803 |
. . . . . . 7
⊢ (𝐴 = {𝑥} → 〈(Base‘ndx), 𝑀〉 = 〈(Base‘ndx),
𝐵〉) |
50 | 49 | tpeq1d 4674 |
. . . . . 6
⊢ (𝐴 = {𝑥} → {〈(Base‘ndx), 𝑀〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉} = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
51 | 40, 42, 50 | 3eqtr3d 2863 |
. . . . 5
⊢ (𝐴 = {𝑥} → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
52 | 51 | exlimiv 1930 |
. . . 4
⊢
(∃𝑥 𝐴 = {𝑥} → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
53 | 35, 52 | syl6bi 255 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 1 → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉})) |
54 | | ssnpss 4073 |
. . . . . . 7
⊢ ((𝐴 ↑m 𝐴) ⊆ 𝐵 → ¬ 𝐵 ⊊ (𝐴 ↑m 𝐴)) |
55 | 11, 5 | symgpssefmnd 18519 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → (Base‘𝐺) ⊊
(Base‘(EndoFMnd‘𝐴))) |
56 | 20, 23 | eqtr4i 2846 |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐺) |
57 | 45 | eqcomi 2829 |
. . . . . . . . 9
⊢ (𝐴 ↑m 𝐴) =
(Base‘(EndoFMnd‘𝐴)) |
58 | 56, 57 | psseq12i 4061 |
. . . . . . . 8
⊢ (𝐵 ⊊ (𝐴 ↑m 𝐴) ↔ (Base‘𝐺) ⊊ (Base‘(EndoFMnd‘𝐴))) |
59 | 55, 58 | sylibr 236 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → 𝐵 ⊊ (𝐴 ↑m 𝐴)) |
60 | 54, 59 | nsyl3 140 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → ¬ (𝐴 ↑m 𝐴) ⊆ 𝐵) |
61 | | fvexd 6678 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → (EndoFMnd‘𝐴) ∈ V) |
62 | 5, 56 | symgbasex 18495 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → 𝐵 ∈ V) |
63 | 62 | adantr 483 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → 𝐵 ∈ V) |
64 | 5, 20 | symgval 18492 |
. . . . . . 7
⊢ 𝐺 = ((EndoFMnd‘𝐴) ↾s 𝐵) |
65 | 64, 57 | ressval2 16548 |
. . . . . 6
⊢ ((¬
(𝐴 ↑m 𝐴) ⊆ 𝐵 ∧ (EndoFMnd‘𝐴) ∈ V ∧ 𝐵 ∈ V) → 𝐺 = ((EndoFMnd‘𝐴) sSet 〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉)) |
66 | 60, 61, 63, 65 | syl3anc 1366 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → 𝐺 = ((EndoFMnd‘𝐴) sSet 〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉)) |
67 | | ovex 7182 |
. . . . . . 7
⊢ (𝐴 ↑m 𝐴) ∈ V |
68 | 67 | inex2 5215 |
. . . . . 6
⊢ (𝐵 ∩ (𝐴 ↑m 𝐴)) ∈ V |
69 | | setsval 16508 |
. . . . . 6
⊢
(((EndoFMnd‘𝐴)
∈ V ∧ (𝐵 ∩
(𝐴 ↑m 𝐴)) ∈ V) →
((EndoFMnd‘𝐴) sSet
〈(Base‘ndx), (𝐵
∩ (𝐴 ↑m
𝐴))〉) =
(((EndoFMnd‘𝐴)
↾ (V ∖ {(Base‘ndx)})) ∪ {〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉})) |
70 | 61, 68, 69 | sylancl 588 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → ((EndoFMnd‘𝐴) sSet 〈(Base‘ndx),
(𝐵 ∩ (𝐴 ↑m 𝐴))〉) = (((EndoFMnd‘𝐴) ↾ (V ∖
{(Base‘ndx)})) ∪ {〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉})) |
71 | 15 | adantr 483 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → (EndoFMnd‘𝐴) = {〈(Base‘ndx),
𝑀〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
72 | 71 | reseq1d 5845 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → ((EndoFMnd‘𝐴) ↾ (V ∖
{(Base‘ndx)})) = ({〈(Base‘ndx), 𝑀〉, 〈(+g‘ndx),
+ 〉,
〈(TopSet‘ndx), 𝐽〉} ↾ (V ∖
{(Base‘ndx)}))) |
73 | 72 | uneq1d 4131 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) →
(((EndoFMnd‘𝐴)
↾ (V ∖ {(Base‘ndx)})) ∪ {〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉}) = (({〈(Base‘ndx),
𝑀〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉} ↾ (V ∖
{(Base‘ndx)})) ∪ {〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉})) |
74 | | eqidd 2821 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) →
{〈(Base‘ndx), 𝑀〉, 〈(+g‘ndx),
+ 〉,
〈(TopSet‘ndx), 𝐽〉} = {〈(Base‘ndx), 𝑀〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
75 | | fvexd 6678 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) →
(+g‘ndx) ∈ V) |
76 | | fvexd 6678 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → (TopSet‘ndx)
∈ V) |
77 | 12, 67 | eqeltri 2908 |
. . . . . . . . . . 11
⊢ 𝑀 ∈ V |
78 | 77, 77 | mpoex 7770 |
. . . . . . . . . 10
⊢ (𝑓 ∈ 𝑀, 𝑔 ∈ 𝑀 ↦ (𝑓 ∘ 𝑔)) ∈ V |
79 | 13, 78 | eqeltri 2908 |
. . . . . . . . 9
⊢ + ∈
V |
80 | 79 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → + ∈ V) |
81 | 14 | fvexi 6677 |
. . . . . . . . 9
⊢ 𝐽 ∈ V |
82 | 81 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → 𝐽 ∈ V) |
83 | | basendxnplusgndx 16603 |
. . . . . . . . . 10
⊢
(Base‘ndx) ≠ (+g‘ndx) |
84 | 83 | necomi 3069 |
. . . . . . . . 9
⊢
(+g‘ndx) ≠ (Base‘ndx) |
85 | 84 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) →
(+g‘ndx) ≠ (Base‘ndx)) |
86 | | tsetndx 16654 |
. . . . . . . . . 10
⊢
(TopSet‘ndx) = 9 |
87 | | 1re 10634 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
88 | | 1lt9 11837 |
. . . . . . . . . . . 12
⊢ 1 <
9 |
89 | 87, 88 | gtneii 10745 |
. . . . . . . . . . 11
⊢ 9 ≠
1 |
90 | | df-base 16484 |
. . . . . . . . . . . 12
⊢ Base =
Slot 1 |
91 | | 1nn 11642 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ |
92 | 90, 91 | ndxarg 16503 |
. . . . . . . . . . 11
⊢
(Base‘ndx) = 1 |
93 | 89, 92 | neeqtrri 3088 |
. . . . . . . . . 10
⊢ 9 ≠
(Base‘ndx) |
94 | 86, 93 | eqnetri 3085 |
. . . . . . . . 9
⊢
(TopSet‘ndx) ≠ (Base‘ndx) |
95 | 94 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → (TopSet‘ndx)
≠ (Base‘ndx)) |
96 | 74, 75, 76, 80, 82, 85, 95 | tpres 6956 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) →
({〈(Base‘ndx), 𝑀〉, 〈(+g‘ndx),
+ 〉,
〈(TopSet‘ndx), 𝐽〉} ↾ (V ∖
{(Base‘ndx)})) = {〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
97 | 96 | uneq1d 4131 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) →
(({〈(Base‘ndx), 𝑀〉, 〈(+g‘ndx),
+ 〉,
〈(TopSet‘ndx), 𝐽〉} ↾ (V ∖
{(Base‘ndx)})) ∪ {〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉}) =
({〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉} ∪ {〈(Base‘ndx),
(𝐵 ∩ (𝐴 ↑m 𝐴))〉})) |
98 | | uncom 4122 |
. . . . . . . 8
⊢
({〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉} ∪ {〈(Base‘ndx),
(𝐵 ∩ (𝐴 ↑m 𝐴))〉}) = ({〈(Base‘ndx),
(𝐵 ∩ (𝐴 ↑m 𝐴))〉} ∪
{〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
99 | | tpass 4681 |
. . . . . . . 8
⊢
{〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉, 〈(+g‘ndx),
+ 〉,
〈(TopSet‘ndx), 𝐽〉} = ({〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉} ∪
{〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
100 | 98, 99 | eqtr4i 2846 |
. . . . . . 7
⊢
({〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉} ∪ {〈(Base‘ndx),
(𝐵 ∩ (𝐴 ↑m 𝐴))〉}) = {〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉, 〈(+g‘ndx),
+ 〉,
〈(TopSet‘ndx), 𝐽〉} |
101 | 5, 56 | symgbasmap 18500 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐵 → 𝑥 ∈ (𝐴 ↑m 𝐴)) |
102 | 101 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → (𝑥 ∈ 𝐵 → 𝑥 ∈ (𝐴 ↑m 𝐴))) |
103 | 102 | ssrdv 3966 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → 𝐵 ⊆ (𝐴 ↑m 𝐴)) |
104 | | df-ss 3945 |
. . . . . . . . . 10
⊢ (𝐵 ⊆ (𝐴 ↑m 𝐴) ↔ (𝐵 ∩ (𝐴 ↑m 𝐴)) = 𝐵) |
105 | 103, 104 | sylib 220 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → (𝐵 ∩ (𝐴 ↑m 𝐴)) = 𝐵) |
106 | 105 | opeq2d 4803 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) →
〈(Base‘ndx), (𝐵
∩ (𝐴 ↑m
𝐴))〉 =
〈(Base‘ndx), 𝐵〉) |
107 | 106 | tpeq1d 4674 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) →
{〈(Base‘ndx), (𝐵
∩ (𝐴 ↑m
𝐴))〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉} = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
108 | 100, 107 | syl5eq 2867 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) →
({〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉} ∪ {〈(Base‘ndx),
(𝐵 ∩ (𝐴 ↑m 𝐴))〉}) = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
109 | 73, 97, 108 | 3eqtrd 2859 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) →
(((EndoFMnd‘𝐴)
↾ (V ∖ {(Base‘ndx)})) ∪ {〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉}) = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
110 | 66, 70, 109 | 3eqtrd 2859 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
111 | 110 | ex 415 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (1 < (♯‘𝐴) → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉})) |
112 | 34, 53, 111 | 3jaod 1423 |
. 2
⊢ (𝐴 ∈ 𝑉 → (((♯‘𝐴) = 0 ∨ (♯‘𝐴) = 1 ∨ 1 < (♯‘𝐴)) → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉})) |
113 | 1, 112 | mpd 15 |
1
⊢ (𝐴 ∈ 𝑉 → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |