Theorem prsal 41329

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 5014	. . . . 5 ⊢ ∅ ∈ V
2	1	prid1 4515	. . . 4 ⊢ ∅ ∈ {∅, 𝑋}
3	2	a1i 11	. . 3 ⊢ (𝑋 ∈ 𝑉 → ∅ ∈ {∅, 𝑋})
4	1	a1i 11	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑉 → ∅ ∈ V)
5		id 22	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ 𝑉)
6		uniprg 4672	. . . . . . . . 9 ⊢ ((∅ ∈ V ∧ 𝑋 ∈ 𝑉) → ∪ {∅, 𝑋} = (∅ ∪ 𝑋))
7	4, 5, 6	syl2anc 581	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑉 → ∪ {∅, 𝑋} = (∅ ∪ 𝑋))
8		uncom 3984	. . . . . . . . . 10 ⊢ (∅ ∪ 𝑋) = (𝑋 ∪ ∅)
9		un0 4192	. . . . . . . . . 10 ⊢ (𝑋 ∪ ∅) = 𝑋
10	8, 9	eqtri 2849	. . . . . . . . 9 ⊢ (∅ ∪ 𝑋) = 𝑋
11	10	a1i 11	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑉 → (∅ ∪ 𝑋) = 𝑋)
12		eqidd 2826	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑉 → 𝑋 = 𝑋)
13	7, 11, 12	3eqtrd 2865	. . . . . . 7 ⊢ (𝑋 ∈ 𝑉 → ∪ {∅, 𝑋} = 𝑋)
14	13	difeq1d 3954	. . . . . 6 ⊢ (𝑋 ∈ 𝑉 → (∪ {∅, 𝑋} ∖ 𝑦) = (𝑋 ∖ 𝑦))
15	14	adantr 474	. . . . 5 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) → (∪ {∅, 𝑋} ∖ 𝑦) = (𝑋 ∖ 𝑦))
16		difeq2 3949	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → (𝑋 ∖ 𝑦) = (𝑋 ∖ ∅))
17	16	adantl 475	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = ∅) → (𝑋 ∖ 𝑦) = (𝑋 ∖ ∅))
18		dif0 4180	. . . . . . . . . 10 ⊢ (𝑋 ∖ ∅) = 𝑋
19	18	a1i 11	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = ∅) → (𝑋 ∖ ∅) = 𝑋)
20	17, 19	eqtrd 2861	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = ∅) → (𝑋 ∖ 𝑦) = 𝑋)
21		prid2g 4514	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {∅, 𝑋})
22	21	adantr 474	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = ∅) → 𝑋 ∈ {∅, 𝑋})
23	20, 22	eqeltrd 2906	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = ∅) → (𝑋 ∖ 𝑦) ∈ {∅, 𝑋})
24	23	adantlr 708	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) ∧ 𝑦 = ∅) → (𝑋 ∖ 𝑦) ∈ {∅, 𝑋})
25		simpll 785	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) ∧ ¬ 𝑦 = ∅) → 𝑋 ∈ 𝑉)
26		simpl 476	. . . . . . . . 9 ⊢ ((𝑦 ∈ {∅, 𝑋} ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ {∅, 𝑋})
27		neqne 3007	. . . . . . . . . 10 ⊢ (¬ 𝑦 = ∅ → 𝑦 ≠ ∅)
28	27	adantl 475	. . . . . . . . 9 ⊢ ((𝑦 ∈ {∅, 𝑋} ∧ ¬ 𝑦 = ∅) → 𝑦 ≠ ∅)
29		elprn1 40660	. . . . . . . . 9 ⊢ ((𝑦 ∈ {∅, 𝑋} ∧ 𝑦 ≠ ∅) → 𝑦 = 𝑋)
30	26, 28, 29	syl2anc 581	. . . . . . . 8 ⊢ ((𝑦 ∈ {∅, 𝑋} ∧ ¬ 𝑦 = ∅) → 𝑦 = 𝑋)
31	30	adantll 707	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) ∧ ¬ 𝑦 = ∅) → 𝑦 = 𝑋)
32		difeq2 3949	. . . . . . . . . 10 ⊢ (𝑦 = 𝑋 → (𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑋))
33		difid 4178	. . . . . . . . . . 11 ⊢ (𝑋 ∖ 𝑋) = ∅
34	33	a1i 11	. . . . . . . . . 10 ⊢ (𝑦 = 𝑋 → (𝑋 ∖ 𝑋) = ∅)
35	32, 34	eqtrd 2861	. . . . . . . . 9 ⊢ (𝑦 = 𝑋 → (𝑋 ∖ 𝑦) = ∅)
36	2	a1i 11	. . . . . . . . 9 ⊢ (𝑦 = 𝑋 → ∅ ∈ {∅, 𝑋})
37	35, 36	eqeltrd 2906	. . . . . . . 8 ⊢ (𝑦 = 𝑋 → (𝑋 ∖ 𝑦) ∈ {∅, 𝑋})
38	37	adantl 475	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = 𝑋) → (𝑋 ∖ 𝑦) ∈ {∅, 𝑋})
39	25, 31, 38	syl2anc 581	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) ∧ ¬ 𝑦 = ∅) → (𝑋 ∖ 𝑦) ∈ {∅, 𝑋})
40	24, 39	pm2.61dan 849	. . . . 5 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) → (𝑋 ∖ 𝑦) ∈ {∅, 𝑋})
41	15, 40	eqeltrd 2906	. . . 4 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {∅, 𝑋}) → (∪ {∅, 𝑋} ∖ 𝑦) ∈ {∅, 𝑋})
42	41	ralrimiva 3175	. . 3 ⊢ (𝑋 ∈ 𝑉 → ∀𝑦 ∈ {∅, 𝑋} (∪ {∅, 𝑋} ∖ 𝑦) ∈ {∅, 𝑋})
43		elpwi 4388	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝒫 {∅, 𝑋} → 𝑦 ⊆ {∅, 𝑋})
44		uniss 4681	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ {∅, 𝑋} → ∪ 𝑦 ⊆ ∪ {∅, 𝑋})
45	43, 44	syl 17	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝒫 {∅, 𝑋} → ∪ 𝑦 ⊆ ∪ {∅, 𝑋})
46	45	adantl 475	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) → ∪ 𝑦 ⊆ ∪ {∅, 𝑋})
47	13	adantr 474	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) → ∪ {∅, 𝑋} = 𝑋)
48	46, 47	sseqtrd 3866	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) → ∪ 𝑦 ⊆ 𝑋)
49	48	adantr 474	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋 ∈ 𝑦) → ∪ 𝑦 ⊆ 𝑋)
50		elssuni 4689	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝑦 → 𝑋 ⊆ ∪ 𝑦)
51	50	adantl 475	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋 ∈ 𝑦) → 𝑋 ⊆ ∪ 𝑦)
52	49, 51	jca 509	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋 ∈ 𝑦) → (∪ 𝑦 ⊆ 𝑋 ∧ 𝑋 ⊆ ∪ 𝑦))
53		eqss 3842	. . . . . . . 8 ⊢ (∪ 𝑦 = 𝑋 ↔ (∪ 𝑦 ⊆ 𝑋 ∧ 𝑋 ⊆ ∪ 𝑦))
54	52, 53	sylibr 226	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋 ∈ 𝑦) → ∪ 𝑦 = 𝑋)
55	21	ad2antrr 719	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋 ∈ 𝑦) → 𝑋 ∈ {∅, 𝑋})
56	54, 55	eqeltrd 2906	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋 ∈ 𝑦) → ∪ 𝑦 ∈ {∅, 𝑋})
57		id 22	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝒫 {∅, 𝑋} → 𝑦 ∈ 𝒫 {∅, 𝑋})
58		pwpr 4652	. . . . . . . . . . . 12 ⊢ 𝒫 {∅, 𝑋} = ({∅, {∅}} ∪ {{𝑋}, {∅, 𝑋}})
59	57, 58	syl6eleq 2916	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝒫 {∅, 𝑋} → 𝑦 ∈ ({∅, {∅}} ∪ {{𝑋}, {∅, 𝑋}}))
60	59	adantr 474	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝒫 {∅, 𝑋} ∧ ¬ 𝑋 ∈ 𝑦) → 𝑦 ∈ ({∅, {∅}} ∪ {{𝑋}, {∅, 𝑋}}))
61	60	adantll 707	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋 ∈ 𝑦) → 𝑦 ∈ ({∅, {∅}} ∪ {{𝑋}, {∅, 𝑋}}))
62		snidg 4427	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {𝑋})
63	62	adantr 474	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = {𝑋}) → 𝑋 ∈ {𝑋})
64		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = {𝑋} → 𝑦 = {𝑋})
65	64	eqcomd 2831	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = {𝑋} → {𝑋} = 𝑦)
66	65	adantl 475	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = {𝑋}) → {𝑋} = 𝑦)
67	63, 66	eleqtrd 2908	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = {𝑋}) → 𝑋 ∈ 𝑦)
68	67	adantlr 708	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) ∧ 𝑦 = {𝑋}) → 𝑋 ∈ 𝑦)
69	5	ad2antrr 719	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) ∧ ¬ 𝑦 = {𝑋}) → 𝑋 ∈ 𝑉)
70		simpl 476	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ {{𝑋}, {∅, 𝑋}} ∧ ¬ 𝑦 = {𝑋}) → 𝑦 ∈ {{𝑋}, {∅, 𝑋}})
71	64	necon3bi 3025	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑦 = {𝑋} → 𝑦 ≠ {𝑋})
72	71	adantl 475	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ {{𝑋}, {∅, 𝑋}} ∧ ¬ 𝑦 = {𝑋}) → 𝑦 ≠ {𝑋})
73		elprn1 40660	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ {{𝑋}, {∅, 𝑋}} ∧ 𝑦 ≠ {𝑋}) → 𝑦 = {∅, 𝑋})
74	70, 72, 73	syl2anc 581	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ {{𝑋}, {∅, 𝑋}} ∧ ¬ 𝑦 = {𝑋}) → 𝑦 = {∅, 𝑋})
75	74	adantll 707	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) ∧ ¬ 𝑦 = {𝑋}) → 𝑦 = {∅, 𝑋})
76	21	adantr 474	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = {∅, 𝑋}) → 𝑋 ∈ {∅, 𝑋})
77		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = {∅, 𝑋} → 𝑦 = {∅, 𝑋})
78	77	eqcomd 2831	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = {∅, 𝑋} → {∅, 𝑋} = 𝑦)
79	78	adantl 475	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = {∅, 𝑋}) → {∅, 𝑋} = 𝑦)
80	76, 79	eleqtrd 2908	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = {∅, 𝑋}) → 𝑋 ∈ 𝑦)
81	69, 75, 80	syl2anc 581	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) ∧ ¬ 𝑦 = {𝑋}) → 𝑋 ∈ 𝑦)
82	68, 81	pm2.61dan 849	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) → 𝑋 ∈ 𝑦)
83	82	adantlr 708	. . . . . . . . . . 11 ⊢ (((𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑦) ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) → 𝑋 ∈ 𝑦)
84		simplr 787	. . . . . . . . . . 11 ⊢ (((𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑦) ∧ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) → ¬ 𝑋 ∈ 𝑦)
85	83, 84	pm2.65da 853	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑦) → ¬ 𝑦 ∈ {{𝑋}, {∅, 𝑋}})
86	85	adantlr 708	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋 ∈ 𝑦) → ¬ 𝑦 ∈ {{𝑋}, {∅, 𝑋}})
87		elunnel2 40016	. . . . . . . . 9 ⊢ ((𝑦 ∈ ({∅, {∅}} ∪ {{𝑋}, {∅, 𝑋}}) ∧ ¬ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) → 𝑦 ∈ {∅, {∅}})
88	61, 86, 87	syl2anc 581	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋 ∈ 𝑦) → 𝑦 ∈ {∅, {∅}})
89		unieq 4666	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∪ ∅)
90		uni0 4687	. . . . . . . . . . . 12 ⊢ ∪ ∅ = ∅
91	90	a1i 11	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → ∪ ∅ = ∅)
92	89, 91	eqtrd 2861	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∅)
93	92	adantl 475	. . . . . . . . 9 ⊢ ((𝑦 ∈ {∅, {∅}} ∧ 𝑦 = ∅) → ∪ 𝑦 = ∅)
94		simpl 476	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ {∅, {∅}} ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ {∅, {∅}})
95	27	adantl 475	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ {∅, {∅}} ∧ ¬ 𝑦 = ∅) → 𝑦 ≠ ∅)
96		elprn1 40660	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ {∅, {∅}} ∧ 𝑦 ≠ ∅) → 𝑦 = {∅})
97	94, 95, 96	syl2anc 581	. . . . . . . . . 10 ⊢ ((𝑦 ∈ {∅, {∅}} ∧ ¬ 𝑦 = ∅) → 𝑦 = {∅})
98		unieq 4666	. . . . . . . . . . 11 ⊢ (𝑦 = {∅} → ∪ 𝑦 = ∪ {∅})
99	1	unisn 4674	. . . . . . . . . . . 12 ⊢ ∪ {∅} = ∅
100	99	a1i 11	. . . . . . . . . . 11 ⊢ (𝑦 = {∅} → ∪ {∅} = ∅)
101	98, 100	eqtrd 2861	. . . . . . . . . 10 ⊢ (𝑦 = {∅} → ∪ 𝑦 = ∅)
102	97, 101	syl 17	. . . . . . . . 9 ⊢ ((𝑦 ∈ {∅, {∅}} ∧ ¬ 𝑦 = ∅) → ∪ 𝑦 = ∅)
103	93, 102	pm2.61dan 849	. . . . . . . 8 ⊢ (𝑦 ∈ {∅, {∅}} → ∪ 𝑦 = ∅)
104	88, 103	syl 17	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋 ∈ 𝑦) → ∪ 𝑦 = ∅)
105	2	a1i 11	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋 ∈ 𝑦) → ∅ ∈ {∅, 𝑋})
106	104, 105	eqeltrd 2906	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋 ∈ 𝑦) → ∪ 𝑦 ∈ {∅, 𝑋})
107	56, 106	pm2.61dan 849	. . . . 5 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) → ∪ 𝑦 ∈ {∅, 𝑋})
108	107	a1d 25	. . . 4 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 {∅, 𝑋}) → (𝑦 ≼ ω → ∪ 𝑦 ∈ {∅, 𝑋}))
109	108	ralrimiva 3175	. . 3 ⊢ (𝑋 ∈ 𝑉 → ∀𝑦 ∈ 𝒫 {∅, 𝑋} (𝑦 ≼ ω → ∪ 𝑦 ∈ {∅, 𝑋}))
110	3, 42, 109	3jca 1164	. 2 ⊢ (𝑋 ∈ 𝑉 → (∅ ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ {∅, 𝑋} (∪ {∅, 𝑋} ∖ 𝑦) ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ 𝒫 {∅, 𝑋} (𝑦 ≼ ω → ∪ 𝑦 ∈ {∅, 𝑋})))
111		prex 5130	. . . 4 ⊢ {∅, 𝑋} ∈ V
112	111	a1i 11	. . 3 ⊢ (𝑋 ∈ 𝑉 → {∅, 𝑋} ∈ V)
113		issal 41325	. . 3 ⊢ ({∅, 𝑋} ∈ V → ({∅, 𝑋} ∈ SAlg ↔ (∅ ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ {∅, 𝑋} (∪ {∅, 𝑋} ∖ 𝑦) ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ 𝒫 {∅, 𝑋} (𝑦 ≼ ω → ∪ 𝑦 ∈ {∅, 𝑋}))))
114	112, 113	syl 17	. 2 ⊢ (𝑋 ∈ 𝑉 → ({∅, 𝑋} ∈ SAlg ↔ (∅ ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ {∅, 𝑋} (∪ {∅, 𝑋} ∖ 𝑦) ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ 𝒫 {∅, 𝑋} (𝑦 ≼ ω → ∪ 𝑦 ∈ {∅, 𝑋}))))
115	110, 114	mpbird 249	1 ⊢ (𝑋 ∈ 𝑉 → {∅, 𝑋} ∈ SAlg)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1113   = wceq 1658   ∈ wcel 2166   ≠ wne 2999  ∀wral 3117  Vcvv 3414   ∖ cdif 3795   ∪ cun 3796   ⊆ wss 3798  ∅c0 4144  𝒫 cpw 4378  {csn 4397  {cpr 4399  ∪ cuni 4658   class class class wbr 4873  ωcom 7326   ≼ cdom 8220  SAlgcsalg 41319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pr 5127

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-pw 4380  df-sn 4398  df-pr 4400  df-uni 4659  df-salg 41320

This theorem is referenced by: (None)