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	|- ( X e. V -> { (/) , X } e. SAlg )

Proof of Theorem prsal

Dummy variable y is distinct from all other variables.

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

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   _Vcvv 3200   \ cdif 3571   u. cun 3572   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   {csn 4177   {cpr 4179   U.cuni 4436   class class class wbr 4653   omcom 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)