Step | Hyp | Ref
| Expression |
1 | | saluni 43847 |
. 2
⊢ (𝑍 ∈ SAlg → ∪ 𝑍
∈ 𝑍) |
2 | | salgencntex.z |
. . . . . . . 8
⊢ 𝑍 = ∩
{𝑠 ∈ SAlg ∣
𝐶 ⊆ 𝑠} |
3 | | salgencntex.t |
. . . . . . . . . . . 12
⊢ 𝑇 = 𝒫 𝐵 |
4 | | salgencntex.b |
. . . . . . . . . . . . . 14
⊢ 𝐵 = (0[,]1) |
5 | | ovex 7305 |
. . . . . . . . . . . . . 14
⊢ (0[,]1)
∈ V |
6 | 4, 5 | eqeltri 2837 |
. . . . . . . . . . . . 13
⊢ 𝐵 ∈ V |
7 | | pwsal 43838 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ V → 𝒫 𝐵 ∈ SAlg) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ 𝒫
𝐵 ∈
SAlg |
9 | 3, 8 | eqeltri 2837 |
. . . . . . . . . . 11
⊢ 𝑇 ∈ SAlg |
10 | | salgencntex.c |
. . . . . . . . . . . 12
⊢ 𝐶 = (𝑆 ∩ 𝑇) |
11 | | inss2 4169 |
. . . . . . . . . . . 12
⊢ (𝑆 ∩ 𝑇) ⊆ 𝑇 |
12 | 10, 11 | eqsstri 3960 |
. . . . . . . . . . 11
⊢ 𝐶 ⊆ 𝑇 |
13 | 9, 12 | pm3.2i 471 |
. . . . . . . . . 10
⊢ (𝑇 ∈ SAlg ∧ 𝐶 ⊆ 𝑇) |
14 | | sseq2 3952 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑇 → (𝐶 ⊆ 𝑠 ↔ 𝐶 ⊆ 𝑇)) |
15 | 14 | elrab 3626 |
. . . . . . . . . 10
⊢ (𝑇 ∈ {𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠} ↔ (𝑇 ∈ SAlg ∧ 𝐶 ⊆ 𝑇)) |
16 | 13, 15 | mpbir 230 |
. . . . . . . . 9
⊢ 𝑇 ∈ {𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠} |
17 | | intss1 4900 |
. . . . . . . . 9
⊢ (𝑇 ∈ {𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠} → ∩ {𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠} ⊆ 𝑇) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . 8
⊢ ∩ {𝑠
∈ SAlg ∣ 𝐶
⊆ 𝑠} ⊆ 𝑇 |
19 | 2, 18 | eqsstri 3960 |
. . . . . . 7
⊢ 𝑍 ⊆ 𝑇 |
20 | 19 | unissi 4854 |
. . . . . 6
⊢ ∪ 𝑍
⊆ ∪ 𝑇 |
21 | 3 | unieqi 4858 |
. . . . . . 7
⊢ ∪ 𝑇 =
∪ 𝒫 𝐵 |
22 | | unipw 5370 |
. . . . . . 7
⊢ ∪ 𝒫 𝐵 = 𝐵 |
23 | 21, 22 | eqtri 2768 |
. . . . . 6
⊢ ∪ 𝑇 =
𝐵 |
24 | 20, 23 | sseqtri 3962 |
. . . . 5
⊢ ∪ 𝑍
⊆ 𝐵 |
25 | | sseq2 3952 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = 𝑡 → (𝐶 ⊆ 𝑠 ↔ 𝐶 ⊆ 𝑡)) |
26 | 25 | elrab 3626 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ {𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠} ↔ (𝑡 ∈ SAlg ∧ 𝐶 ⊆ 𝑡)) |
27 | 26 | biimpi 215 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ {𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠} → (𝑡 ∈ SAlg ∧ 𝐶 ⊆ 𝑡)) |
28 | 27 | simprd 496 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ {𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠} → 𝐶 ⊆ 𝑡) |
29 | 28 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑡 ∈ {𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠}) → 𝐶 ⊆ 𝑡) |
30 | | 0red 10989 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ 𝐵 → 0 ∈ ℝ) |
31 | | 2re 12058 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
ℝ |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ 𝐵 → 2 ∈ ℝ) |
33 | | unitssre 13242 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0[,]1)
⊆ ℝ |
34 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐵) |
35 | 34, 4 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ (0[,]1)) |
36 | 33, 35 | sselid 3924 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ ℝ) |
37 | 30 | rexrd 11036 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ 𝐵 → 0 ∈
ℝ*) |
38 | | 1xr 11045 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℝ* |
39 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ 𝐵 → 1 ∈
ℝ*) |
40 | | iccgelb 13146 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑦 ∈ (0[,]1)) → 0 ≤
𝑦) |
41 | 37, 39, 35, 40 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ 𝐵 → 0 ≤ 𝑦) |
42 | | 1re 10986 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℝ |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ 𝐵 → 1 ∈ ℝ) |
44 | | iccleub 13145 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑦 ∈ (0[,]1)) → 𝑦 ≤ 1) |
45 | 37, 39, 35, 44 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ 𝐵 → 𝑦 ≤ 1) |
46 | | 1le2 12193 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ≤
2 |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ 𝐵 → 1 ≤ 2) |
48 | 36, 43, 32, 45, 47 | letrd 11143 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ 𝐵 → 𝑦 ≤ 2) |
49 | 30, 32, 36, 41, 48 | eliccd 43024 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ (0[,]2)) |
50 | | salgencntex.a |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐴 = (0[,]2) |
51 | 49, 50 | eleqtrrdi 2852 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐴) |
52 | | snelpwi 5364 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ 𝐴 → {𝑦} ∈ 𝒫 𝐴) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝐵 → {𝑦} ∈ 𝒫 𝐴) |
54 | | snfi 8826 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {𝑦} ∈ Fin |
55 | | fict 9399 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({𝑦} ∈ Fin → {𝑦} ≼
ω) |
56 | 54, 55 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑦} ≼
ω |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ 𝐵 → {𝑦} ≼ ω) |
58 | | orc 864 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({𝑦} ≼ ω → ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝐵 → ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)) |
60 | 53, 59 | jca 512 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝐵 → ({𝑦} ∈ 𝒫 𝐴 ∧ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω))) |
61 | | breq1 5082 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = {𝑦} → (𝑥 ≼ ω ↔ {𝑦} ≼ ω)) |
62 | | difeq2 4056 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = {𝑦} → (𝐴 ∖ 𝑥) = (𝐴 ∖ {𝑦})) |
63 | 62 | breq1d 5089 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = {𝑦} → ((𝐴 ∖ 𝑥) ≼ ω ↔ (𝐴 ∖ {𝑦}) ≼ ω)) |
64 | 61, 63 | orbi12d 916 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = {𝑦} → ((𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω) ↔ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω))) |
65 | | salgencntex.s |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)} |
66 | 64, 65 | elrab2 3629 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑦} ∈ 𝑆 ↔ ({𝑦} ∈ 𝒫 𝐴 ∧ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω))) |
67 | 60, 66 | sylibr 233 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝐵 → {𝑦} ∈ 𝑆) |
68 | | snelpwi 5364 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝐵 → {𝑦} ∈ 𝒫 𝐵) |
69 | 68, 3 | eleqtrrdi 2852 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝐵 → {𝑦} ∈ 𝑇) |
70 | 67, 69 | elind 4133 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝐵 → {𝑦} ∈ (𝑆 ∩ 𝑇)) |
71 | 10 | eqcomi 2749 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ∩ 𝑇) = 𝐶 |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝐵 → (𝑆 ∩ 𝑇) = 𝐶) |
73 | 70, 72 | eleqtrd 2843 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐵 → {𝑦} ∈ 𝐶) |
74 | 73 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑡 ∈ {𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠}) → {𝑦} ∈ 𝐶) |
75 | 29, 74 | sseldd 3927 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑡 ∈ {𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠}) → {𝑦} ∈ 𝑡) |
76 | 75 | ralrimiva 3110 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐵 → ∀𝑡 ∈ {𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠} {𝑦} ∈ 𝑡) |
77 | | snex 5358 |
. . . . . . . . . . . 12
⊢ {𝑦} ∈ V |
78 | 77 | elint2 4892 |
. . . . . . . . . . 11
⊢ ({𝑦} ∈ ∩ {𝑠
∈ SAlg ∣ 𝐶
⊆ 𝑠} ↔
∀𝑡 ∈ {𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠} {𝑦} ∈ 𝑡) |
79 | 76, 78 | sylibr 233 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐵 → {𝑦} ∈ ∩ {𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠}) |
80 | 79, 2 | eleqtrrdi 2852 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 → {𝑦} ∈ 𝑍) |
81 | | snidg 4601 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ {𝑦}) |
82 | | eleq2 2829 |
. . . . . . . . . 10
⊢ (𝑤 = {𝑦} → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ {𝑦})) |
83 | 82 | rspcev 3561 |
. . . . . . . . 9
⊢ (({𝑦} ∈ 𝑍 ∧ 𝑦 ∈ {𝑦}) → ∃𝑤 ∈ 𝑍 𝑦 ∈ 𝑤) |
84 | 80, 81, 83 | syl2anc 584 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → ∃𝑤 ∈ 𝑍 𝑦 ∈ 𝑤) |
85 | | eluni2 4849 |
. . . . . . . 8
⊢ (𝑦 ∈ ∪ 𝑍
↔ ∃𝑤 ∈
𝑍 𝑦 ∈ 𝑤) |
86 | 84, 85 | sylibr 233 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ ∪ 𝑍) |
87 | 86 | rgen 3076 |
. . . . . 6
⊢
∀𝑦 ∈
𝐵 𝑦 ∈ ∪ 𝑍 |
88 | | dfss3 3914 |
. . . . . 6
⊢ (𝐵 ⊆ ∪ 𝑍
↔ ∀𝑦 ∈
𝐵 𝑦 ∈ ∪ 𝑍) |
89 | 87, 88 | mpbir 230 |
. . . . 5
⊢ 𝐵 ⊆ ∪ 𝑍 |
90 | 24, 89 | eqssi 3942 |
. . . 4
⊢ ∪ 𝑍 =
𝐵 |
91 | | ovex 7305 |
. . . . . . . . . . . . . 14
⊢ (0[,]2)
∈ V |
92 | 50, 91 | eqeltri 2837 |
. . . . . . . . . . . . 13
⊢ 𝐴 ∈ V |
93 | 92 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ 𝐴 ∈
V) |
94 | 93, 65 | salexct 43855 |
. . . . . . . . . . 11
⊢ (⊤
→ 𝑆 ∈
SAlg) |
95 | 94 | mptru 1549 |
. . . . . . . . . 10
⊢ 𝑆 ∈ SAlg |
96 | | inss1 4168 |
. . . . . . . . . . 11
⊢ (𝑆 ∩ 𝑇) ⊆ 𝑆 |
97 | 10, 96 | eqsstri 3960 |
. . . . . . . . . 10
⊢ 𝐶 ⊆ 𝑆 |
98 | 95, 97 | pm3.2i 471 |
. . . . . . . . 9
⊢ (𝑆 ∈ SAlg ∧ 𝐶 ⊆ 𝑆) |
99 | | sseq2 3952 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑆 → (𝐶 ⊆ 𝑠 ↔ 𝐶 ⊆ 𝑆)) |
100 | 99 | elrab 3626 |
. . . . . . . . 9
⊢ (𝑆 ∈ {𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠} ↔ (𝑆 ∈ SAlg ∧ 𝐶 ⊆ 𝑆)) |
101 | 98, 100 | mpbir 230 |
. . . . . . . 8
⊢ 𝑆 ∈ {𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠} |
102 | | intss1 4900 |
. . . . . . . 8
⊢ (𝑆 ∈ {𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠} → ∩ {𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠} ⊆ 𝑆) |
103 | 101, 102 | ax-mp 5 |
. . . . . . 7
⊢ ∩ {𝑠
∈ SAlg ∣ 𝐶
⊆ 𝑠} ⊆ 𝑆 |
104 | 2, 103 | eqsstri 3960 |
. . . . . 6
⊢ 𝑍 ⊆ 𝑆 |
105 | 104 | sseli 3922 |
. . . . 5
⊢ (𝐵 ∈ 𝑍 → 𝐵 ∈ 𝑆) |
106 | 50, 65, 4 | salexct2 43860 |
. . . . . 6
⊢ ¬
𝐵 ∈ 𝑆 |
107 | 106 | a1i 11 |
. . . . 5
⊢ (𝐵 ∈ 𝑍 → ¬ 𝐵 ∈ 𝑆) |
108 | 105, 107 | pm2.65i 193 |
. . . 4
⊢ ¬
𝐵 ∈ 𝑍 |
109 | 90, 108 | eqneltri 2834 |
. . 3
⊢ ¬
∪ 𝑍 ∈ 𝑍 |
110 | 109 | a1i 11 |
. 2
⊢ (𝑍 ∈ SAlg → ¬ ∪ 𝑍
∈ 𝑍) |
111 | 1, 110 | pm2.65i 193 |
1
⊢ ¬
𝑍 ∈
SAlg |