salgensscntex

Description: This counterexample shows that the sigma-algebra generated by a set is not the smallest sigma-algebra containing the set, if we consider also sigma-algebras with a larger base set. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypotheses	salgensscntex.a	$⊢ A = [0, 2]$
	salgensscntex.s	$⊢ S = \{x \in 𝒫 A \| (x ≼ ω \lor (A ∖ x) ≼ ω)\}$
	salgensscntex.x	$⊢ X = ran (y \in [0, 1] ⟼ \{y\})$
	salgensscntex.g	$⊢ G = SalGen (X)$
Assertion	salgensscntex	$⊢ (X \subseteq S \land S \in SAlg \land \neg G \subseteq S)$

Proof

Step	Hyp	Ref	Expression
1		salgensscntex.a	$⊢ A = [0, 2]$
2		salgensscntex.s	$⊢ S = \{x \in 𝒫 A \| (x ≼ ω \lor (A ∖ x) ≼ ω)\}$
3		salgensscntex.x	$⊢ X = ran (y \in [0, 1] ⟼ \{y\})$
4		salgensscntex.g	$⊢ G = SalGen (X)$
5		0re	$⊢ 0 \in ℝ$
6		2re	$⊢ 2 \in ℝ$
7	5 6	pm3.2i	$⊢ (0 \in ℝ \land 2 \in ℝ)$
8	5	leidi	$⊢ 0 \leq 0$
9		1le2	$⊢ 1 \leq 2$
10	8 9	pm3.2i	$⊢ (0 \leq 0 \land 1 \leq 2)$
11		iccss	$⊢ ((0 \in ℝ \land 2 \in ℝ) \land (0 \leq 0 \land 1 \leq 2)) \to [0, 1] \subseteq [0, 2]$
12	7 10 11	mp2an	$⊢ [0, 1] \subseteq [0, 2]$
13		id	$⊢ y \in [0, 1] \to y \in [0, 1]$
14	12 13	sselid	$⊢ y \in [0, 1] \to y \in [0, 2]$
15	14 1	eleqtrrdi	$⊢ y \in [0, 1] \to y \in A$
16		snelpwi	$⊢ y \in A \to \{y\} \in 𝒫 A$
17	15 16	syl	$⊢ y \in [0, 1] \to \{y\} \in 𝒫 A$
18		snfi	$⊢ \{y\} \in Fin$
19		fict	$⊢ \{y\} \in Fin \to \{y\} ≼ ω$
20	18 19	ax-mp	$⊢ \{y\} ≼ ω$
21		orc	$⊢ \{y\} ≼ ω \to (\{y\} ≼ ω \lor (A ∖ \{y\}) ≼ ω)$
22	20 21	ax-mp	$⊢ (\{y\} ≼ ω \lor (A ∖ \{y\}) ≼ ω)$
23	22	a1i	$⊢ y \in [0, 1] \to (\{y\} ≼ ω \lor (A ∖ \{y\}) ≼ ω)$
24	17 23	jca	$⊢ y \in [0, 1] \to (\{y\} \in 𝒫 A \land (\{y\} ≼ ω \lor (A ∖ \{y\}) ≼ ω))$
25		breq1	$⊢ x = \{y\} \to (x ≼ ω \leftrightarrow \{y\} ≼ ω)$
26		difeq2	$⊢ x = \{y\} \to A ∖ x = A ∖ \{y\}$
27	26	breq1d	$⊢ x = \{y\} \to ((A ∖ x) ≼ ω \leftrightarrow (A ∖ \{y\}) ≼ ω)$
28	25 27	orbi12d	$⊢ x = \{y\} \to ((x ≼ ω \lor (A ∖ x) ≼ ω) \leftrightarrow (\{y\} ≼ ω \lor (A ∖ \{y\}) ≼ ω))$
29	28 2	elrab2	$⊢ \{y\} \in S \leftrightarrow (\{y\} \in 𝒫 A \land (\{y\} ≼ ω \lor (A ∖ \{y\}) ≼ ω))$
30	24 29	sylibr	$⊢ y \in [0, 1] \to \{y\} \in S$
31	30	rgen	$⊢ \forall y \in [0, 1] \{y\} \in S$
32		eqid	$⊢ (y \in [0, 1] ⟼ \{y\}) = (y \in [0, 1] ⟼ \{y\})$
33	32	rnmptss	$⊢ \forall y \in [0, 1] \{y\} \in S \to ran (y \in [0, 1] ⟼ \{y\}) \subseteq S$
34	31 33	ax-mp	$⊢ ran (y \in [0, 1] ⟼ \{y\}) \subseteq S$
35	3 34	eqsstri	$⊢ X \subseteq S$
36		ovex	$⊢ [0, 2] \in V$
37	1 36	eqeltri	$⊢ A \in V$
38	37	a1i	$⊢ ⊤ \to A \in V$
39	38 2	salexct	$⊢ ⊤ \to S \in SAlg$
40	39	mptru	$⊢ S \in SAlg$
41		ovex	$⊢ [0, 1] \in V$
42	41	mptex	$⊢ (y \in [0, 1] ⟼ \{y\}) \in V$
43	42	rnex	$⊢ ran (y \in [0, 1] ⟼ \{y\}) \in V$
44	3 43	eqeltri	$⊢ X \in V$
45	44	a1i	$⊢ ⊤ \to X \in V$
46	3	unieqi	$⊢ ⋃ X = ⋃ ran (y \in [0, 1] ⟼ \{y\})$
47		snex	$⊢ \{y\} \in V$
48	47	rgenw	$⊢ \forall y \in [0, 1] \{y\} \in V$
49		dfiun3g	$⊢ \forall y \in [0, 1] \{y\} \in V \to ⋃_{y \in [0, 1]} \{y\} = ⋃ ran (y \in [0, 1] ⟼ \{y\})$
50	48 49	ax-mp	$⊢ ⋃_{y \in [0, 1]} \{y\} = ⋃ ran (y \in [0, 1] ⟼ \{y\})$
51	50	eqcomi	$⊢ ⋃ ran (y \in [0, 1] ⟼ \{y\}) = ⋃_{y \in [0, 1]} \{y\}$
52		iunid	$⊢ ⋃_{y \in [0, 1]} \{y\} = [0, 1]$
53	46 51 52	3eqtrri	$⊢ [0, 1] = ⋃ X$
54	45 4 53	unisalgen	$⊢ ⊤ \to [0, 1] \in G$
55	54	mptru	$⊢ [0, 1] \in G$
56		eqid	$⊢ [0, 1] = [0, 1]$
57	1 2 56	salexct2	$⊢ \neg [0, 1] \in S$
58		nelss	$⊢ ([0, 1] \in G \land \neg [0, 1] \in S) \to \neg G \subseteq S$
59	55 57 58	mp2an	$⊢ \neg G \subseteq S$
60	35 40 59	3pm3.2i	$⊢ (X \subseteq S \land S \in SAlg \land \neg G \subseteq S)$

Metamath Proof Explorer

Theorem salgensscntex

Proof