Theorem prsal 39214

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

Assertion

Ref	Expression
prsal	⊢ (𝑋 ∈ 𝑉 → {∅, 𝑋} ∈ SAlg)

Proof of Theorem prsal

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		0ex 4718	. . . . 5 ⊢ ∅ ∈ V
2	1	prid1 4241	. . . 4 ⊢ ∅ ∈ {∅, 𝑋}
3	2	a1i 11	. . 3 ⊢ (𝑋 ∈ 𝑉 → ∅ ∈ {∅, 𝑋})
4	1	a1i 11	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑉 → ∅ ∈ V)
5		id 22	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ 𝑉)
6		uniprg 4386	. . . . . . . . 9 ⊢ ((∅ ∈ V ∧ 𝑋 ∈ 𝑉) → ∪ {∅, 𝑋} = (∅ ∪ 𝑋))
7	4, 5, 6	syl2anc 691	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑉 → ∪ {∅, 𝑋} = (∅ ∪ 𝑋))
8		uncom 3719	. . . . . . . . . 10 ⊢ (∅ ∪ 𝑋) = (𝑋 ∪ ∅)
9		un0 3919	. . . . . . . . . 10 ⊢ (𝑋 ∪ ∅) = 𝑋
10	8, 9	eqtri 2632	. . . . . . . . 9 ⊢ (∅ ∪ 𝑋) = 𝑋
11	10	a1i 11	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑉 → (∅ ∪ 𝑋) = 𝑋)
12		eqidd 2611	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑉 → 𝑋 = 𝑋)
13	7, 11, 12	3eqtrd 2648	. . . . . . 7 ⊢ (𝑋 ∈ 𝑉 → ∪ {∅, 𝑋} = 𝑋)
14	13	difeq1d 3689	. . . . . 6 ⊢ (𝑋 ∈ 𝑉 → (∪ {∅, 𝑋} ∖ 𝑦) = (𝑋 ∖ 𝑦))
15	14	adantr 480	. . . . 5 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) → (∪ {∅, 𝑋} ∖ 𝑦) = (𝑋 ∖ 𝑦))
16		difeq2 3684	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → (𝑋 ∖ 𝑦) = (𝑋 ∖ ∅))
17	16	adantl 481	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = ∅) → (𝑋 ∖ 𝑦) = (𝑋 ∖ ∅))
18		dif0 3904	. . . . . . . . . 10 ⊢ (𝑋 ∖ ∅) = 𝑋
19	18	a1i 11	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = ∅) → (𝑋 ∖ ∅) = 𝑋)
20	17, 19	eqtrd 2644	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = ∅) → (𝑋 ∖ 𝑦) = 𝑋)
21		prid2g 4240	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {∅, 𝑋})
22	21	adantr 480	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = ∅) → 𝑋 ∈ {∅, 𝑋})
23	20, 22	eqeltrd 2688	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = ∅) → (𝑋 ∖ 𝑦) ∈ {∅, 𝑋})
24	23	adantlr 747	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) ∧ 𝑦 = ∅) → (𝑋 ∖ 𝑦) ∈ {∅, 𝑋})
25		simpll 786	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) ∧ ¬ 𝑦 = ∅) → 𝑋 ∈ 𝑉)
26		simpl 472	. . . . . . . . 9 ⊢ ((𝑦 ∈ {∅, 𝑋} ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ {∅, 𝑋})
27		neqne 2790	. . . . . . . . . 10 ⊢ (¬ 𝑦 = ∅ → 𝑦 ≠ ∅)
28	27	adantl 481	. . . . . . . . 9 ⊢ ((𝑦 ∈ {∅, 𝑋} ∧ ¬ 𝑦 = ∅) → 𝑦 ≠ ∅)
29		elprn1 38700	. . . . . . . . 9 ⊢ ((𝑦 ∈ {∅, 𝑋} ∧ 𝑦 ≠ ∅) → 𝑦 = 𝑋)
30	26, 28, 29	syl2anc 691	. . . . . . . 8 ⊢ ((𝑦 ∈ {∅, 𝑋} ∧ ¬ 𝑦 = ∅) → 𝑦 = 𝑋)
31	30	adantll 746	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) ∧ ¬ 𝑦 = ∅) → 𝑦 = 𝑋)
32		difeq2 3684	. . . . . . . . . 10 ⊢ (𝑦 = 𝑋 → (𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑋))
33		difid 3902	. . . . . . . . . . 11 ⊢ (𝑋 ∖ 𝑋) = ∅
34	33	a1i 11	. . . . . . . . . 10 ⊢ (𝑦 = 𝑋 → (𝑋 ∖ 𝑋) = ∅)
35	32, 34	eqtrd 2644	. . . . . . . . 9 ⊢ (𝑦 = 𝑋 → (𝑋 ∖ 𝑦) = ∅)
36	2	a1i 11	. . . . . . . . 9 ⊢ (𝑦 = 𝑋 → ∅ ∈ {∅, 𝑋})
37	35, 36	eqeltrd 2688	. . . . . . . 8 ⊢ (𝑦 = 𝑋 → (𝑋 ∖ 𝑦) ∈ {∅, 𝑋})
38	37	adantl 481	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = 𝑋) → (𝑋 ∖ 𝑦) ∈ {∅, 𝑋})
39	25, 31, 38	syl2anc 691	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) ∧ ¬ 𝑦 = ∅) → (𝑋 ∖ 𝑦) ∈ {∅, 𝑋})
40	24, 39	pm2.61dan 828	. . . . 5 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) → (𝑋 ∖ 𝑦) ∈ {∅, 𝑋})
41	15, 40	eqeltrd 2688	. . . 4 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) → (∪ {∅, 𝑋} ∖ 𝑦) ∈ {∅, 𝑋})
42	41	ralrimiva 2949	. . 3 ⊢ (𝑋 ∈ 𝑉 → ∀𝑦 ∈ {∅, 𝑋} (∪ {∅, 𝑋} ∖ 𝑦) ∈ {∅, 𝑋})
43		elpwi 4117	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝒫 {∅, 𝑋} → 𝑦 ⊆ {∅, 𝑋})
44		uniss 4394	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ {∅, 𝑋} → ∪ 𝑦 ⊆ ∪ {∅, 𝑋})
45	43, 44	syl 17	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝒫 {∅, 𝑋} → ∪ 𝑦 ⊆ ∪ {∅, 𝑋})
46	45	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) → ∪ 𝑦 ⊆ ∪ {∅, 𝑋})
47	13	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) → ∪ {∅, 𝑋} = 𝑋)
48	46, 47	sseqtrd 3604	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) → ∪ 𝑦 ⊆ 𝑋)
49	48	adantr 480	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋 ∈ 𝑦) → ∪ 𝑦 ⊆ 𝑋)
50		elssuni 4403	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝑦 → 𝑋 ⊆ ∪ 𝑦)
51	50	adantl 481	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋 ∈ 𝑦) → 𝑋 ⊆ ∪ 𝑦)
52	49, 51	jca 553	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋 ∈ 𝑦) → (∪ 𝑦 ⊆ 𝑋 ∧ 𝑋 ⊆ ∪ 𝑦))
53		eqss 3583	. . . . . . . 8 ⊢ (∪ 𝑦 = 𝑋 ↔ (∪ 𝑦 ⊆ 𝑋 ∧ 𝑋 ⊆ ∪ 𝑦))
54	52, 53	sylibr 223	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋 ∈ 𝑦) → ∪ 𝑦 = 𝑋)
55	21	ad2antrr 758	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋 ∈ 𝑦) → 𝑋 ∈ {∅, 𝑋})
56	54, 55	eqeltrd 2688	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋 ∈ 𝑦) → ∪ 𝑦 ∈ {∅, 𝑋})
57		id 22	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝒫 {∅, 𝑋} → 𝑦 ∈ 𝒫 {∅, 𝑋})
58		pwpr 4368	. . . . . . . . . . . 12 ⊢ 𝒫 {∅, 𝑋} = ({∅, {∅}} ∪ {{𝑋}, {∅, 𝑋}})
59	57, 58	syl6eleq 2698	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝒫 {∅, 𝑋} → 𝑦 ∈ ({∅, {∅}} ∪ {{𝑋}, {∅, 𝑋}}))
60	59	adantr 480	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝒫 {∅, 𝑋} ∧ ¬ 𝑋 ∈ 𝑦) → 𝑦 ∈ ({∅, {∅}} ∪ {{𝑋}, {∅, 𝑋}}))
61	60	adantll 746	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋 ∈ 𝑦) → 𝑦 ∈ ({∅, {∅}} ∪ {{𝑋}, {∅, 𝑋}}))
62		snidg 4153	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {𝑋})
63	62	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = {𝑋}) → 𝑋 ∈ {𝑋})
64		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = {𝑋} → 𝑦 = {𝑋})
65	64	eqcomd 2616	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = {𝑋} → {𝑋} = 𝑦)
66	65	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = {𝑋}) → {𝑋} = 𝑦)
67	63, 66	eleqtrd 2690	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = {𝑋}) → 𝑋 ∈ 𝑦)
68	67	adantlr 747	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) ∧ 𝑦 = {𝑋}) → 𝑋 ∈ 𝑦)
69	5	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) ∧ ¬ 𝑦 = {𝑋}) → 𝑋 ∈ 𝑉)
70		simpl 472	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ {{𝑋}, {∅, 𝑋}} ∧ ¬ 𝑦 = {𝑋}) → 𝑦 ∈ {{𝑋}, {∅, 𝑋}})
71	64	necon3bi 2808	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑦 = {𝑋} → 𝑦 ≠ {𝑋})
72	71	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ {{𝑋}, {∅, 𝑋}} ∧ ¬ 𝑦 = {𝑋}) → 𝑦 ≠ {𝑋})
73		elprn1 38700	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ {{𝑋}, {∅, 𝑋}} ∧ 𝑦 ≠ {𝑋}) → 𝑦 = {∅, 𝑋})
74	70, 72, 73	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ {{𝑋}, {∅, 𝑋}} ∧ ¬ 𝑦 = {𝑋}) → 𝑦 = {∅, 𝑋})
75	74	adantll 746	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) ∧ ¬ 𝑦 = {𝑋}) → 𝑦 = {∅, 𝑋})
76	21	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = {∅, 𝑋}) → 𝑋 ∈ {∅, 𝑋})
77		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = {∅, 𝑋} → 𝑦 = {∅, 𝑋})
78	77	eqcomd 2616	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = {∅, 𝑋} → {∅, 𝑋} = 𝑦)
79	78	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = {∅, 𝑋}) → {∅, 𝑋} = 𝑦)
80	76, 79	eleqtrd 2690	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = {∅, 𝑋}) → 𝑋 ∈ 𝑦)
81	69, 75, 80	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) ∧ ¬ 𝑦 = {𝑋}) → 𝑋 ∈ 𝑦)
82	68, 81	pm2.61dan 828	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) → 𝑋 ∈ 𝑦)
83	82	adantlr 747	. . . . . . . . . . 11 ⊢ (((𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑦) ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) → 𝑋 ∈ 𝑦)
84		simplr 788	. . . . . . . . . . 11 ⊢ (((𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑦) ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) → ¬ 𝑋 ∈ 𝑦)
85	83, 84	pm2.65da 598	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑦) → ¬ 𝑦 ∈ {{𝑋}, {∅, 𝑋}})
86	85	adantlr 747	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋 ∈ 𝑦) → ¬ 𝑦 ∈ {{𝑋}, {∅, 𝑋}})
87		elunnel2 38221	. . . . . . . . 9 ⊢ ((𝑦 ∈ ({∅, {∅}} ∪ {{𝑋}, {∅, 𝑋}}) ∧ ¬ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) → 𝑦 ∈ {∅, {∅}})
88	61, 86, 87	syl2anc 691	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋 ∈ 𝑦) → 𝑦 ∈ {∅, {∅}})
89		unieq 4380	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∪ ∅)
90		uni0 4401	. . . . . . . . . . . 12 ⊢ ∪ ∅ = ∅
91	90	a1i 11	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → ∪ ∅ = ∅)
92	89, 91	eqtrd 2644	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∅)
93	92	adantl 481	. . . . . . . . 9 ⊢ ((𝑦 ∈ {∅, {∅}} ∧ 𝑦 = ∅) → ∪ 𝑦 = ∅)
94		simpl 472	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ {∅, {∅}} ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ {∅, {∅}})
95	27	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ {∅, {∅}} ∧ ¬ 𝑦 = ∅) → 𝑦 ≠ ∅)
96		elprn1 38700	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ {∅, {∅}} ∧ 𝑦 ≠ ∅) → 𝑦 = {∅})
97	94, 95, 96	syl2anc 691	. . . . . . . . . 10 ⊢ ((𝑦 ∈ {∅, {∅}} ∧ ¬ 𝑦 = ∅) → 𝑦 = {∅})
98		unieq 4380	. . . . . . . . . . 11 ⊢ (𝑦 = {∅} → ∪ 𝑦 = ∪ {∅})
99	1	unisn 4387	. . . . . . . . . . . 12 ⊢ ∪ {∅} = ∅
100	99	a1i 11	. . . . . . . . . . 11 ⊢ (𝑦 = {∅} → ∪ {∅} = ∅)
101	98, 100	eqtrd 2644	. . . . . . . . . 10 ⊢ (𝑦 = {∅} → ∪ 𝑦 = ∅)
102	97, 101	syl 17	. . . . . . . . 9 ⊢ ((𝑦 ∈ {∅, {∅}} ∧ ¬ 𝑦 = ∅) → ∪ 𝑦 = ∅)
103	93, 102	pm2.61dan 828	. . . . . . . 8 ⊢ (𝑦 ∈ {∅, {∅}} → ∪ 𝑦 = ∅)
104	88, 103	syl 17	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋 ∈ 𝑦) → ∪ 𝑦 = ∅)
105	2	a1i 11	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋 ∈ 𝑦) → ∅ ∈ {∅, 𝑋})
106	104, 105	eqeltrd 2688	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋 ∈ 𝑦) → ∪ 𝑦 ∈ {∅, 𝑋})
107	56, 106	pm2.61dan 828	. . . . 5 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) → ∪ 𝑦 ∈ {∅, 𝑋})
108	107	a1d 25	. . . 4 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) → (𝑦 ≼ ω → ∪ 𝑦 ∈ {∅, 𝑋}))
109	108	ralrimiva 2949	. . 3 ⊢ (𝑋 ∈ 𝑉 → ∀𝑦 ∈ 𝒫 {∅, 𝑋} (𝑦 ≼ ω → ∪ 𝑦 ∈ {∅, 𝑋}))
110	3, 42, 109	3jca 1235	. 2 ⊢ (𝑋 ∈ 𝑉 → (∅ ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ {∅, 𝑋} (∪ {∅, 𝑋} ∖ 𝑦) ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ 𝒫 {∅, 𝑋} (𝑦 ≼ ω → ∪ 𝑦 ∈ {∅, 𝑋})))
111		prex 4836	. . . 4 ⊢ {∅, 𝑋} ∈ V
112	111	a1i 11	. . 3 ⊢ (𝑋 ∈ 𝑉 → {∅, 𝑋} ∈ V)
113		issal 39210	. . 3 ⊢ ({∅, 𝑋} ∈ V → ({∅, 𝑋} ∈ SAlg ↔ (∅ ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ {∅, 𝑋} (∪ {∅, 𝑋} ∖ 𝑦) ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ 𝒫 {∅, 𝑋} (𝑦 ≼ ω → ∪ 𝑦 ∈ {∅, 𝑋}))))
114	112, 113	syl 17	. 2 ⊢ (𝑋 ∈ 𝑉 → ({∅, 𝑋} ∈ SAlg ↔ (∅ ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ {∅, 𝑋} (∪ {∅, 𝑋} ∖ 𝑦) ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ 𝒫 {∅, 𝑋} (𝑦 ≼ ω → ∪ 𝑦 ∈ {∅, 𝑋}))))
115	110, 114	mpbird 246	1 ⊢ (𝑋 ∈ 𝑉 → {∅, 𝑋} ∈ SAlg)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125  {cpr 4127  ∪ cuni 4372   class class class wbr 4583  ωcom 6957   ≼ cdom 7839  SAlgcsalg 39204

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-pw 4110  df-sn 4126  df-pr 4128  df-uni 4373  df-salg 39205

This theorem is referenced by: (None)