Theorem prsal 40538

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 4790	. . . . 5 ⊢ ∅ ∈ V
2	1	prid1 4297	. . . 4 ⊢ ∅ ∈ {∅, 𝑋}
3	2	a1i 11	. . 3 ⊢ (𝑋 ∈ 𝑉 → ∅ ∈ {∅, 𝑋})
4	1	a1i 11	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑉 → ∅ ∈ V)
5		id 22	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ 𝑉)
6		uniprg 4450	. . . . . . . . 9 ⊢ ((∅ ∈ V ∧ 𝑋 ∈ 𝑉) → ∪ {∅, 𝑋} = (∅ ∪ 𝑋))
7	4, 5, 6	syl2anc 693	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑉 → ∪ {∅, 𝑋} = (∅ ∪ 𝑋))
8		uncom 3757	. . . . . . . . . 10 ⊢ (∅ ∪ 𝑋) = (𝑋 ∪ ∅)
9		un0 3967	. . . . . . . . . 10 ⊢ (𝑋 ∪ ∅) = 𝑋
10	8, 9	eqtri 2644	. . . . . . . . 9 ⊢ (∅ ∪ 𝑋) = 𝑋
11	10	a1i 11	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑉 → (∅ ∪ 𝑋) = 𝑋)
12		eqidd 2623	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑉 → 𝑋 = 𝑋)
13	7, 11, 12	3eqtrd 2660	. . . . . . 7 ⊢ (𝑋 ∈ 𝑉 → ∪ {∅, 𝑋} = 𝑋)
14	13	difeq1d 3727	. . . . . 6 ⊢ (𝑋 ∈ 𝑉 → (∪ {∅, 𝑋} ∖ 𝑦) = (𝑋 ∖ 𝑦))
15	14	adantr 481	. . . . 5 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) → (∪ {∅, 𝑋} ∖ 𝑦) = (𝑋 ∖ 𝑦))
16		difeq2 3722	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → (𝑋 ∖ 𝑦) = (𝑋 ∖ ∅))
17	16	adantl 482	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = ∅) → (𝑋 ∖ 𝑦) = (𝑋 ∖ ∅))
18		dif0 3950	. . . . . . . . . 10 ⊢ (𝑋 ∖ ∅) = 𝑋
19	18	a1i 11	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = ∅) → (𝑋 ∖ ∅) = 𝑋)
20	17, 19	eqtrd 2656	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = ∅) → (𝑋 ∖ 𝑦) = 𝑋)
21		prid2g 4296	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {∅, 𝑋})
22	21	adantr 481	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = ∅) → 𝑋 ∈ {∅, 𝑋})
23	20, 22	eqeltrd 2701	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = ∅) → (𝑋 ∖ 𝑦) ∈ {∅, 𝑋})
24	23	adantlr 751	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) ∧ 𝑦 = ∅) → (𝑋 ∖ 𝑦) ∈ {∅, 𝑋})
25		simpll 790	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) ∧ ¬ 𝑦 = ∅) → 𝑋 ∈ 𝑉)
26		simpl 473	. . . . . . . . 9 ⊢ ((𝑦 ∈ {∅, 𝑋} ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ {∅, 𝑋})
27		neqne 2802	. . . . . . . . . 10 ⊢ (¬ 𝑦 = ∅ → 𝑦 ≠ ∅)
28	27	adantl 482	. . . . . . . . 9 ⊢ ((𝑦 ∈ {∅, 𝑋} ∧ ¬ 𝑦 = ∅) → 𝑦 ≠ ∅)
29		elprn1 39865	. . . . . . . . 9 ⊢ ((𝑦 ∈ {∅, 𝑋} ∧ 𝑦 ≠ ∅) → 𝑦 = 𝑋)
30	26, 28, 29	syl2anc 693	. . . . . . . 8 ⊢ ((𝑦 ∈ {∅, 𝑋} ∧ ¬ 𝑦 = ∅) → 𝑦 = 𝑋)
31	30	adantll 750	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) ∧ ¬ 𝑦 = ∅) → 𝑦 = 𝑋)
32		difeq2 3722	. . . . . . . . . 10 ⊢ (𝑦 = 𝑋 → (𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑋))
33		difid 3948	. . . . . . . . . . 11 ⊢ (𝑋 ∖ 𝑋) = ∅
34	33	a1i 11	. . . . . . . . . 10 ⊢ (𝑦 = 𝑋 → (𝑋 ∖ 𝑋) = ∅)
35	32, 34	eqtrd 2656	. . . . . . . . 9 ⊢ (𝑦 = 𝑋 → (𝑋 ∖ 𝑦) = ∅)
36	2	a1i 11	. . . . . . . . 9 ⊢ (𝑦 = 𝑋 → ∅ ∈ {∅, 𝑋})
37	35, 36	eqeltrd 2701	. . . . . . . 8 ⊢ (𝑦 = 𝑋 → (𝑋 ∖ 𝑦) ∈ {∅, 𝑋})
38	37	adantl 482	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = 𝑋) → (𝑋 ∖ 𝑦) ∈ {∅, 𝑋})
39	25, 31, 38	syl2anc 693	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) ∧ ¬ 𝑦 = ∅) → (𝑋 ∖ 𝑦) ∈ {∅, 𝑋})
40	24, 39	pm2.61dan 832	. . . . 5 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) → (𝑋 ∖ 𝑦) ∈ {∅, 𝑋})
41	15, 40	eqeltrd 2701	. . . 4 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) → (∪ {∅, 𝑋} ∖ 𝑦) ∈ {∅, 𝑋})
42	41	ralrimiva 2966	. . 3 ⊢ (𝑋 ∈ 𝑉 → ∀𝑦 ∈ {∅, 𝑋} (∪ {∅, 𝑋} ∖ 𝑦) ∈ {∅, 𝑋})
43		elpwi 4168	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝒫 {∅, 𝑋} → 𝑦 ⊆ {∅, 𝑋})
44		uniss 4458	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ {∅, 𝑋} → ∪ 𝑦 ⊆ ∪ {∅, 𝑋})
45	43, 44	syl 17	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝒫 {∅, 𝑋} → ∪ 𝑦 ⊆ ∪ {∅, 𝑋})
46	45	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) → ∪ 𝑦 ⊆ ∪ {∅, 𝑋})
47	13	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) → ∪ {∅, 𝑋} = 𝑋)
48	46, 47	sseqtrd 3641	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) → ∪ 𝑦 ⊆ 𝑋)
49	48	adantr 481	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋 ∈ 𝑦) → ∪ 𝑦 ⊆ 𝑋)
50		elssuni 4467	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝑦 → 𝑋 ⊆ ∪ 𝑦)
51	50	adantl 482	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋 ∈ 𝑦) → 𝑋 ⊆ ∪ 𝑦)
52	49, 51	jca 554	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋 ∈ 𝑦) → (∪ 𝑦 ⊆ 𝑋 ∧ 𝑋 ⊆ ∪ 𝑦))
53		eqss 3618	. . . . . . . 8 ⊢ (∪ 𝑦 = 𝑋 ↔ (∪ 𝑦 ⊆ 𝑋 ∧ 𝑋 ⊆ ∪ 𝑦))
54	52, 53	sylibr 224	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋 ∈ 𝑦) → ∪ 𝑦 = 𝑋)
55	21	ad2antrr 762	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋 ∈ 𝑦) → 𝑋 ∈ {∅, 𝑋})
56	54, 55	eqeltrd 2701	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋 ∈ 𝑦) → ∪ 𝑦 ∈ {∅, 𝑋})
57		id 22	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝒫 {∅, 𝑋} → 𝑦 ∈ 𝒫 {∅, 𝑋})
58		pwpr 4430	. . . . . . . . . . . 12 ⊢ 𝒫 {∅, 𝑋} = ({∅, {∅}} ∪ {{𝑋}, {∅, 𝑋}})
59	57, 58	syl6eleq 2711	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝒫 {∅, 𝑋} → 𝑦 ∈ ({∅, {∅}} ∪ {{𝑋}, {∅, 𝑋}}))
60	59	adantr 481	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝒫 {∅, 𝑋} ∧ ¬ 𝑋 ∈ 𝑦) → 𝑦 ∈ ({∅, {∅}} ∪ {{𝑋}, {∅, 𝑋}}))
61	60	adantll 750	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋 ∈ 𝑦) → 𝑦 ∈ ({∅, {∅}} ∪ {{𝑋}, {∅, 𝑋}}))
62		snidg 4206	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {𝑋})
63	62	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = {𝑋}) → 𝑋 ∈ {𝑋})
64		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = {𝑋} → 𝑦 = {𝑋})
65	64	eqcomd 2628	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = {𝑋} → {𝑋} = 𝑦)
66	65	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = {𝑋}) → {𝑋} = 𝑦)
67	63, 66	eleqtrd 2703	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = {𝑋}) → 𝑋 ∈ 𝑦)
68	67	adantlr 751	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) ∧ 𝑦 = {𝑋}) → 𝑋 ∈ 𝑦)
69	5	ad2antrr 762	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) ∧ ¬ 𝑦 = {𝑋}) → 𝑋 ∈ 𝑉)
70		simpl 473	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ {{𝑋}, {∅, 𝑋}} ∧ ¬ 𝑦 = {𝑋}) → 𝑦 ∈ {{𝑋}, {∅, 𝑋}})
71	64	necon3bi 2820	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑦 = {𝑋} → 𝑦 ≠ {𝑋})
72	71	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ {{𝑋}, {∅, 𝑋}} ∧ ¬ 𝑦 = {𝑋}) → 𝑦 ≠ {𝑋})
73		elprn1 39865	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ {{𝑋}, {∅, 𝑋}} ∧ 𝑦 ≠ {𝑋}) → 𝑦 = {∅, 𝑋})
74	70, 72, 73	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ {{𝑋}, {∅, 𝑋}} ∧ ¬ 𝑦 = {𝑋}) → 𝑦 = {∅, 𝑋})
75	74	adantll 750	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) ∧ ¬ 𝑦 = {𝑋}) → 𝑦 = {∅, 𝑋})
76	21	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = {∅, 𝑋}) → 𝑋 ∈ {∅, 𝑋})
77		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = {∅, 𝑋} → 𝑦 = {∅, 𝑋})
78	77	eqcomd 2628	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = {∅, 𝑋} → {∅, 𝑋} = 𝑦)
79	78	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = {∅, 𝑋}) → {∅, 𝑋} = 𝑦)
80	76, 79	eleqtrd 2703	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = {∅, 𝑋}) → 𝑋 ∈ 𝑦)
81	69, 75, 80	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) ∧ ¬ 𝑦 = {𝑋}) → 𝑋 ∈ 𝑦)
82	68, 81	pm2.61dan 832	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) → 𝑋 ∈ 𝑦)
83	82	adantlr 751	. . . . . . . . . . 11 ⊢ (((𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑦) ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) → 𝑋 ∈ 𝑦)
84		simplr 792	. . . . . . . . . . 11 ⊢ (((𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑦) ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) → ¬ 𝑋 ∈ 𝑦)
85	83, 84	pm2.65da 600	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑦) → ¬ 𝑦 ∈ {{𝑋}, {∅, 𝑋}})
86	85	adantlr 751	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋 ∈ 𝑦) → ¬ 𝑦 ∈ {{𝑋}, {∅, 𝑋}})
87		elunnel2 39198	. . . . . . . . 9 ⊢ ((𝑦 ∈ ({∅, {∅}} ∪ {{𝑋}, {∅, 𝑋}}) ∧ ¬ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) → 𝑦 ∈ {∅, {∅}})
88	61, 86, 87	syl2anc 693	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋 ∈ 𝑦) → 𝑦 ∈ {∅, {∅}})
89		unieq 4444	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∪ ∅)
90		uni0 4465	. . . . . . . . . . . 12 ⊢ ∪ ∅ = ∅
91	90	a1i 11	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → ∪ ∅ = ∅)
92	89, 91	eqtrd 2656	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∅)
93	92	adantl 482	. . . . . . . . 9 ⊢ ((𝑦 ∈ {∅, {∅}} ∧ 𝑦 = ∅) → ∪ 𝑦 = ∅)
94		simpl 473	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ {∅, {∅}} ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ {∅, {∅}})
95	27	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ {∅, {∅}} ∧ ¬ 𝑦 = ∅) → 𝑦 ≠ ∅)
96		elprn1 39865	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ {∅, {∅}} ∧ 𝑦 ≠ ∅) → 𝑦 = {∅})
97	94, 95, 96	syl2anc 693	. . . . . . . . . 10 ⊢ ((𝑦 ∈ {∅, {∅}} ∧ ¬ 𝑦 = ∅) → 𝑦 = {∅})
98		unieq 4444	. . . . . . . . . . 11 ⊢ (𝑦 = {∅} → ∪ 𝑦 = ∪ {∅})
99	1	unisn 4451	. . . . . . . . . . . 12 ⊢ ∪ {∅} = ∅
100	99	a1i 11	. . . . . . . . . . 11 ⊢ (𝑦 = {∅} → ∪ {∅} = ∅)
101	98, 100	eqtrd 2656	. . . . . . . . . 10 ⊢ (𝑦 = {∅} → ∪ 𝑦 = ∅)
102	97, 101	syl 17	. . . . . . . . 9 ⊢ ((𝑦 ∈ {∅, {∅}} ∧ ¬ 𝑦 = ∅) → ∪ 𝑦 = ∅)
103	93, 102	pm2.61dan 832	. . . . . . . 8 ⊢ (𝑦 ∈ {∅, {∅}} → ∪ 𝑦 = ∅)
104	88, 103	syl 17	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋 ∈ 𝑦) → ∪ 𝑦 = ∅)
105	2	a1i 11	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋 ∈ 𝑦) → ∅ ∈ {∅, 𝑋})
106	104, 105	eqeltrd 2701	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋 ∈ 𝑦) → ∪ 𝑦 ∈ {∅, 𝑋})
107	56, 106	pm2.61dan 832	. . . . 5 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) → ∪ 𝑦 ∈ {∅, 𝑋})
108	107	a1d 25	. . . 4 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) → (𝑦 ≼ ω → ∪ 𝑦 ∈ {∅, 𝑋}))
109	108	ralrimiva 2966	. . 3 ⊢ (𝑋 ∈ 𝑉 → ∀𝑦 ∈ 𝒫 {∅, 𝑋} (𝑦 ≼ ω → ∪ 𝑦 ∈ {∅, 𝑋}))
110	3, 42, 109	3jca 1242	. 2 ⊢ (𝑋 ∈ 𝑉 → (∅ ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ {∅, 𝑋} (∪ {∅, 𝑋} ∖ 𝑦) ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ 𝒫 {∅, 𝑋} (𝑦 ≼ ω → ∪ 𝑦 ∈ {∅, 𝑋})))
111		prex 4909	. . . 4 ⊢ {∅, 𝑋} ∈ V
112	111	a1i 11	. . 3 ⊢ (𝑋 ∈ 𝑉 → {∅, 𝑋} ∈ V)
113		issal 40534	. . 3 ⊢ ({∅, 𝑋} ∈ V → ({∅, 𝑋} ∈ SAlg ↔ (∅ ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ {∅, 𝑋} (∪ {∅, 𝑋} ∖ 𝑦) ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ 𝒫 {∅, 𝑋} (𝑦 ≼ ω → ∪ 𝑦 ∈ {∅, 𝑋}))))
114	112, 113	syl 17	. 2 ⊢ (𝑋 ∈ 𝑉 → ({∅, 𝑋} ∈ SAlg ↔ (∅ ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ {∅, 𝑋} (∪ {∅, 𝑋} ∖ 𝑦) ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ 𝒫 {∅, 𝑋} (𝑦 ≼ ω → ∪ 𝑦 ∈ {∅, 𝑋}))))
115	110, 114	mpbird 247	1 ⊢ (𝑋 ∈ 𝑉 → {∅, 𝑋} ∈ SAlg)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912  Vcvv 3200   ∖ cdif 3571   ∪ cun 3572   ⊆ wss 3574  ∅c0 3915  𝒫 cpw 4158  {csn 4177  {cpr 4179  ∪ cuni 4436   class class class wbr 4653  ωcom 7065   ≼ cdom 7953  SAlgcsalg 40528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-pw 4160  df-sn 4178  df-pr 4180  df-uni 4437  df-salg 40529

This theorem is referenced by: (None)