salexct3

Description: An example of a sigma-algebra that's not closed under uncountable union. (Contributed by Glauco Siliprandi, 3-Jan-2021)

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

Proof

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

Metamath Proof Explorer

Theorem salexct3

Proof