salexct

Description: An example of nontrivial sigma-algebra: the collection of all subsets which either are countable or have countable complement. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypotheses	salexct.a	$⊢ φ \to A \in V$
	salexct.b	$⊢ S = \{x \in 𝒫 A \| (x ≼ ω \lor (A ∖ x) ≼ ω)\}$
Assertion	salexct	$⊢ φ \to S \in SAlg$

Proof

Step	Hyp	Ref	Expression
1		salexct.a	$⊢ φ \to A \in V$
2		salexct.b	$⊢ S = \{x \in 𝒫 A \| (x ≼ ω \lor (A ∖ x) ≼ ω)\}$
3	1	pwexd	$⊢ φ \to 𝒫 A \in V$
4		rabexg	$⊢ 𝒫 A \in V \to \{x \in 𝒫 A \| (x ≼ ω \lor (A ∖ x) ≼ ω)\} \in V$
5	3 4	syl	$⊢ φ \to \{x \in 𝒫 A \| (x ≼ ω \lor (A ∖ x) ≼ ω)\} \in V$
6	2 5	eqeltrid	$⊢ φ \to S \in V$
7		0elpw	$⊢ \emptyset \in 𝒫 A$
8	7	a1i	$⊢ φ \to \emptyset \in 𝒫 A$
9		0fin	$⊢ \emptyset \in Fin$
10		fict	$⊢ \emptyset \in Fin \to \emptyset ≼ ω$
11	9 10	ax-mp	$⊢ \emptyset ≼ ω$
12	11	orci	$⊢ (\emptyset ≼ ω \lor (A ∖ \emptyset) ≼ ω)$
13	12	a1i	$⊢ φ \to (\emptyset ≼ ω \lor (A ∖ \emptyset) ≼ ω)$
14	8 13	jca	$⊢ φ \to (\emptyset \in 𝒫 A \land (\emptyset ≼ ω \lor (A ∖ \emptyset) ≼ ω))$
15		breq1	$⊢ x = \emptyset \to (x ≼ ω \leftrightarrow \emptyset ≼ ω)$
16		difeq2	$⊢ x = \emptyset \to A ∖ x = A ∖ \emptyset$
17	16	breq1d	$⊢ x = \emptyset \to ((A ∖ x) ≼ ω \leftrightarrow (A ∖ \emptyset) ≼ ω)$
18	15 17	orbi12d	$⊢ x = \emptyset \to ((x ≼ ω \lor (A ∖ x) ≼ ω) \leftrightarrow (\emptyset ≼ ω \lor (A ∖ \emptyset) ≼ ω))$
19	18 2	elrab2	$⊢ \emptyset \in S \leftrightarrow (\emptyset \in 𝒫 A \land (\emptyset ≼ ω \lor (A ∖ \emptyset) ≼ ω))$
20	14 19	sylibr	$⊢ φ \to \emptyset \in S$
21		snidg	$⊢ y \in A \to y \in \{y\}$
22		snelpwi	$⊢ y \in A \to \{y\} \in 𝒫 A$
23		snfi	$⊢ \{y\} \in Fin$
24		fict	$⊢ \{y\} \in Fin \to \{y\} ≼ ω$
25	23 24	ax-mp	$⊢ \{y\} ≼ ω$
26	25	orci	$⊢ (\{y\} ≼ ω \lor (A ∖ \{y\}) ≼ ω)$
27	26	a1i	$⊢ y \in A \to (\{y\} ≼ ω \lor (A ∖ \{y\}) ≼ ω)$
28	22 27	jca	$⊢ y \in A \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 A \to \{y\} \in S$
35		elunii	$⊢ (y \in \{y\} \land \{y\} \in S) \to y \in ⋃ S$
36	21 34 35	syl2anc	$⊢ y \in A \to y \in ⋃ S$
37	36	rgen	$⊢ \forall y \in A y \in ⋃ S$
38		dfss3	$⊢ A \subseteq ⋃ S \leftrightarrow \forall y \in A y \in ⋃ S$
39	37 38	mpbir	$⊢ A \subseteq ⋃ S$
40		ssrab2	$⊢ \{x \in 𝒫 A \| (x ≼ ω \lor (A ∖ x) ≼ ω)\} \subseteq 𝒫 A$
41	2 40	eqsstri	$⊢ S \subseteq 𝒫 A$
42	41	unissi	$⊢ ⋃ S \subseteq ⋃ 𝒫 A$
43		unipw	$⊢ ⋃ 𝒫 A = A$
44	42 43	sseqtri	$⊢ ⋃ S \subseteq A$
45	39 44	eqssi	$⊢ A = ⋃ S$
46		difssd	$⊢ φ \to A ∖ x \subseteq A$
47	1 46	ssexd	$⊢ φ \to A ∖ x \in V$
48		elpwg	$⊢ A ∖ x \in V \to (A ∖ x \in 𝒫 A \leftrightarrow A ∖ x \subseteq A)$
49	47 48	syl	$⊢ φ \to (A ∖ x \in 𝒫 A \leftrightarrow A ∖ x \subseteq A)$
50	46 49	mpbird	$⊢ φ \to A ∖ x \in 𝒫 A$
51	50	ad2antrr	$⊢ ((φ \land x \in S) \land x ≼ ω) \to A ∖ x \in 𝒫 A$
52	41	sseli	$⊢ x \in S \to x \in 𝒫 A$
53		elpwi	$⊢ x \in 𝒫 A \to x \subseteq A$
54	52 53	syl	$⊢ x \in S \to x \subseteq A$
55		dfss4	$⊢ x \subseteq A \leftrightarrow A ∖ (A ∖ x) = x$
56	54 55	sylib	$⊢ x \in S \to A ∖ (A ∖ x) = x$
57	56	ad2antlr	$⊢ ((φ \land x \in S) \land x ≼ ω) \to A ∖ (A ∖ x) = x$
58		simpr	$⊢ ((φ \land x \in S) \land x ≼ ω) \to x ≼ ω$
59	57 58	eqbrtrd	$⊢ ((φ \land x \in S) \land x ≼ ω) \to (A ∖ (A ∖ x)) ≼ ω$
60		olc	$⊢ (A ∖ (A ∖ x)) ≼ ω \to ((A ∖ x) ≼ ω \lor (A ∖ (A ∖ x)) ≼ ω)$
61	59 60	syl	$⊢ ((φ \land x \in S) \land x ≼ ω) \to ((A ∖ x) ≼ ω \lor (A ∖ (A ∖ x)) ≼ ω)$
62	51 61	jca	$⊢ ((φ \land x \in S) \land x ≼ ω) \to (A ∖ x \in 𝒫 A \land ((A ∖ x) ≼ ω \lor (A ∖ (A ∖ x)) ≼ ω))$
63		breq1	$⊢ y = A ∖ x \to (y ≼ ω \leftrightarrow (A ∖ x) ≼ ω)$
64		difeq2	$⊢ y = A ∖ x \to A ∖ y = A ∖ (A ∖ x)$
65	64	breq1d	$⊢ y = A ∖ x \to ((A ∖ y) ≼ ω \leftrightarrow (A ∖ (A ∖ x)) ≼ ω)$
66	63 65	orbi12d	$⊢ y = A ∖ x \to ((y ≼ ω \lor (A ∖ y) ≼ ω) \leftrightarrow ((A ∖ x) ≼ ω \lor (A ∖ (A ∖ x)) ≼ ω))$
67		breq1	$⊢ x = y \to (x ≼ ω \leftrightarrow y ≼ ω)$
68		difeq2	$⊢ x = y \to A ∖ x = A ∖ y$
69	68	breq1d	$⊢ x = y \to ((A ∖ x) ≼ ω \leftrightarrow (A ∖ y) ≼ ω)$
70	67 69	orbi12d	$⊢ x = y \to ((x ≼ ω \lor (A ∖ x) ≼ ω) \leftrightarrow (y ≼ ω \lor (A ∖ y) ≼ ω))$
71	70	cbvrabv	$⊢ \{x \in 𝒫 A \| (x ≼ ω \lor (A ∖ x) ≼ ω)\} = \{y \in 𝒫 A \| (y ≼ ω \lor (A ∖ y) ≼ ω)\}$
72	2 71	eqtri	$⊢ S = \{y \in 𝒫 A \| (y ≼ ω \lor (A ∖ y) ≼ ω)\}$
73	66 72	elrab2	$⊢ A ∖ x \in S \leftrightarrow (A ∖ x \in 𝒫 A \land ((A ∖ x) ≼ ω \lor (A ∖ (A ∖ x)) ≼ ω))$
74	62 73	sylibr	$⊢ ((φ \land x \in S) \land x ≼ ω) \to A ∖ x \in S$
75	50	ad2antrr	$⊢ ((φ \land x \in S) \land \neg x ≼ ω) \to A ∖ x \in 𝒫 A$
76	2	rabeq2i	$⊢ x \in S \leftrightarrow (x \in 𝒫 A \land (x ≼ ω \lor (A ∖ x) ≼ ω))$
77	76	biimpi	$⊢ x \in S \to (x \in 𝒫 A \land (x ≼ ω \lor (A ∖ x) ≼ ω))$
78	77	simprd	$⊢ x \in S \to (x ≼ ω \lor (A ∖ x) ≼ ω)$
79	78	adantl	$⊢ (φ \land x \in S) \to (x ≼ ω \lor (A ∖ x) ≼ ω)$
80	79	adantr	$⊢ ((φ \land x \in S) \land \neg x ≼ ω) \to (x ≼ ω \lor (A ∖ x) ≼ ω)$
81		simpr	$⊢ ((φ \land x \in S) \land \neg x ≼ ω) \to \neg x ≼ ω$
82		pm2.53	$⊢ (x ≼ ω \lor (A ∖ x) ≼ ω) \to (\neg x ≼ ω \to (A ∖ x) ≼ ω)$
83	80 81 82	sylc	$⊢ ((φ \land x \in S) \land \neg x ≼ ω) \to (A ∖ x) ≼ ω$
84		orc	$⊢ (A ∖ x) ≼ ω \to ((A ∖ x) ≼ ω \lor (A ∖ (A ∖ x)) ≼ ω)$
85	83 84	syl	$⊢ ((φ \land x \in S) \land \neg x ≼ ω) \to ((A ∖ x) ≼ ω \lor (A ∖ (A ∖ x)) ≼ ω)$
86	75 85	jca	$⊢ ((φ \land x \in S) \land \neg x ≼ ω) \to (A ∖ x \in 𝒫 A \land ((A ∖ x) ≼ ω \lor (A ∖ (A ∖ x)) ≼ ω))$
87	86 73	sylibr	$⊢ ((φ \land x \in S) \land \neg x ≼ ω) \to A ∖ x \in S$
88	74 87	pm2.61dan	$⊢ (φ \land x \in S) \to A ∖ x \in S$
89		elpwi	$⊢ x \in 𝒫 S \to x \subseteq S$
90	89	adantr	$⊢ (x \in 𝒫 S \land y \in x) \to x \subseteq S$
91		simpr	$⊢ (x \in 𝒫 S \land y \in x) \to y \in x$
92	90 91	sseldd	$⊢ (x \in 𝒫 S \land y \in x) \to y \in S$
93	41	sseli	$⊢ y \in S \to y \in 𝒫 A$
94		elpwi	$⊢ y \in 𝒫 A \to y \subseteq A$
95	93 94	syl	$⊢ y \in S \to y \subseteq A$
96	92 95	syl	$⊢ (x \in 𝒫 S \land y \in x) \to y \subseteq A$
97	96	ralrimiva	$⊢ x \in 𝒫 S \to \forall y \in x y \subseteq A$
98		unissb	$⊢ ⋃ x \subseteq A \leftrightarrow \forall y \in x y \subseteq A$
99	97 98	sylibr	$⊢ x \in 𝒫 S \to ⋃ x \subseteq A$
100		vuniex	$⊢ ⋃ x \in V$
101	100	elpw	$⊢ ⋃ x \in 𝒫 A \leftrightarrow ⋃ x \subseteq A$
102	99 101	sylibr	$⊢ x \in 𝒫 S \to ⋃ x \in 𝒫 A$
103	102	adantr	$⊢ (x \in 𝒫 S \land x ≼ ω) \to ⋃ x \in 𝒫 A$
104		id	$⊢ (x ≼ ω \land \forall y \in x y ≼ ω) \to (x ≼ ω \land \forall y \in x y ≼ ω)$
105	104	adantll	$⊢ ((x \in 𝒫 S \land x ≼ ω) \land \forall y \in x y ≼ ω) \to (x ≼ ω \land \forall y \in x y ≼ ω)$
106		unictb	$⊢ (x ≼ ω \land \forall y \in x y ≼ ω) \to ⋃ x ≼ ω$
107		orc	$⊢ ⋃ x ≼ ω \to (⋃ x ≼ ω \lor (A ∖ ⋃ x) ≼ ω)$
108	105 106 107	3syl	$⊢ ((x \in 𝒫 S \land x ≼ ω) \land \forall y \in x y ≼ ω) \to (⋃ x ≼ ω \lor (A ∖ ⋃ x) ≼ ω)$
109		rexnal	$⊢ \exists y \in x \neg y ≼ ω \leftrightarrow \neg \forall y \in x y ≼ ω$
110	109	bicomi	$⊢ \neg \forall y \in x y ≼ ω \leftrightarrow \exists y \in x \neg y ≼ ω$
111	110	biimpi	$⊢ \neg \forall y \in x y ≼ ω \to \exists y \in x \neg y ≼ ω$
112	111	adantl	$⊢ (x \in 𝒫 S \land \neg \forall y \in x y ≼ ω) \to \exists y \in x \neg y ≼ ω$
113		nfv	$⊢ Ⅎ y x \in 𝒫 S$
114		nfra1	$⊢ Ⅎ y \forall y \in x y ≼ ω$
115	114	nfn	$⊢ Ⅎ y \neg \forall y \in x y ≼ ω$
116	113 115	nfan	$⊢ Ⅎ y (x \in 𝒫 S \land \neg \forall y \in x y ≼ ω)$
117		nfv	$⊢ Ⅎ y (A ∖ ⋃ x) ≼ ω$
118		elssuni	$⊢ y \in x \to y \subseteq ⋃ x$
119	118	3ad2ant2	$⊢ (x \in 𝒫 S \land y \in x \land \neg y ≼ ω) \to y \subseteq ⋃ x$
120	119	sscond	$⊢ (x \in 𝒫 S \land y \in x \land \neg y ≼ ω) \to A ∖ ⋃ x \subseteq A ∖ y$
121	92	3adant3	$⊢ (x \in 𝒫 S \land y \in x \land \neg y ≼ ω) \to y \in S$
122		simp3	$⊢ (x \in 𝒫 S \land y \in x \land \neg y ≼ ω) \to \neg y ≼ ω$
123	72	rabeq2i	$⊢ y \in S \leftrightarrow (y \in 𝒫 A \land (y ≼ ω \lor (A ∖ y) ≼ ω))$
124	123	biimpi	$⊢ y \in S \to (y \in 𝒫 A \land (y ≼ ω \lor (A ∖ y) ≼ ω))$
125	124	simprd	$⊢ y \in S \to (y ≼ ω \lor (A ∖ y) ≼ ω)$
126	125	adantr	$⊢ (y \in S \land \neg y ≼ ω) \to (y ≼ ω \lor (A ∖ y) ≼ ω)$
127		simpr	$⊢ (y \in S \land \neg y ≼ ω) \to \neg y ≼ ω$
128		pm2.53	$⊢ (y ≼ ω \lor (A ∖ y) ≼ ω) \to (\neg y ≼ ω \to (A ∖ y) ≼ ω)$
129	126 127 128	sylc	$⊢ (y \in S \land \neg y ≼ ω) \to (A ∖ y) ≼ ω$
130	121 122 129	syl2anc	$⊢ (x \in 𝒫 S \land y \in x \land \neg y ≼ ω) \to (A ∖ y) ≼ ω$
131		ssct	$⊢ (A ∖ ⋃ x \subseteq A ∖ y \land (A ∖ y) ≼ ω) \to (A ∖ ⋃ x) ≼ ω$
132	120 130 131	syl2anc	$⊢ (x \in 𝒫 S \land y \in x \land \neg y ≼ ω) \to (A ∖ ⋃ x) ≼ ω$
133	132	3exp	$⊢ x \in 𝒫 S \to (y \in x \to (\neg y ≼ ω \to (A ∖ ⋃ x) ≼ ω))$
134	133	adantr	$⊢ (x \in 𝒫 S \land \neg \forall y \in x y ≼ ω) \to (y \in x \to (\neg y ≼ ω \to (A ∖ ⋃ x) ≼ ω))$
135	116 117 134	rexlimd	$⊢ (x \in 𝒫 S \land \neg \forall y \in x y ≼ ω) \to (\exists y \in x \neg y ≼ ω \to (A ∖ ⋃ x) ≼ ω)$
136	112 135	mpd	$⊢ (x \in 𝒫 S \land \neg \forall y \in x y ≼ ω) \to (A ∖ ⋃ x) ≼ ω$
137		olc	$⊢ (A ∖ ⋃ x) ≼ ω \to (⋃ x ≼ ω \lor (A ∖ ⋃ x) ≼ ω)$
138	136 137	syl	$⊢ (x \in 𝒫 S \land \neg \forall y \in x y ≼ ω) \to (⋃ x ≼ ω \lor (A ∖ ⋃ x) ≼ ω)$
139	138	adantlr	$⊢ ((x \in 𝒫 S \land x ≼ ω) \land \neg \forall y \in x y ≼ ω) \to (⋃ x ≼ ω \lor (A ∖ ⋃ x) ≼ ω)$
140	108 139	pm2.61dan	$⊢ (x \in 𝒫 S \land x ≼ ω) \to (⋃ x ≼ ω \lor (A ∖ ⋃ x) ≼ ω)$
141	103 140	jca	$⊢ (x \in 𝒫 S \land x ≼ ω) \to (⋃ x \in 𝒫 A \land (⋃ x ≼ ω \lor (A ∖ ⋃ x) ≼ ω))$
142		breq1	$⊢ y = ⋃ x \to (y ≼ ω \leftrightarrow ⋃ x ≼ ω)$
143		difeq2	$⊢ y = ⋃ x \to A ∖ y = A ∖ ⋃ x$
144	143	breq1d	$⊢ y = ⋃ x \to ((A ∖ y) ≼ ω \leftrightarrow (A ∖ ⋃ x) ≼ ω)$
145	142 144	orbi12d	$⊢ y = ⋃ x \to ((y ≼ ω \lor (A ∖ y) ≼ ω) \leftrightarrow (⋃ x ≼ ω \lor (A ∖ ⋃ x) ≼ ω))$
146	145 72	elrab2	$⊢ ⋃ x \in S \leftrightarrow (⋃ x \in 𝒫 A \land (⋃ x ≼ ω \lor (A ∖ ⋃ x) ≼ ω))$
147	141 146	sylibr	$⊢ (x \in 𝒫 S \land x ≼ ω) \to ⋃ x \in S$
148	147	3adant1	$⊢ (φ \land x \in 𝒫 S \land x ≼ ω) \to ⋃ x \in S$
149	6 20 45 88 148	issald	$⊢ φ \to S \in SAlg$

Metamath Proof Explorer

Theorem salexct

Proof