prsal

Description: The pair of the empty set and the whole base is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Assertion	prsal	$⊢ X \in V \to \{\emptyset, X\} \in SAlg$

Proof

Step	Hyp	Ref	Expression
1		0ex	$⊢ \emptyset \in V$
2	1	prid1	$⊢ \emptyset \in \{\emptyset, X\}$
3	2	a1i	$⊢ X \in V \to \emptyset \in \{\emptyset, X\}$
4		uniprg	$⊢ (\emptyset \in V \land X \in V) \to ⋃ \{\emptyset, X\} = \emptyset \cup X$
5	1 4	mpan	$⊢ X \in V \to ⋃ \{\emptyset, X\} = \emptyset \cup X$
6		0un	$⊢ \emptyset \cup X = X$
7	5 6	eqtrdi	$⊢ X \in V \to ⋃ \{\emptyset, X\} = X$
8	7	difeq1d	$⊢ X \in V \to ⋃ \{\emptyset, X\} ∖ y = X ∖ y$
9	8	adantr	$⊢ (X \in V \land y \in \{\emptyset, X\}) \to ⋃ \{\emptyset, X\} ∖ y = X ∖ y$
10		difeq2	$⊢ y = \emptyset \to X ∖ y = X ∖ \emptyset$
11	10	adantl	$⊢ (X \in V \land y = \emptyset) \to X ∖ y = X ∖ \emptyset$
12		dif0	$⊢ X ∖ \emptyset = X$
13	11 12	eqtrdi	$⊢ (X \in V \land y = \emptyset) \to X ∖ y = X$
14		prid2g	$⊢ X \in V \to X \in \{\emptyset, X\}$
15	14	adantr	$⊢ (X \in V \land y = \emptyset) \to X \in \{\emptyset, X\}$
16	13 15	eqeltrd	$⊢ (X \in V \land y = \emptyset) \to X ∖ y \in \{\emptyset, X\}$
17	16	adantlr	$⊢ ((X \in V \land y \in \{\emptyset, X\}) \land y = \emptyset) \to X ∖ y \in \{\emptyset, X\}$
18		neqne	$⊢ \neg y = \emptyset \to y \neq \emptyset$
19		elprn1	$⊢ (y \in \{\emptyset, X\} \land y \neq \emptyset) \to y = X$
20	18 19	sylan2	$⊢ (y \in \{\emptyset, X\} \land \neg y = \emptyset) \to y = X$
21	20	adantll	$⊢ ((X \in V \land y \in \{\emptyset, X\}) \land \neg y = \emptyset) \to y = X$
22		difeq2	$⊢ y = X \to X ∖ y = X ∖ X$
23		difid	$⊢ X ∖ X = \emptyset$
24	22 23	eqtrdi	$⊢ y = X \to X ∖ y = \emptyset$
25	2	a1i	$⊢ y = X \to \emptyset \in \{\emptyset, X\}$
26	24 25	eqeltrd	$⊢ y = X \to X ∖ y \in \{\emptyset, X\}$
27	21 26	syl	$⊢ ((X \in V \land y \in \{\emptyset, X\}) \land \neg y = \emptyset) \to X ∖ y \in \{\emptyset, X\}$
28	17 27	pm2.61dan	$⊢ (X \in V \land y \in \{\emptyset, X\}) \to X ∖ y \in \{\emptyset, X\}$
29	9 28	eqeltrd	$⊢ (X \in V \land y \in \{\emptyset, X\}) \to ⋃ \{\emptyset, X\} ∖ y \in \{\emptyset, X\}$
30	29	ralrimiva	$⊢ X \in V \to \forall y \in \{\emptyset, X\} ⋃ \{\emptyset, X\} ∖ y \in \{\emptyset, X\}$
31		elpwi	$⊢ y \in 𝒫 \{\emptyset, X\} \to y \subseteq \{\emptyset, X\}$
32	31	unissd	$⊢ y \in 𝒫 \{\emptyset, X\} \to ⋃ y \subseteq ⋃ \{\emptyset, X\}$
33	32	adantl	$⊢ (X \in V \land y \in 𝒫 \{\emptyset, X\}) \to ⋃ y \subseteq ⋃ \{\emptyset, X\}$
34	7	adantr	$⊢ (X \in V \land y \in 𝒫 \{\emptyset, X\}) \to ⋃ \{\emptyset, X\} = X$
35	33 34	sseqtrd	$⊢ (X \in V \land y \in 𝒫 \{\emptyset, X\}) \to ⋃ y \subseteq X$
36	35	adantr	$⊢ ((X \in V \land y \in 𝒫 \{\emptyset, X\}) \land X \in y) \to ⋃ y \subseteq X$
37		elssuni	$⊢ X \in y \to X \subseteq ⋃ y$
38	37	adantl	$⊢ ((X \in V \land y \in 𝒫 \{\emptyset, X\}) \land X \in y) \to X \subseteq ⋃ y$
39	36 38	eqssd	$⊢ ((X \in V \land y \in 𝒫 \{\emptyset, X\}) \land X \in y) \to ⋃ y = X$
40	14	ad2antrr	$⊢ ((X \in V \land y \in 𝒫 \{\emptyset, X\}) \land X \in y) \to X \in \{\emptyset, X\}$
41	39 40	eqeltrd	$⊢ ((X \in V \land y \in 𝒫 \{\emptyset, X\}) \land X \in y) \to ⋃ y \in \{\emptyset, X\}$
42		id	$⊢ y \in 𝒫 \{\emptyset, X\} \to y \in 𝒫 \{\emptyset, X\}$
43		pwpr	$⊢ 𝒫 \{\emptyset, X\} = \{\emptyset, \{\emptyset\}\} \cup \{\{X\}, \{\emptyset, X\}\}$
44	42 43	eleqtrdi	$⊢ y \in 𝒫 \{\emptyset, X\} \to y \in (\{\emptyset, \{\emptyset\}\} \cup \{\{X\}, \{\emptyset, X\}\})$
45	44	adantr	$⊢ (y \in 𝒫 \{\emptyset, X\} \land \neg X \in y) \to y \in (\{\emptyset, \{\emptyset\}\} \cup \{\{X\}, \{\emptyset, X\}\})$
46	45	adantll	$⊢ ((X \in V \land y \in 𝒫 \{\emptyset, X\}) \land \neg X \in y) \to y \in (\{\emptyset, \{\emptyset\}\} \cup \{\{X\}, \{\emptyset, X\}\})$
47		snidg	$⊢ X \in V \to X \in \{X\}$
48	47	adantr	$⊢ (X \in V \land y = \{X\}) \to X \in \{X\}$
49		id	$⊢ y = \{X\} \to y = \{X\}$
50	49	eqcomd	$⊢ y = \{X\} \to \{X\} = y$
51	50	adantl	$⊢ (X \in V \land y = \{X\}) \to \{X\} = y$
52	48 51	eleqtrd	$⊢ (X \in V \land y = \{X\}) \to X \in y$
53	52	adantlr	$⊢ ((X \in V \land y \in \{\{X\}, \{\emptyset, X\}\}) \land y = \{X\}) \to X \in y$
54		id	$⊢ X \in V \to X \in V$
55	54	ad2antrr	$⊢ ((X \in V \land y \in \{\{X\}, \{\emptyset, X\}\}) \land \neg y = \{X\}) \to X \in V$
56		neqne	$⊢ \neg y = \{X\} \to y \neq \{X\}$
57		elprn1	$⊢ (y \in \{\{X\}, \{\emptyset, X\}\} \land y \neq \{X\}) \to y = \{\emptyset, X\}$
58	56 57	sylan2	$⊢ (y \in \{\{X\}, \{\emptyset, X\}\} \land \neg y = \{X\}) \to y = \{\emptyset, X\}$
59	58	adantll	$⊢ ((X \in V \land y \in \{\{X\}, \{\emptyset, X\}\}) \land \neg y = \{X\}) \to y = \{\emptyset, X\}$
60	14	adantr	$⊢ (X \in V \land y = \{\emptyset, X\}) \to X \in \{\emptyset, X\}$
61		id	$⊢ y = \{\emptyset, X\} \to y = \{\emptyset, X\}$
62	61	eqcomd	$⊢ y = \{\emptyset, X\} \to \{\emptyset, X\} = y$
63	62	adantl	$⊢ (X \in V \land y = \{\emptyset, X\}) \to \{\emptyset, X\} = y$
64	60 63	eleqtrd	$⊢ (X \in V \land y = \{\emptyset, X\}) \to X \in y$
65	55 59 64	syl2anc	$⊢ ((X \in V \land y \in \{\{X\}, \{\emptyset, X\}\}) \land \neg y = \{X\}) \to X \in y$
66	53 65	pm2.61dan	$⊢ (X \in V \land y \in \{\{X\}, \{\emptyset, X\}\}) \to X \in y$
67	66	stoic1a	$⊢ (X \in V \land \neg X \in y) \to \neg y \in \{\{X\}, \{\emptyset, X\}\}$
68	67	adantlr	$⊢ ((X \in V \land y \in 𝒫 \{\emptyset, X\}) \land \neg X \in y) \to \neg y \in \{\{X\}, \{\emptyset, X\}\}$
69		elunnel2	$⊢ (y \in (\{\emptyset, \{\emptyset\}\} \cup \{\{X\}, \{\emptyset, X\}\}) \land \neg y \in \{\{X\}, \{\emptyset, X\}\}) \to y \in \{\emptyset, \{\emptyset\}\}$
70	46 68 69	syl2anc	$⊢ ((X \in V \land y \in 𝒫 \{\emptyset, X\}) \land \neg X \in y) \to y \in \{\emptyset, \{\emptyset\}\}$
71		unieq	$⊢ y = \emptyset \to ⋃ y = ⋃ \emptyset$
72		uni0	$⊢ ⋃ \emptyset = \emptyset$
73	71 72	eqtrdi	$⊢ y = \emptyset \to ⋃ y = \emptyset$
74	73	adantl	$⊢ (y \in \{\emptyset, \{\emptyset\}\} \land y = \emptyset) \to ⋃ y = \emptyset$
75		elprn1	$⊢ (y \in \{\emptyset, \{\emptyset\}\} \land y \neq \emptyset) \to y = \{\emptyset\}$
76	18 75	sylan2	$⊢ (y \in \{\emptyset, \{\emptyset\}\} \land \neg y = \emptyset) \to y = \{\emptyset\}$
77		unieq	$⊢ y = \{\emptyset\} \to ⋃ y = ⋃ \{\emptyset\}$
78		unisn0	$⊢ ⋃ \{\emptyset\} = \emptyset$
79	77 78	eqtrdi	$⊢ y = \{\emptyset\} \to ⋃ y = \emptyset$
80	76 79	syl	$⊢ (y \in \{\emptyset, \{\emptyset\}\} \land \neg y = \emptyset) \to ⋃ y = \emptyset$
81	74 80	pm2.61dan	$⊢ y \in \{\emptyset, \{\emptyset\}\} \to ⋃ y = \emptyset$
82	70 81	syl	$⊢ ((X \in V \land y \in 𝒫 \{\emptyset, X\}) \land \neg X \in y) \to ⋃ y = \emptyset$
83	2	a1i	$⊢ ((X \in V \land y \in 𝒫 \{\emptyset, X\}) \land \neg X \in y) \to \emptyset \in \{\emptyset, X\}$
84	82 83	eqeltrd	$⊢ ((X \in V \land y \in 𝒫 \{\emptyset, X\}) \land \neg X \in y) \to ⋃ y \in \{\emptyset, X\}$
85	41 84	pm2.61dan	$⊢ (X \in V \land y \in 𝒫 \{\emptyset, X\}) \to ⋃ y \in \{\emptyset, X\}$
86	85	a1d	$⊢ (X \in V \land y \in 𝒫 \{\emptyset, X\}) \to (y ≼ ω \to ⋃ y \in \{\emptyset, X\})$
87	86	ralrimiva	$⊢ X \in V \to \forall y \in 𝒫 \{\emptyset, X\} (y ≼ ω \to ⋃ y \in \{\emptyset, X\})$
88		prex	$⊢ \{\emptyset, X\} \in V$
89		issal	$⊢ \{\emptyset, X\} \in V \to (\{\emptyset, X\} \in SAlg \leftrightarrow (\emptyset \in \{\emptyset, X\} \land \forall y \in \{\emptyset, X\} ⋃ \{\emptyset, X\} ∖ y \in \{\emptyset, X\} \land \forall y \in 𝒫 \{\emptyset, X\} (y ≼ ω \to ⋃ y \in \{\emptyset, X\})))$
90	88 89	mp1i	$⊢ X \in V \to (\{\emptyset, X\} \in SAlg \leftrightarrow (\emptyset \in \{\emptyset, X\} \land \forall y \in \{\emptyset, X\} ⋃ \{\emptyset, X\} ∖ y \in \{\emptyset, X\} \land \forall y \in 𝒫 \{\emptyset, X\} (y ≼ ω \to ⋃ y \in \{\emptyset, X\})))$
91	3 30 87 90	mpbir3and	$⊢ X \in V \to \{\emptyset, X\} \in SAlg$

Metamath Proof Explorer

Theorem prsal

Proof