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	$⊢ A = [0, 2]$
	salgencntex.s	$⊢ S = \{x \in 𝒫 A \| (x ≼ ω \lor (A ∖ x) ≼ ω)\}$
	salgencntex.b	$⊢ B = [0, 1]$
	salgencntex.t	$⊢ T = 𝒫 B$
	salgencntex.c	$⊢ C = S \cap T$
	salgencntex.z	$⊢ Z = ⋂ \{s \in SAlg \| C \subseteq s\}$
Assertion	salgencntex	$⊢ \neg Z \in SAlg$

Proof

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

Metamath Proof Explorer

Theorem salgencntex

Proof