Theorem 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	⊢ 𝐴 = ( 0 [,] 2 )
	salexct2.2	⊢ 𝑆 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) }
	salexct2.3	⊢ 𝐵 = ( 0 [,] 1 )
Assertion	salexct2	⊢ ¬ 𝐵 ∈ 𝑆

Proof

Step	Hyp	Ref	Expression
1		salexct2.1	⊢ 𝐴 = ( 0 [,] 2 )
2		salexct2.2	⊢ 𝑆 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) }
3		salexct2.3	⊢ 𝐵 = ( 0 [,] 1 )
4		0xr	⊢ 0 ∈ ℝ*
5	4	a1i	⊢ ( ⊤ → 0 ∈ ℝ* )
6		1xr	⊢ 1 ∈ ℝ*
7	6	a1i	⊢ ( ⊤ → 1 ∈ ℝ* )
8		0lt1	⊢ 0 < 1
9	8	a1i	⊢ ( ⊤ → 0 < 1 )
10	5 7 9 3	iccnct	⊢ ( ⊤ → ¬ 𝐵 ≼ ω )
11	10	mptru	⊢ ¬ 𝐵 ≼ ω
12		2re	⊢ 2 ∈ ℝ
13	12	rexri	⊢ 2 ∈ ℝ*
14	13	a1i	⊢ ( ⊤ → 2 ∈ ℝ* )
15		1lt2	⊢ 1 < 2
16	15	a1i	⊢ ( ⊤ → 1 < 2 )
17		eqid	⊢ ( 1 (,] 2 ) = ( 1 (,] 2 )
18	7 14 16 17	iocnct	⊢ ( ⊤ → ¬ ( 1 (,] 2 ) ≼ ω )
19	18	mptru	⊢ ¬ ( 1 (,] 2 ) ≼ ω
20	1 3	difeq12i	⊢ ( 𝐴 ∖ 𝐵 ) = ( ( 0 [,] 2 ) ∖ ( 0 [,] 1 ) )
21	5 7 9	xrltled	⊢ ( ⊤ → 0 ≤ 1 )
22	5 7 14 21	iccdificc	⊢ ( ⊤ → ( ( 0 [,] 2 ) ∖ ( 0 [,] 1 ) ) = ( 1 (,] 2 ) )
23	22	mptru	⊢ ( ( 0 [,] 2 ) ∖ ( 0 [,] 1 ) ) = ( 1 (,] 2 )
24	20 23	eqtri	⊢ ( 𝐴 ∖ 𝐵 ) = ( 1 (,] 2 )
25	24	breq1i	⊢ ( ( 𝐴 ∖ 𝐵 ) ≼ ω ↔ ( 1 (,] 2 ) ≼ ω )
26	19 25	mtbir	⊢ ¬ ( 𝐴 ∖ 𝐵 ) ≼ ω
27	11 26	pm3.2i	⊢ ( ¬ 𝐵 ≼ ω ∧ ¬ ( 𝐴 ∖ 𝐵 ) ≼ ω )
28		ioran	⊢ ( ¬ ( 𝐵 ≼ ω ∨ ( 𝐴 ∖ 𝐵 ) ≼ ω ) ↔ ( ¬ 𝐵 ≼ ω ∧ ¬ ( 𝐴 ∖ 𝐵 ) ≼ ω ) )
29	27 28	mpbir	⊢ ¬ ( 𝐵 ≼ ω ∨ ( 𝐴 ∖ 𝐵 ) ≼ ω )
30	29	intnan	⊢ ¬ ( 𝐵 ∈ 𝒫 𝐴 ∧ ( 𝐵 ≼ ω ∨ ( 𝐴 ∖ 𝐵 ) ≼ ω ) )
31		breq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 ≼ ω ↔ 𝐵 ≼ ω ) )
32		difeq2	⊢ ( 𝑥 = 𝐵 → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ 𝐵 ) )
33	32	breq1d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ∖ 𝑥 ) ≼ ω ↔ ( 𝐴 ∖ 𝐵 ) ≼ ω ) )
34	31 33	orbi12d	⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) ↔ ( 𝐵 ≼ ω ∨ ( 𝐴 ∖ 𝐵 ) ≼ ω ) ) )
35	34 2	elrab2	⊢ ( 𝐵 ∈ 𝑆 ↔ ( 𝐵 ∈ 𝒫 𝐴 ∧ ( 𝐵 ≼ ω ∨ ( 𝐴 ∖ 𝐵 ) ≼ ω ) ) )
36	30 35	mtbir	⊢ ¬ 𝐵 ∈ 𝑆