Proof of Theorem symgvalstruct
Step | Hyp | Ref
| Expression |
1 | | hashv01gt1 14057 |
. 2
⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 0 ∨ (♯‘𝐴) = 1 ∨ 1 < (♯‘𝐴))) |
2 | | hasheq0 14076 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅)) |
3 | | 0symgefmndeq 18999 |
. . . . . . . . 9
⊢
(EndoFMnd‘∅) = (SymGrp‘∅) |
4 | 3 | eqcomi 2749 |
. . . . . . . 8
⊢
(SymGrp‘∅) = (EndoFMnd‘∅) |
5 | | symgvalstruct.g |
. . . . . . . . 9
⊢ 𝐺 = (SymGrp‘𝐴) |
6 | | fveq2 6771 |
. . . . . . . . 9
⊢ (𝐴 = ∅ →
(SymGrp‘𝐴) =
(SymGrp‘∅)) |
7 | 5, 6 | eqtrid 2792 |
. . . . . . . 8
⊢ (𝐴 = ∅ → 𝐺 =
(SymGrp‘∅)) |
8 | | fveq2 6771 |
. . . . . . . 8
⊢ (𝐴 = ∅ →
(EndoFMnd‘𝐴) =
(EndoFMnd‘∅)) |
9 | 4, 7, 8 | 3eqtr4a 2806 |
. . . . . . 7
⊢ (𝐴 = ∅ → 𝐺 = (EndoFMnd‘𝐴)) |
10 | 9 | adantl 482 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = ∅) → 𝐺 = (EndoFMnd‘𝐴)) |
11 | | eqid 2740 |
. . . . . . . 8
⊢
(EndoFMnd‘𝐴) =
(EndoFMnd‘𝐴) |
12 | | symgvalstruct.m |
. . . . . . . 8
⊢ 𝑀 = (𝐴 ↑m 𝐴) |
13 | | symgvalstruct.p |
. . . . . . . 8
⊢ + = (𝑓 ∈ 𝑀, 𝑔 ∈ 𝑀 ↦ (𝑓 ∘ 𝑔)) |
14 | | symgvalstruct.j |
. . . . . . . 8
⊢ 𝐽 =
(∏t‘(𝐴 × {𝒫 𝐴})) |
15 | 11, 12, 13, 14 | efmnd 18507 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (EndoFMnd‘𝐴) = {〈(Base‘ndx), 𝑀〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
16 | 15 | adantr 481 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = ∅) → (EndoFMnd‘𝐴) = {〈(Base‘ndx),
𝑀〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
17 | | 0map0sn0 8656 |
. . . . . . . . . . 11
⊢ (∅
↑m ∅) = {∅} |
18 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∅ → 𝐴 = ∅) |
19 | 18, 18 | oveq12d 7289 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ → (𝐴 ↑m 𝐴) = (∅ ↑m
∅)) |
20 | | symgvalstruct.b |
. . . . . . . . . . . 12
⊢ 𝐵 = {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} |
21 | 7 | fveq2d 6775 |
. . . . . . . . . . . . 13
⊢ (𝐴 = ∅ →
(Base‘𝐺) =
(Base‘(SymGrp‘∅))) |
22 | | eqid 2740 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝐺) =
(Base‘𝐺) |
23 | 5, 22 | symgbas 18976 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐺) =
{𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} |
24 | | symgbas0 18994 |
. . . . . . . . . . . . 13
⊢
(Base‘(SymGrp‘∅)) = {∅} |
25 | 21, 23, 24 | 3eqtr3g 2803 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∅ → {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} = {∅}) |
26 | 20, 25 | eqtrid 2792 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ → 𝐵 = {∅}) |
27 | 17, 19, 26 | 3eqtr4a 2806 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ → (𝐴 ↑m 𝐴) = 𝐵) |
28 | 27 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = ∅) → (𝐴 ↑m 𝐴) = 𝐵) |
29 | 12, 28 | eqtrid 2792 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = ∅) → 𝑀 = 𝐵) |
30 | 29 | opeq2d 4817 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = ∅) → 〈(Base‘ndx),
𝑀〉 =
〈(Base‘ndx), 𝐵〉) |
31 | 30 | tpeq1d 4687 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = ∅) → {〈(Base‘ndx),
𝑀〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉} = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
32 | 10, 16, 31 | 3eqtrd 2784 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = ∅) → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
33 | 32 | ex 413 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (𝐴 = ∅ → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉})) |
34 | 2, 33 | sylbid 239 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 0 → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉})) |
35 | | hash1snb 14132 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 1 ↔ ∃𝑥 𝐴 = {𝑥})) |
36 | | snex 5358 |
. . . . . . . 8
⊢ {𝑥} ∈ V |
37 | | eleq1 2828 |
. . . . . . . 8
⊢ (𝐴 = {𝑥} → (𝐴 ∈ V ↔ {𝑥} ∈ V)) |
38 | 36, 37 | mpbiri 257 |
. . . . . . 7
⊢ (𝐴 = {𝑥} → 𝐴 ∈ V) |
39 | 11, 12, 13, 14 | efmnd 18507 |
. . . . . . 7
⊢ (𝐴 ∈ V →
(EndoFMnd‘𝐴) =
{〈(Base‘ndx), 𝑀〉, 〈(+g‘ndx),
+ 〉,
〈(TopSet‘ndx), 𝐽〉}) |
40 | 38, 39 | syl 17 |
. . . . . 6
⊢ (𝐴 = {𝑥} → (EndoFMnd‘𝐴) = {〈(Base‘ndx), 𝑀〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
41 | | snsymgefmndeq 19000 |
. . . . . . 7
⊢ (𝐴 = {𝑥} → (EndoFMnd‘𝐴) = (SymGrp‘𝐴)) |
42 | 41, 5 | eqtr4di 2798 |
. . . . . 6
⊢ (𝐴 = {𝑥} → (EndoFMnd‘𝐴) = 𝐺) |
43 | 42 | fveq2d 6775 |
. . . . . . . . 9
⊢ (𝐴 = {𝑥} → (Base‘(EndoFMnd‘𝐴)) = (Base‘𝐺)) |
44 | | eqid 2740 |
. . . . . . . . . . 11
⊢
(Base‘(EndoFMnd‘𝐴)) = (Base‘(EndoFMnd‘𝐴)) |
45 | 11, 44 | efmndbas 18508 |
. . . . . . . . . 10
⊢
(Base‘(EndoFMnd‘𝐴)) = (𝐴 ↑m 𝐴) |
46 | 45, 12 | eqtr4i 2771 |
. . . . . . . . 9
⊢
(Base‘(EndoFMnd‘𝐴)) = 𝑀 |
47 | 23, 20 | eqtr4i 2771 |
. . . . . . . . 9
⊢
(Base‘𝐺) =
𝐵 |
48 | 43, 46, 47 | 3eqtr3g 2803 |
. . . . . . . 8
⊢ (𝐴 = {𝑥} → 𝑀 = 𝐵) |
49 | 48 | opeq2d 4817 |
. . . . . . 7
⊢ (𝐴 = {𝑥} → 〈(Base‘ndx), 𝑀〉 = 〈(Base‘ndx),
𝐵〉) |
50 | 49 | tpeq1d 4687 |
. . . . . 6
⊢ (𝐴 = {𝑥} → {〈(Base‘ndx), 𝑀〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉} = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
51 | 40, 42, 50 | 3eqtr3d 2788 |
. . . . 5
⊢ (𝐴 = {𝑥} → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
52 | 51 | exlimiv 1937 |
. . . 4
⊢
(∃𝑥 𝐴 = {𝑥} → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
53 | 35, 52 | syl6bi 252 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 1 → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉})) |
54 | | ssnpss 4043 |
. . . . . . 7
⊢ ((𝐴 ↑m 𝐴) ⊆ 𝐵 → ¬ 𝐵 ⊊ (𝐴 ↑m 𝐴)) |
55 | 11, 5 | symgpssefmnd 19001 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → (Base‘𝐺) ⊊
(Base‘(EndoFMnd‘𝐴))) |
56 | 20, 23 | eqtr4i 2771 |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐺) |
57 | 45 | eqcomi 2749 |
. . . . . . . . 9
⊢ (𝐴 ↑m 𝐴) =
(Base‘(EndoFMnd‘𝐴)) |
58 | 56, 57 | psseq12i 4031 |
. . . . . . . 8
⊢ (𝐵 ⊊ (𝐴 ↑m 𝐴) ↔ (Base‘𝐺) ⊊ (Base‘(EndoFMnd‘𝐴))) |
59 | 55, 58 | sylibr 233 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → 𝐵 ⊊ (𝐴 ↑m 𝐴)) |
60 | 54, 59 | nsyl3 138 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → ¬ (𝐴 ↑m 𝐴) ⊆ 𝐵) |
61 | | fvexd 6786 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → (EndoFMnd‘𝐴) ∈ V) |
62 | | f1osetex 8630 |
. . . . . . . 8
⊢ {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} ∈ V |
63 | 20, 62 | eqeltri 2837 |
. . . . . . 7
⊢ 𝐵 ∈ V |
64 | 63 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → 𝐵 ∈ V) |
65 | 5, 20 | symgval 18974 |
. . . . . . 7
⊢ 𝐺 = ((EndoFMnd‘𝐴) ↾s 𝐵) |
66 | 65, 57 | ressval2 16944 |
. . . . . 6
⊢ ((¬
(𝐴 ↑m 𝐴) ⊆ 𝐵 ∧ (EndoFMnd‘𝐴) ∈ V ∧ 𝐵 ∈ V) → 𝐺 = ((EndoFMnd‘𝐴) sSet 〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉)) |
67 | 60, 61, 64, 66 | syl3anc 1370 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → 𝐺 = ((EndoFMnd‘𝐴) sSet 〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉)) |
68 | | ovex 7304 |
. . . . . . 7
⊢ (𝐴 ↑m 𝐴) ∈ V |
69 | 68 | inex2 5246 |
. . . . . 6
⊢ (𝐵 ∩ (𝐴 ↑m 𝐴)) ∈ V |
70 | | setsval 16866 |
. . . . . 6
⊢
(((EndoFMnd‘𝐴)
∈ V ∧ (𝐵 ∩
(𝐴 ↑m 𝐴)) ∈ V) →
((EndoFMnd‘𝐴) sSet
〈(Base‘ndx), (𝐵
∩ (𝐴 ↑m
𝐴))〉) =
(((EndoFMnd‘𝐴)
↾ (V ∖ {(Base‘ndx)})) ∪ {〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉})) |
71 | 61, 69, 70 | sylancl 586 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → ((EndoFMnd‘𝐴) sSet 〈(Base‘ndx),
(𝐵 ∩ (𝐴 ↑m 𝐴))〉) = (((EndoFMnd‘𝐴) ↾ (V ∖
{(Base‘ndx)})) ∪ {〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉})) |
72 | 15 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → (EndoFMnd‘𝐴) = {〈(Base‘ndx),
𝑀〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
73 | 72 | reseq1d 5889 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → ((EndoFMnd‘𝐴) ↾ (V ∖
{(Base‘ndx)})) = ({〈(Base‘ndx), 𝑀〉, 〈(+g‘ndx),
+ 〉,
〈(TopSet‘ndx), 𝐽〉} ↾ (V ∖
{(Base‘ndx)}))) |
74 | 73 | uneq1d 4101 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) →
(((EndoFMnd‘𝐴)
↾ (V ∖ {(Base‘ndx)})) ∪ {〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉}) = (({〈(Base‘ndx),
𝑀〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉} ↾ (V ∖
{(Base‘ndx)})) ∪ {〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉})) |
75 | | eqidd 2741 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) →
{〈(Base‘ndx), 𝑀〉, 〈(+g‘ndx),
+ 〉,
〈(TopSet‘ndx), 𝐽〉} = {〈(Base‘ndx), 𝑀〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
76 | | fvexd 6786 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) →
(+g‘ndx) ∈ V) |
77 | | fvexd 6786 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → (TopSet‘ndx)
∈ V) |
78 | 12, 68 | eqeltri 2837 |
. . . . . . . . . . 11
⊢ 𝑀 ∈ V |
79 | 78, 78 | mpoex 7913 |
. . . . . . . . . 10
⊢ (𝑓 ∈ 𝑀, 𝑔 ∈ 𝑀 ↦ (𝑓 ∘ 𝑔)) ∈ V |
80 | 13, 79 | eqeltri 2837 |
. . . . . . . . 9
⊢ + ∈
V |
81 | 80 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → + ∈ V) |
82 | 14 | fvexi 6785 |
. . . . . . . . 9
⊢ 𝐽 ∈ V |
83 | 82 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → 𝐽 ∈ V) |
84 | | basendxnplusgndx 16990 |
. . . . . . . . . 10
⊢
(Base‘ndx) ≠ (+g‘ndx) |
85 | 84 | necomi 3000 |
. . . . . . . . 9
⊢
(+g‘ndx) ≠ (Base‘ndx) |
86 | 85 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) →
(+g‘ndx) ≠ (Base‘ndx)) |
87 | | tsetndxnbasendx 17064 |
. . . . . . . . 9
⊢
(TopSet‘ndx) ≠ (Base‘ndx) |
88 | 87 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → (TopSet‘ndx)
≠ (Base‘ndx)) |
89 | 75, 76, 77, 81, 83, 86, 88 | tpres 7073 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) →
({〈(Base‘ndx), 𝑀〉, 〈(+g‘ndx),
+ 〉,
〈(TopSet‘ndx), 𝐽〉} ↾ (V ∖
{(Base‘ndx)})) = {〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
90 | 89 | uneq1d 4101 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) →
(({〈(Base‘ndx), 𝑀〉, 〈(+g‘ndx),
+ 〉,
〈(TopSet‘ndx), 𝐽〉} ↾ (V ∖
{(Base‘ndx)})) ∪ {〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉}) =
({〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉} ∪ {〈(Base‘ndx),
(𝐵 ∩ (𝐴 ↑m 𝐴))〉})) |
91 | | uncom 4092 |
. . . . . . . 8
⊢
({〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉} ∪ {〈(Base‘ndx),
(𝐵 ∩ (𝐴 ↑m 𝐴))〉}) = ({〈(Base‘ndx),
(𝐵 ∩ (𝐴 ↑m 𝐴))〉} ∪
{〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
92 | | tpass 4694 |
. . . . . . . 8
⊢
{〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉, 〈(+g‘ndx),
+ 〉,
〈(TopSet‘ndx), 𝐽〉} = ({〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉} ∪
{〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
93 | 91, 92 | eqtr4i 2771 |
. . . . . . 7
⊢
({〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉} ∪ {〈(Base‘ndx),
(𝐵 ∩ (𝐴 ↑m 𝐴))〉}) = {〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉, 〈(+g‘ndx),
+ 〉,
〈(TopSet‘ndx), 𝐽〉} |
94 | 5, 56 | symgbasmap 18982 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐵 → 𝑥 ∈ (𝐴 ↑m 𝐴)) |
95 | 94 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → (𝑥 ∈ 𝐵 → 𝑥 ∈ (𝐴 ↑m 𝐴))) |
96 | 95 | ssrdv 3932 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → 𝐵 ⊆ (𝐴 ↑m 𝐴)) |
97 | | df-ss 3909 |
. . . . . . . . . 10
⊢ (𝐵 ⊆ (𝐴 ↑m 𝐴) ↔ (𝐵 ∩ (𝐴 ↑m 𝐴)) = 𝐵) |
98 | 96, 97 | sylib 217 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → (𝐵 ∩ (𝐴 ↑m 𝐴)) = 𝐵) |
99 | 98 | opeq2d 4817 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) →
〈(Base‘ndx), (𝐵
∩ (𝐴 ↑m
𝐴))〉 =
〈(Base‘ndx), 𝐵〉) |
100 | 99 | tpeq1d 4687 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) →
{〈(Base‘ndx), (𝐵
∩ (𝐴 ↑m
𝐴))〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉} = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
101 | 93, 100 | eqtrid 2792 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) →
({〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉} ∪ {〈(Base‘ndx),
(𝐵 ∩ (𝐴 ↑m 𝐴))〉}) = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
102 | 74, 90, 101 | 3eqtrd 2784 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) →
(((EndoFMnd‘𝐴)
↾ (V ∖ {(Base‘ndx)})) ∪ {〈(Base‘ndx), (𝐵 ∩ (𝐴 ↑m 𝐴))〉}) = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
103 | 67, 71, 102 | 3eqtrd 2784 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 1 < (♯‘𝐴)) → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
104 | 103 | ex 413 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (1 < (♯‘𝐴) → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉})) |
105 | 34, 53, 104 | 3jaod 1427 |
. 2
⊢ (𝐴 ∈ 𝑉 → (((♯‘𝐴) = 0 ∨ (♯‘𝐴) = 1 ∨ 1 < (♯‘𝐴)) → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉})) |
106 | 1, 105 | mpd 15 |
1
⊢ (𝐴 ∈ 𝑉 → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |