salexct2

Description: An example of a subset that does not belong to a nontrivial sigma-algebra, see salexct . (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypotheses	salexct2.1	$⊢ A = [0, 2]$
	salexct2.2	$⊢ S = \{x \in 𝒫 A \| (x ≼ ω \lor (A ∖ x) ≼ ω)\}$
	salexct2.3	$⊢ B = [0, 1]$
Assertion	salexct2	$⊢ \neg B \in S$

Proof

Step	Hyp	Ref	Expression
1		salexct2.1	$⊢ A = [0, 2]$
2		salexct2.2	$⊢ S = \{x \in 𝒫 A \| (x ≼ ω \lor (A ∖ x) ≼ ω)\}$
3		salexct2.3	$⊢ B = [0, 1]$
4		0xr	$⊢ 0 \in ℝ^{*}$
5	4	a1i	$⊢ ⊤ \to 0 \in ℝ^{*}$
6		1xr	$⊢ 1 \in ℝ^{*}$
7	6	a1i	$⊢ ⊤ \to 1 \in ℝ^{*}$
8		0lt1	$⊢ 0 < 1$
9	8	a1i	$⊢ ⊤ \to 0 < 1$
10	5 7 9 3	iccnct	$⊢ ⊤ \to \neg B ≼ ω$
11	10	mptru	$⊢ \neg B ≼ ω$
12		2re	$⊢ 2 \in ℝ$
13	12	rexri	$⊢ 2 \in ℝ^{*}$
14	13	a1i	$⊢ ⊤ \to 2 \in ℝ^{*}$
15		1lt2	$⊢ 1 < 2$
16	15	a1i	$⊢ ⊤ \to 1 < 2$
17		eqid	$⊢ (1, 2] = (1, 2]$
18	7 14 16 17	iocnct	$⊢ ⊤ \to \neg (1, 2] ≼ ω$
19	18	mptru	$⊢ \neg (1, 2] ≼ ω$
20	1 3	difeq12i	$⊢ A ∖ B = [0, 2] ∖ [0, 1]$
21	5 7 9	xrltled	$⊢ ⊤ \to 0 \leq 1$
22	5 7 14 21	iccdificc	$⊢ ⊤ \to [0, 2] ∖ [0, 1] = (1, 2]$
23	22	mptru	$⊢ [0, 2] ∖ [0, 1] = (1, 2]$
24	20 23	eqtri	$⊢ A ∖ B = (1, 2]$
25	24	breq1i	$⊢ (A ∖ B) ≼ ω \leftrightarrow (1, 2] ≼ ω$
26	19 25	mtbir	$⊢ \neg (A ∖ B) ≼ ω$
27	11 26	pm3.2i	$⊢ (\neg B ≼ ω \land \neg (A ∖ B) ≼ ω)$
28		ioran	$⊢ \neg (B ≼ ω \lor (A ∖ B) ≼ ω) \leftrightarrow (\neg B ≼ ω \land \neg (A ∖ B) ≼ ω)$
29	27 28	mpbir	$⊢ \neg (B ≼ ω \lor (A ∖ B) ≼ ω)$
30	29	intnan	$⊢ \neg (B \in 𝒫 A \land (B ≼ ω \lor (A ∖ B) ≼ ω))$
31		breq1	$⊢ x = B \to (x ≼ ω \leftrightarrow B ≼ ω)$
32		difeq2	$⊢ x = B \to A ∖ x = A ∖ B$
33	32	breq1d	$⊢ x = B \to ((A ∖ x) ≼ ω \leftrightarrow (A ∖ B) ≼ ω)$
34	31 33	orbi12d	$⊢ x = B \to ((x ≼ ω \lor (A ∖ x) ≼ ω) \leftrightarrow (B ≼ ω \lor (A ∖ B) ≼ ω))$
35	34 2	elrab2	$⊢ B \in S \leftrightarrow (B \in 𝒫 A \land (B ≼ ω \lor (A ∖ B) ≼ ω))$
36	30 35	mtbir	$⊢ \neg B \in S$

Metamath Proof Explorer

Theorem salexct2

Proof