Theorem prsal 38291

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 4528	. . . . 5 |- (/) e. _V
2	1	prid1 4071	. . . 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 4204	. . . . . . . . 9 |- ( ( (/) e. _V /\ X e. V ) -> U. { (/) , X } = ( (/) u. X ) )
7	4, 5, 6	syl2anc 673	. . . . . . . 8 |- ( X e. V -> U. { (/) , X } = ( (/) u. X ) )
8		uncom 3569	. . . . . . . . . 10 |- ( (/) u. X ) = ( X u. (/) )
9		un0 3762	. . . . . . . . . 10 |- ( X u. (/) ) = X
10	8, 9	eqtri 2493	. . . . . . . . 9 |- ( (/) u. X ) = X
11	10	a1i 11	. . . . . . . 8 |- ( X e. V -> ( (/) u. X ) = X )
12		eqidd 2472	. . . . . . . 8 |- ( X e. V -> X = X )
13	7, 11, 12	3eqtrd 2509	. . . . . . 7 |- ( X e. V -> U. { (/) , X } = X )
14	13	difeq1d 3539	. . . . . 6 |- ( X e. V -> ( U. { (/) , X } \ y ) = ( X \ y ) )
15	14	adantr 472	. . . . 5 |- ( ( X e. V /\ y e. { (/) , X } ) -> ( U. { (/) , X } \ y ) = ( X \ y ) )
16		difeq2 3534	. . . . . . . . . 10 |- ( y = (/) -> ( X \ y ) = ( X \ (/) ) )
17	16	adantl 473	. . . . . . . . 9 |- ( ( X e. V /\ y = (/) ) -> ( X \ y ) = ( X \ (/) ) )
18		dif0 3749	. . . . . . . . . 10 |- ( X \ (/) ) = X
19	18	a1i 11	. . . . . . . . 9 |- ( ( X e. V /\ y = (/) ) -> ( X \ (/) ) = X )
20	17, 19	eqtrd 2505	. . . . . . . 8 |- ( ( X e. V /\ y = (/) ) -> ( X \ y ) = X )
21		prid2g 4070	. . . . . . . . 9 |- ( X e. V -> X e. { (/) , X } )
22	21	adantr 472	. . . . . . . 8 |- ( ( X e. V /\ y = (/) ) -> X e. { (/) , X } )
23	20, 22	eqeltrd 2549	. . . . . . 7 |- ( ( X e. V /\ y = (/) ) -> ( X \ y ) e. { (/) , X } )
24	23	adantlr 729	. . . . . 6 |- ( ( ( X e. V /\ y e. { (/) , X } ) /\ y = (/) ) -> ( X \ y ) e. { (/) , X } )
25		simpll 768	. . . . . . 7 |- ( ( ( X e. V /\ y e. { (/) , X } ) /\ -. y = (/) ) -> X e. V )
26		simpl 464	. . . . . . . . 9 |- ( ( y e. { (/) , X } /\ -. y = (/) ) -> y e. { (/) , X } )
27		neqne 2651	. . . . . . . . . 10 |- ( -. y = (/) -> y =/= (/) )
28	27	adantl 473	. . . . . . . . 9 |- ( ( y e. { (/) , X } /\ -. y = (/) ) -> y =/= (/) )
29		elprn1 37810	. . . . . . . . 9 |- ( ( y e. { (/) , X } /\ y =/= (/) ) -> y = X )
30	26, 28, 29	syl2anc 673	. . . . . . . 8 |- ( ( y e. { (/) , X } /\ -. y = (/) ) -> y = X )
31	30	adantll 728	. . . . . . 7 |- ( ( ( X e. V /\ y e. { (/) , X } ) /\ -. y = (/) ) -> y = X )
32		difeq2 3534	. . . . . . . . . 10 |- ( y = X -> ( X \ y ) = ( X \ X ) )
33		difid 3747	. . . . . . . . . . 11 |- ( X \ X ) = (/)
34	33	a1i 11	. . . . . . . . . 10 |- ( y = X -> ( X \ X ) = (/) )
35	32, 34	eqtrd 2505	. . . . . . . . 9 |- ( y = X -> ( X \ y ) = (/) )
36	2	a1i 11	. . . . . . . . 9 |- ( y = X -> (/) e. { (/) , X } )
37	35, 36	eqeltrd 2549	. . . . . . . 8 |- ( y = X -> ( X \ y ) e. { (/) , X } )
38	37	adantl 473	. . . . . . 7 |- ( ( X e. V /\ y = X ) -> ( X \ y ) e. { (/) , X } )
39	25, 31, 38	syl2anc 673	. . . . . 6 |- ( ( ( X e. V /\ y e. { (/) , X } ) /\ -. y = (/) ) -> ( X \ y ) e. { (/) , X } )
40	24, 39	pm2.61dan 808	. . . . 5 |- ( ( X e. V /\ y e. { (/) , X } ) -> ( X \ y ) e. { (/) , X } )
41	15, 40	eqeltrd 2549	. . . 4 |- ( ( X e. V /\ y e. { (/) , X } ) -> ( U. { (/) , X } \ y ) e. { (/) , X } )
42	41	ralrimiva 2809	. . 3 |- ( X e. V -> A. y e. { (/) , X } ( U. { (/) , X } \ y ) e. { (/) , X } )
43		elpwi 3951	. . . . . . . . . . . . 13 |- ( y e. ~P { (/) , X } -> y C_ { (/) , X } )
44		uniss 4211	. . . . . . . . . . . . 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 473	. . . . . . . . . . 11 |- ( ( X e. V /\ y e. ~P { (/) , X } ) -> U. y C_ U. { (/) , X } )
47	13	adantr 472	. . . . . . . . . . 11 |- ( ( X e. V /\ y e. ~P { (/) , X } ) -> U. { (/) , X } = X )
48	46, 47	sseqtrd 3454	. . . . . . . . . 10 |- ( ( X e. V /\ y e. ~P { (/) , X } ) -> U. y C_ X )
49	48	adantr 472	. . . . . . . . 9 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ X e. y ) -> U. y C_ X )
50		elssuni 4219	. . . . . . . . . 10 |- ( X e. y -> X C_ U. y )
51	50	adantl 473	. . . . . . . . 9 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ X e. y ) -> X C_ U. y )
52	49, 51	jca 541	. . . . . . . 8 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ X e. y ) -> ( U. y C_ X /\ X C_ U. y ) )
53		eqss 3433	. . . . . . . 8 |- ( U. y = X <-> ( U. y C_ X /\ X C_ U. y ) )
54	52, 53	sylibr 217	. . . . . . 7 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ X e. y ) -> U. y = X )
55	21	ad2antrr 740	. . . . . . 7 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ X e. y ) -> X e. { (/) , X } )
56	54, 55	eqeltrd 2549	. . . . . 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 4186	. . . . . . . . . . . 12 |- ~P { (/) , X } = ( { (/) , { (/) } } u. { { X } , { (/) , X } } )
59	57, 58	syl6eleq 2559	. . . . . . . . . . 11 |- ( y e. ~P { (/) , X } -> y e. ( { (/) , { (/) } } u. { { X } , { (/) , X } } ) )
60	59	adantr 472	. . . . . . . . . 10 |- ( ( y e. ~P { (/) , X } /\ -. X e. y ) -> y e. ( { (/) , { (/) } } u. { { X } , { (/) , X } } ) )
61	60	adantll 728	. . . . . . . . 9 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ -. X e. y ) -> y e. ( { (/) , { (/) } } u. { { X } , { (/) , X } } ) )
62		snidg 3986	. . . . . . . . . . . . . . . 16 |- ( X e. V -> X e. { X } )
63	62	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( X e. V /\ y = { X } ) -> X e. { X } )
64		id 22	. . . . . . . . . . . . . . . . 17 |- ( y = { X } -> y = { X } )
65	64	eqcomd 2477	. . . . . . . . . . . . . . . 16 |- ( y = { X } -> { X } = y )
66	65	adantl 473	. . . . . . . . . . . . . . 15 |- ( ( X e. V /\ y = { X } ) -> { X } = y )
67	63, 66	eleqtrd 2551	. . . . . . . . . . . . . 14 |- ( ( X e. V /\ y = { X } ) -> X e. y )
68	67	adantlr 729	. . . . . . . . . . . . 13 |- ( ( ( X e. V /\ y e. { { X } , { (/) , X } } ) /\ y = { X } ) -> X e. y )
69	5	ad2antrr 740	. . . . . . . . . . . . . 14 |- ( ( ( X e. V /\ y e. { { X } , { (/) , X } } ) /\ -. y = { X } ) -> X e. V )
70		simpl 464	. . . . . . . . . . . . . . . 16 |- ( ( y e. { { X } , { (/) , X } } /\ -. y = { X } ) -> y e. { { X } , { (/) , X } } )
71	64	necon3bi 2669	. . . . . . . . . . . . . . . . 17 |- ( -. y = { X } -> y =/= { X } )
72	71	adantl 473	. . . . . . . . . . . . . . . 16 |- ( ( y e. { { X } , { (/) , X } } /\ -. y = { X } ) -> y =/= { X } )
73		elprn1 37810	. . . . . . . . . . . . . . . 16 |- ( ( y e. { { X } , { (/) , X } } /\ y =/= { X } ) -> y = { (/) , X } )
74	70, 72, 73	syl2anc 673	. . . . . . . . . . . . . . 15 |- ( ( y e. { { X } , { (/) , X } } /\ -. y = { X } ) -> y = { (/) , X } )
75	74	adantll 728	. . . . . . . . . . . . . 14 |- ( ( ( X e. V /\ y e. { { X } , { (/) , X } } ) /\ -. y = { X } ) -> y = { (/) , X } )
76	21	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( X e. V /\ y = { (/) , X } ) -> X e. { (/) , X } )
77		id 22	. . . . . . . . . . . . . . . . 17 |- ( y = { (/) , X } -> y = { (/) , X } )
78	77	eqcomd 2477	. . . . . . . . . . . . . . . 16 |- ( y = { (/) , X } -> { (/) , X } = y )
79	78	adantl 473	. . . . . . . . . . . . . . 15 |- ( ( X e. V /\ y = { (/) , X } ) -> { (/) , X } = y )
80	76, 79	eleqtrd 2551	. . . . . . . . . . . . . 14 |- ( ( X e. V /\ y = { (/) , X } ) -> X e. y )
81	69, 75, 80	syl2anc 673	. . . . . . . . . . . . 13 |- ( ( ( X e. V /\ y e. { { X } , { (/) , X } } ) /\ -. y = { X } ) -> X e. y )
82	68, 81	pm2.61dan 808	. . . . . . . . . . . 12 |- ( ( X e. V /\ y e. { { X } , { (/) , X } } ) -> X e. y )
83	82	adantlr 729	. . . . . . . . . . 11 |- ( ( ( X e. V /\ -. X e. y ) /\ y e. { { X } , { (/) , X } } ) -> X e. y )
84		simplr 770	. . . . . . . . . . 11 |- ( ( ( X e. V /\ -. X e. y ) /\ y e. { { X } , { (/) , X } } ) -> -. X e. y )
85	83, 84	pm2.65da 586	. . . . . . . . . 10 |- ( ( X e. V /\ -. X e. y ) -> -. y e. { { X } , { (/) , X } } )
86	85	adantlr 729	. . . . . . . . 9 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ -. X e. y ) -> -. y e. { { X } , { (/) , X } } )
87		elunnel2 37423	. . . . . . . . 9 |- ( ( y e. ( { (/) , { (/) } } u. { { X } , { (/) , X } } ) /\ -. y e. { { X } , { (/) , X } } ) -> y e. { (/) , { (/) } } )
88	61, 86, 87	syl2anc 673	. . . . . . . 8 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ -. X e. y ) -> y e. { (/) , { (/) } } )
89		unieq 4198	. . . . . . . . . . 11 |- ( y = (/) -> U. y = U. (/) )
90		uni0 4217	. . . . . . . . . . . 12 |- U. (/) = (/)
91	90	a1i 11	. . . . . . . . . . 11 |- ( y = (/) -> U. (/) = (/) )
92	89, 91	eqtrd 2505	. . . . . . . . . 10 |- ( y = (/) -> U. y = (/) )
93	92	adantl 473	. . . . . . . . 9 |- ( ( y e. { (/) , { (/) } } /\ y = (/) ) -> U. y = (/) )
94		simpl 464	. . . . . . . . . . 11 |- ( ( y e. { (/) , { (/) } } /\ -. y = (/) ) -> y e. { (/) , { (/) } } )
95	27	adantl 473	. . . . . . . . . . 11 |- ( ( y e. { (/) , { (/) } } /\ -. y = (/) ) -> y =/= (/) )
96		elprn1 37810	. . . . . . . . . . 11 |- ( ( y e. { (/) , { (/) } } /\ y =/= (/) ) -> y = { (/) } )
97	94, 95, 96	syl2anc 673	. . . . . . . . . 10 |- ( ( y e. { (/) , { (/) } } /\ -. y = (/) ) -> y = { (/) } )
98		unieq 4198	. . . . . . . . . . 11 |- ( y = { (/) } -> U. y = U. { (/) } )
99	1	unisn 4205	. . . . . . . . . . . 12 |- U. { (/) } = (/)
100	99	a1i 11	. . . . . . . . . . 11 |- ( y = { (/) } -> U. { (/) } = (/) )
101	98, 100	eqtrd 2505	. . . . . . . . . 10 |- ( y = { (/) } -> U. y = (/) )
102	97, 101	syl 17	. . . . . . . . 9 |- ( ( y e. { (/) , { (/) } } /\ -. y = (/) ) -> U. y = (/) )
103	93, 102	pm2.61dan 808	. . . . . . . 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 2549	. . . . . 6 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ -. X e. y ) -> U. y e. { (/) , X } )
107	56, 106	pm2.61dan 808	. . . . 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 2809	. . 3 |- ( X e. V -> A. y e. ~P { (/) , X } ( y ~<_ om -> U. y e. { (/) , X } ) )
110	3, 42, 109	3jca 1210	. 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 4642	. . . 4 |- { (/) , X } e. _V
112	111	a1i 11	. . 3 |- ( X e. V -> { (/) , X } e. _V )
113		issal 38287	. . 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 240	1 |- ( X e. V -> { (/) , X } e. SAlg )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 376   /\ w3a 1007   = wceq 1452   e. wcel 1904   =/= wne 2641   A.wral 2756   _Vcvv 3031   \ cdif 3387   u. cun 3388   C_ wss 3390   (/)c0 3722   ~Pcpw 3942   {csn 3959   {cpr 3961   U.cuni 4190   class class class wbr 4395   omcom 6711   ~<_ cdom 7585  SAlgcsalg 38281

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-pw 3944  df-sn 3960  df-pr 3962  df-uni 4191  df-salg 38282

This theorem is referenced by: (None)