Theorem salgencntex

Description: This counterexample shows that df-salgen needs to require that all containing sigma-algebra have the same base set. Otherwise, the intersection could lead to a set that is not a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypotheses	salgencntex.a	⊢ 𝐴 = ( 0 [,] 2 )
	salgencntex.s	⊢ 𝑆 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) }
	salgencntex.b	⊢ 𝐵 = ( 0 [,] 1 )
	salgencntex.t	⊢ 𝑇 = 𝒫 𝐵
	salgencntex.c	⊢ 𝐶 = ( 𝑆 ∩ 𝑇 )
	salgencntex.z	⊢ 𝑍 = ∩ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 }
Assertion	salgencntex	⊢ ¬ 𝑍 ∈ SAlg

Proof

Step	Hyp	Ref	Expression
1		salgencntex.a	⊢ 𝐴 = ( 0 [,] 2 )
2		salgencntex.s	⊢ 𝑆 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) }
3		salgencntex.b	⊢ 𝐵 = ( 0 [,] 1 )
4		salgencntex.t	⊢ 𝑇 = 𝒫 𝐵
5		salgencntex.c	⊢ 𝐶 = ( 𝑆 ∩ 𝑇 )
6		salgencntex.z	⊢ 𝑍 = ∩ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 }
7		saluni	⊢ ( 𝑍 ∈ SAlg → ∪ 𝑍 ∈ 𝑍 )
8		ovex	⊢ ( 0 [,] 1 ) ∈ V
9	3 8	eqeltri	⊢ 𝐵 ∈ V
10		pwsal	⊢ ( 𝐵 ∈ V → 𝒫 𝐵 ∈ SAlg )
11	9 10	ax-mp	⊢ 𝒫 𝐵 ∈ SAlg
12	4 11	eqeltri	⊢ 𝑇 ∈ SAlg
13		inss2	⊢ ( 𝑆 ∩ 𝑇 ) ⊆ 𝑇
14	5 13	eqsstri	⊢ 𝐶 ⊆ 𝑇
15	12 14	pm3.2i	⊢ ( 𝑇 ∈ SAlg ∧ 𝐶 ⊆ 𝑇 )
16		sseq2	⊢ ( 𝑠 = 𝑇 → ( 𝐶 ⊆ 𝑠 ↔ 𝐶 ⊆ 𝑇 ) )
17	16	elrab	⊢ ( 𝑇 ∈ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 } ↔ ( 𝑇 ∈ SAlg ∧ 𝐶 ⊆ 𝑇 ) )
18	15 17	mpbir	⊢ 𝑇 ∈ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 }
19		intss1	⊢ ( 𝑇 ∈ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 } → ∩ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 } ⊆ 𝑇 )
20	18 19	ax-mp	⊢ ∩ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 } ⊆ 𝑇
21	6 20	eqsstri	⊢ 𝑍 ⊆ 𝑇
22	21	unissi	⊢ ∪ 𝑍 ⊆ ∪ 𝑇
23	4	unieqi	⊢ ∪ 𝑇 = ∪ 𝒫 𝐵
24		unipw	⊢ ∪ 𝒫 𝐵 = 𝐵
25	23 24	eqtri	⊢ ∪ 𝑇 = 𝐵
26	22 25	sseqtri	⊢ ∪ 𝑍 ⊆ 𝐵
27		sseq2	⊢ ( 𝑠 = 𝑡 → ( 𝐶 ⊆ 𝑠 ↔ 𝐶 ⊆ 𝑡 ) )
28	27	elrab	⊢ ( 𝑡 ∈ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 } ↔ ( 𝑡 ∈ SAlg ∧ 𝐶 ⊆ 𝑡 ) )
29	28	biimpi	⊢ ( 𝑡 ∈ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 } → ( 𝑡 ∈ SAlg ∧ 𝐶 ⊆ 𝑡 ) )
30	29	simprd	⊢ ( 𝑡 ∈ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 } → 𝐶 ⊆ 𝑡 )
31	30	adantl	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑡 ∈ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 } ) → 𝐶 ⊆ 𝑡 )
32		0red	⊢ ( 𝑦 ∈ 𝐵 → 0 ∈ ℝ )
33		2re	⊢ 2 ∈ ℝ
34	33	a1i	⊢ ( 𝑦 ∈ 𝐵 → 2 ∈ ℝ )
35		unitssre	⊢ ( 0 [,] 1 ) ⊆ ℝ
36		id	⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐵 )
37	36 3	eleqtrdi	⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ( 0 [,] 1 ) )
38	35 37	sselid	⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ℝ )
39	32	rexrd	⊢ ( 𝑦 ∈ 𝐵 → 0 ∈ ℝ* )
40		1xr	⊢ 1 ∈ ℝ*
41	40	a1i	⊢ ( 𝑦 ∈ 𝐵 → 1 ∈ ℝ* )
42		iccgelb	⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑦 ∈ ( 0 [,] 1 ) ) → 0 ≤ 𝑦 )
43	39 41 37 42	syl3anc	⊢ ( 𝑦 ∈ 𝐵 → 0 ≤ 𝑦 )
44		1re	⊢ 1 ∈ ℝ
45	44	a1i	⊢ ( 𝑦 ∈ 𝐵 → 1 ∈ ℝ )
46		iccleub	⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑦 ∈ ( 0 [,] 1 ) ) → 𝑦 ≤ 1 )
47	39 41 37 46	syl3anc	⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ≤ 1 )
48		1le2	⊢ 1 ≤ 2
49	48	a1i	⊢ ( 𝑦 ∈ 𝐵 → 1 ≤ 2 )
50	38 45 34 47 49	letrd	⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ≤ 2 )
51	32 34 38 43 50	eliccd	⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ( 0 [,] 2 ) )
52	51 1	eleqtrrdi	⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐴 )
53		snelpwi	⊢ ( 𝑦 ∈ 𝐴 → { 𝑦 } ∈ 𝒫 𝐴 )
54	52 53	syl	⊢ ( 𝑦 ∈ 𝐵 → { 𝑦 } ∈ 𝒫 𝐴 )
55		snfi	⊢ { 𝑦 } ∈ Fin
56		fict	⊢ ( { 𝑦 } ∈ Fin → { 𝑦 } ≼ ω )
57	55 56	ax-mp	⊢ { 𝑦 } ≼ ω
58	57	a1i	⊢ ( 𝑦 ∈ 𝐵 → { 𝑦 } ≼ ω )
59		orc	⊢ ( { 𝑦 } ≼ ω → ( { 𝑦 } ≼ ω ∨ ( 𝐴 ∖ { 𝑦 } ) ≼ ω ) )
60	58 59	syl	⊢ ( 𝑦 ∈ 𝐵 → ( { 𝑦 } ≼ ω ∨ ( 𝐴 ∖ { 𝑦 } ) ≼ ω ) )
61	54 60	jca	⊢ ( 𝑦 ∈ 𝐵 → ( { 𝑦 } ∈ 𝒫 𝐴 ∧ ( { 𝑦 } ≼ ω ∨ ( 𝐴 ∖ { 𝑦 } ) ≼ ω ) ) )
62		breq1	⊢ ( 𝑥 = { 𝑦 } → ( 𝑥 ≼ ω ↔ { 𝑦 } ≼ ω ) )
63		difeq2	⊢ ( 𝑥 = { 𝑦 } → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ { 𝑦 } ) )
64	63	breq1d	⊢ ( 𝑥 = { 𝑦 } → ( ( 𝐴 ∖ 𝑥 ) ≼ ω ↔ ( 𝐴 ∖ { 𝑦 } ) ≼ ω ) )
65	62 64	orbi12d	⊢ ( 𝑥 = { 𝑦 } → ( ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) ↔ ( { 𝑦 } ≼ ω ∨ ( 𝐴 ∖ { 𝑦 } ) ≼ ω ) ) )
66	65 2	elrab2	⊢ ( { 𝑦 } ∈ 𝑆 ↔ ( { 𝑦 } ∈ 𝒫 𝐴 ∧ ( { 𝑦 } ≼ ω ∨ ( 𝐴 ∖ { 𝑦 } ) ≼ ω ) ) )
67	61 66	sylibr	⊢ ( 𝑦 ∈ 𝐵 → { 𝑦 } ∈ 𝑆 )
68		snelpwi	⊢ ( 𝑦 ∈ 𝐵 → { 𝑦 } ∈ 𝒫 𝐵 )
69	68 4	eleqtrrdi	⊢ ( 𝑦 ∈ 𝐵 → { 𝑦 } ∈ 𝑇 )
70	67 69	elind	⊢ ( 𝑦 ∈ 𝐵 → { 𝑦 } ∈ ( 𝑆 ∩ 𝑇 ) )
71	5	eqcomi	⊢ ( 𝑆 ∩ 𝑇 ) = 𝐶
72	71	a1i	⊢ ( 𝑦 ∈ 𝐵 → ( 𝑆 ∩ 𝑇 ) = 𝐶 )
73	70 72	eleqtrd	⊢ ( 𝑦 ∈ 𝐵 → { 𝑦 } ∈ 𝐶 )
74	73	adantr	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑡 ∈ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 } ) → { 𝑦 } ∈ 𝐶 )
75	31 74	sseldd	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑡 ∈ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 } ) → { 𝑦 } ∈ 𝑡 )
76	75	ralrimiva	⊢ ( 𝑦 ∈ 𝐵 → ∀ 𝑡 ∈ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 } { 𝑦 } ∈ 𝑡 )
77		snex	⊢ { 𝑦 } ∈ V
78	77	elint2	⊢ ( { 𝑦 } ∈ ∩ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 } ↔ ∀ 𝑡 ∈ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 } { 𝑦 } ∈ 𝑡 )
79	76 78	sylibr	⊢ ( 𝑦 ∈ 𝐵 → { 𝑦 } ∈ ∩ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 } )
80	79 6	eleqtrrdi	⊢ ( 𝑦 ∈ 𝐵 → { 𝑦 } ∈ 𝑍 )
81		snidg	⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ { 𝑦 } )
82		eleq2	⊢ ( 𝑤 = { 𝑦 } → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ { 𝑦 } ) )
83	82	rspcev	⊢ ( ( { 𝑦 } ∈ 𝑍 ∧ 𝑦 ∈ { 𝑦 } ) → ∃ 𝑤 ∈ 𝑍 𝑦 ∈ 𝑤 )
84	80 81 83	syl2anc	⊢ ( 𝑦 ∈ 𝐵 → ∃ 𝑤 ∈ 𝑍 𝑦 ∈ 𝑤 )
85		eluni2	⊢ ( 𝑦 ∈ ∪ 𝑍 ↔ ∃ 𝑤 ∈ 𝑍 𝑦 ∈ 𝑤 )
86	84 85	sylibr	⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ∪ 𝑍 )
87	86	rgen	⊢ ∀ 𝑦 ∈ 𝐵 𝑦 ∈ ∪ 𝑍
88		dfss3	⊢ ( 𝐵 ⊆ ∪ 𝑍 ↔ ∀ 𝑦 ∈ 𝐵 𝑦 ∈ ∪ 𝑍 )
89	87 88	mpbir	⊢ 𝐵 ⊆ ∪ 𝑍
90	26 89	eqssi	⊢ ∪ 𝑍 = 𝐵
91		ovex	⊢ ( 0 [,] 2 ) ∈ V
92	1 91	eqeltri	⊢ 𝐴 ∈ V
93	92	a1i	⊢ ( ⊤ → 𝐴 ∈ V )
94	93 2	salexct	⊢ ( ⊤ → 𝑆 ∈ SAlg )
95	94	mptru	⊢ 𝑆 ∈ SAlg
96		inss1	⊢ ( 𝑆 ∩ 𝑇 ) ⊆ 𝑆
97	5 96	eqsstri	⊢ 𝐶 ⊆ 𝑆
98	95 97	pm3.2i	⊢ ( 𝑆 ∈ SAlg ∧ 𝐶 ⊆ 𝑆 )
99		sseq2	⊢ ( 𝑠 = 𝑆 → ( 𝐶 ⊆ 𝑠 ↔ 𝐶 ⊆ 𝑆 ) )
100	99	elrab	⊢ ( 𝑆 ∈ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 } ↔ ( 𝑆 ∈ SAlg ∧ 𝐶 ⊆ 𝑆 ) )
101	98 100	mpbir	⊢ 𝑆 ∈ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 }
102		intss1	⊢ ( 𝑆 ∈ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 } → ∩ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 } ⊆ 𝑆 )
103	101 102	ax-mp	⊢ ∩ { 𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠 } ⊆ 𝑆
104	6 103	eqsstri	⊢ 𝑍 ⊆ 𝑆
105	104	sseli	⊢ ( 𝐵 ∈ 𝑍 → 𝐵 ∈ 𝑆 )
106	1 2 3	salexct2	⊢ ¬ 𝐵 ∈ 𝑆
107	106	a1i	⊢ ( 𝐵 ∈ 𝑍 → ¬ 𝐵 ∈ 𝑆 )
108	105 107	pm2.65i	⊢ ¬ 𝐵 ∈ 𝑍
109	90 108	eqneltri	⊢ ¬ ∪ 𝑍 ∈ 𝑍
110	109	a1i	⊢ ( 𝑍 ∈ SAlg → ¬ ∪ 𝑍 ∈ 𝑍 )
111	7 110	pm2.65i	⊢ ¬ 𝑍 ∈ SAlg