Theorem prsal 38179

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 4535	. . . . 5 |- (/) e. _V
2	1	prid1 4080	. . . 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 4212	. . . . . . . . 9 |- ( ( (/) e. _V /\ X e. V ) -> U. { (/) , X } = ( (/) u. X ) )
7	4, 5, 6	syl2anc 667	. . . . . . . 8 |- ( X e. V -> U. { (/) , X } = ( (/) u. X ) )
8		uncom 3578	. . . . . . . . . 10 |- ( (/) u. X ) = ( X u. (/) )
9		un0 3759	. . . . . . . . . 10 |- ( X u. (/) ) = X
10	8, 9	eqtri 2473	. . . . . . . . 9 |- ( (/) u. X ) = X
11	10	a1i 11	. . . . . . . 8 |- ( X e. V -> ( (/) u. X ) = X )
12		eqidd 2452	. . . . . . . 8 |- ( X e. V -> X = X )
13	7, 11, 12	3eqtrd 2489	. . . . . . 7 |- ( X e. V -> U. { (/) , X } = X )
14	13	difeq1d 3550	. . . . . 6 |- ( X e. V -> ( U. { (/) , X } \ y ) = ( X \ y ) )
15	14	adantr 467	. . . . 5 |- ( ( X e. V /\ y e. { (/) , X } ) -> ( U. { (/) , X } \ y ) = ( X \ y ) )
16		difeq2 3545	. . . . . . . . . 10 |- ( y = (/) -> ( X \ y ) = ( X \ (/) ) )
17	16	adantl 468	. . . . . . . . 9 |- ( ( X e. V /\ y = (/) ) -> ( X \ y ) = ( X \ (/) ) )
18		dif0 3837	. . . . . . . . . 10 |- ( X \ (/) ) = X
19	18	a1i 11	. . . . . . . . 9 |- ( ( X e. V /\ y = (/) ) -> ( X \ (/) ) = X )
20	17, 19	eqtrd 2485	. . . . . . . 8 |- ( ( X e. V /\ y = (/) ) -> ( X \ y ) = X )
21		prid2g 4079	. . . . . . . . 9 |- ( X e. V -> X e. { (/) , X } )
22	21	adantr 467	. . . . . . . 8 |- ( ( X e. V /\ y = (/) ) -> X e. { (/) , X } )
23	20, 22	eqeltrd 2529	. . . . . . 7 |- ( ( X e. V /\ y = (/) ) -> ( X \ y ) e. { (/) , X } )
24	23	adantlr 721	. . . . . 6 |- ( ( ( X e. V /\ y e. { (/) , X } ) /\ y = (/) ) -> ( X \ y ) e. { (/) , X } )
25		simpll 760	. . . . . . 7 |- ( ( ( X e. V /\ y e. { (/) , X } ) /\ -. y = (/) ) -> X e. V )
26		simpl 459	. . . . . . . . 9 |- ( ( y e. { (/) , X } /\ -. y = (/) ) -> y e. { (/) , X } )
27		neqne 37374	. . . . . . . . . 10 |- ( -. y = (/) -> y =/= (/) )
28	27	adantl 468	. . . . . . . . 9 |- ( ( y e. { (/) , X } /\ -. y = (/) ) -> y =/= (/) )
29		elprn1 37713	. . . . . . . . 9 |- ( ( y e. { (/) , X } /\ y =/= (/) ) -> y = X )
30	26, 28, 29	syl2anc 667	. . . . . . . 8 |- ( ( y e. { (/) , X } /\ -. y = (/) ) -> y = X )
31	30	adantll 720	. . . . . . 7 |- ( ( ( X e. V /\ y e. { (/) , X } ) /\ -. y = (/) ) -> y = X )
32		difeq2 3545	. . . . . . . . . 10 |- ( y = X -> ( X \ y ) = ( X \ X ) )
33		difid 3835	. . . . . . . . . . 11 |- ( X \ X ) = (/)
34	33	a1i 11	. . . . . . . . . 10 |- ( y = X -> ( X \ X ) = (/) )
35	32, 34	eqtrd 2485	. . . . . . . . 9 |- ( y = X -> ( X \ y ) = (/) )
36	2	a1i 11	. . . . . . . . 9 |- ( y = X -> (/) e. { (/) , X } )
37	35, 36	eqeltrd 2529	. . . . . . . 8 |- ( y = X -> ( X \ y ) e. { (/) , X } )
38	37	adantl 468	. . . . . . 7 |- ( ( X e. V /\ y = X ) -> ( X \ y ) e. { (/) , X } )
39	25, 31, 38	syl2anc 667	. . . . . 6 |- ( ( ( X e. V /\ y e. { (/) , X } ) /\ -. y = (/) ) -> ( X \ y ) e. { (/) , X } )
40	24, 39	pm2.61dan 800	. . . . 5 |- ( ( X e. V /\ y e. { (/) , X } ) -> ( X \ y ) e. { (/) , X } )
41	15, 40	eqeltrd 2529	. . . 4 |- ( ( X e. V /\ y e. { (/) , X } ) -> ( U. { (/) , X } \ y ) e. { (/) , X } )
42	41	ralrimiva 2802	. . 3 |- ( X e. V -> A. y e. { (/) , X } ( U. { (/) , X } \ y ) e. { (/) , X } )
43		elpwi 3960	. . . . . . . . . . . . 13 |- ( y e. ~P { (/) , X } -> y C_ { (/) , X } )
44		uniss 4219	. . . . . . . . . . . . 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 468	. . . . . . . . . . 11 |- ( ( X e. V /\ y e. ~P { (/) , X } ) -> U. y C_ U. { (/) , X } )
47	13	adantr 467	. . . . . . . . . . 11 |- ( ( X e. V /\ y e. ~P { (/) , X } ) -> U. { (/) , X } = X )
48	46, 47	sseqtrd 3468	. . . . . . . . . 10 |- ( ( X e. V /\ y e. ~P { (/) , X } ) -> U. y C_ X )
49	48	adantr 467	. . . . . . . . 9 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ X e. y ) -> U. y C_ X )
50		elssuni 4227	. . . . . . . . . 10 |- ( X e. y -> X C_ U. y )
51	50	adantl 468	. . . . . . . . 9 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ X e. y ) -> X C_ U. y )
52	49, 51	jca 535	. . . . . . . 8 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ X e. y ) -> ( U. y C_ X /\ X C_ U. y ) )
53		eqss 3447	. . . . . . . 8 |- ( U. y = X <-> ( U. y C_ X /\ X C_ U. y ) )
54	52, 53	sylibr 216	. . . . . . 7 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ X e. y ) -> U. y = X )
55	21	ad2antrr 732	. . . . . . 7 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ X e. y ) -> X e. { (/) , X } )
56	54, 55	eqeltrd 2529	. . . . . 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 4194	. . . . . . . . . . . 12 |- ~P { (/) , X } = ( { (/) , { (/) } } u. { { X } , { (/) , X } } )
59	57, 58	syl6eleq 2539	. . . . . . . . . . 11 |- ( y e. ~P { (/) , X } -> y e. ( { (/) , { (/) } } u. { { X } , { (/) , X } } ) )
60	59	adantr 467	. . . . . . . . . 10 |- ( ( y e. ~P { (/) , X } /\ -. X e. y ) -> y e. ( { (/) , { (/) } } u. { { X } , { (/) , X } } ) )
61	60	adantll 720	. . . . . . . . 9 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ -. X e. y ) -> y e. ( { (/) , { (/) } } u. { { X } , { (/) , X } } ) )
62		snidg 3994	. . . . . . . . . . . . . . . 16 |- ( X e. V -> X e. { X } )
63	62	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( X e. V /\ y = { X } ) -> X e. { X } )
64		id 22	. . . . . . . . . . . . . . . . 17 |- ( y = { X } -> y = { X } )
65	64	eqcomd 2457	. . . . . . . . . . . . . . . 16 |- ( y = { X } -> { X } = y )
66	65	adantl 468	. . . . . . . . . . . . . . 15 |- ( ( X e. V /\ y = { X } ) -> { X } = y )
67	63, 66	eleqtrd 2531	. . . . . . . . . . . . . 14 |- ( ( X e. V /\ y = { X } ) -> X e. y )
68	67	adantlr 721	. . . . . . . . . . . . 13 |- ( ( ( X e. V /\ y e. { { X } , { (/) , X } } ) /\ y = { X } ) -> X e. y )
69	5	ad2antrr 732	. . . . . . . . . . . . . 14 |- ( ( ( X e. V /\ y e. { { X } , { (/) , X } } ) /\ -. y = { X } ) -> X e. V )
70		simpl 459	. . . . . . . . . . . . . . . 16 |- ( ( y e. { { X } , { (/) , X } } /\ -. y = { X } ) -> y e. { { X } , { (/) , X } } )
71	64	necon3bi 2650	. . . . . . . . . . . . . . . . 17 |- ( -. y = { X } -> y =/= { X } )
72	71	adantl 468	. . . . . . . . . . . . . . . 16 |- ( ( y e. { { X } , { (/) , X } } /\ -. y = { X } ) -> y =/= { X } )
73		elprn1 37713	. . . . . . . . . . . . . . . 16 |- ( ( y e. { { X } , { (/) , X } } /\ y =/= { X } ) -> y = { (/) , X } )
74	70, 72, 73	syl2anc 667	. . . . . . . . . . . . . . 15 |- ( ( y e. { { X } , { (/) , X } } /\ -. y = { X } ) -> y = { (/) , X } )
75	74	adantll 720	. . . . . . . . . . . . . 14 |- ( ( ( X e. V /\ y e. { { X } , { (/) , X } } ) /\ -. y = { X } ) -> y = { (/) , X } )
76	21	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( X e. V /\ y = { (/) , X } ) -> X e. { (/) , X } )
77		id 22	. . . . . . . . . . . . . . . . 17 |- ( y = { (/) , X } -> y = { (/) , X } )
78	77	eqcomd 2457	. . . . . . . . . . . . . . . 16 |- ( y = { (/) , X } -> { (/) , X } = y )
79	78	adantl 468	. . . . . . . . . . . . . . 15 |- ( ( X e. V /\ y = { (/) , X } ) -> { (/) , X } = y )
80	76, 79	eleqtrd 2531	. . . . . . . . . . . . . 14 |- ( ( X e. V /\ y = { (/) , X } ) -> X e. y )
81	69, 75, 80	syl2anc 667	. . . . . . . . . . . . 13 |- ( ( ( X e. V /\ y e. { { X } , { (/) , X } } ) /\ -. y = { X } ) -> X e. y )
82	68, 81	pm2.61dan 800	. . . . . . . . . . . 12 |- ( ( X e. V /\ y e. { { X } , { (/) , X } } ) -> X e. y )
83	82	adantlr 721	. . . . . . . . . . 11 |- ( ( ( X e. V /\ -. X e. y ) /\ y e. { { X } , { (/) , X } } ) -> X e. y )
84		simplr 762	. . . . . . . . . . 11 |- ( ( ( X e. V /\ -. X e. y ) /\ y e. { { X } , { (/) , X } } ) -> -. X e. y )
85	83, 84	pm2.65da 580	. . . . . . . . . 10 |- ( ( X e. V /\ -. X e. y ) -> -. y e. { { X } , { (/) , X } } )
86	85	adantlr 721	. . . . . . . . 9 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ -. X e. y ) -> -. y e. { { X } , { (/) , X } } )
87		elunnel2 37360	. . . . . . . . 9 |- ( ( y e. ( { (/) , { (/) } } u. { { X } , { (/) , X } } ) /\ -. y e. { { X } , { (/) , X } } ) -> y e. { (/) , { (/) } } )
88	61, 86, 87	syl2anc 667	. . . . . . . 8 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ -. X e. y ) -> y e. { (/) , { (/) } } )
89		unieq 4206	. . . . . . . . . . 11 |- ( y = (/) -> U. y = U. (/) )
90		uni0 4225	. . . . . . . . . . . 12 |- U. (/) = (/)
91	90	a1i 11	. . . . . . . . . . 11 |- ( y = (/) -> U. (/) = (/) )
92	89, 91	eqtrd 2485	. . . . . . . . . 10 |- ( y = (/) -> U. y = (/) )
93	92	adantl 468	. . . . . . . . 9 |- ( ( y e. { (/) , { (/) } } /\ y = (/) ) -> U. y = (/) )
94		simpl 459	. . . . . . . . . . 11 |- ( ( y e. { (/) , { (/) } } /\ -. y = (/) ) -> y e. { (/) , { (/) } } )
95	27	adantl 468	. . . . . . . . . . 11 |- ( ( y e. { (/) , { (/) } } /\ -. y = (/) ) -> y =/= (/) )
96		elprn1 37713	. . . . . . . . . . 11 |- ( ( y e. { (/) , { (/) } } /\ y =/= (/) ) -> y = { (/) } )
97	94, 95, 96	syl2anc 667	. . . . . . . . . 10 |- ( ( y e. { (/) , { (/) } } /\ -. y = (/) ) -> y = { (/) } )
98		unieq 4206	. . . . . . . . . . 11 |- ( y = { (/) } -> U. y = U. { (/) } )
99	1	unisn 4213	. . . . . . . . . . . 12 |- U. { (/) } = (/)
100	99	a1i 11	. . . . . . . . . . 11 |- ( y = { (/) } -> U. { (/) } = (/) )
101	98, 100	eqtrd 2485	. . . . . . . . . 10 |- ( y = { (/) } -> U. y = (/) )
102	97, 101	syl 17	. . . . . . . . 9 |- ( ( y e. { (/) , { (/) } } /\ -. y = (/) ) -> U. y = (/) )
103	93, 102	pm2.61dan 800	. . . . . . . 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 2529	. . . . . 6 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ -. X e. y ) -> U. y e. { (/) , X } )
107	56, 106	pm2.61dan 800	. . . . 5 |- ( ( X e. V /\ y e. ~P { (/) , X } ) -> U. y e. { (/) , X } )
108	107	a1d 26	. . . 4 |- ( ( X e. V /\ y e. ~P { (/) , X } ) -> ( y ~<_ om -> U. y e. { (/) , X } ) )
109	108	ralrimiva 2802	. . 3 |- ( X e. V -> A. y e. ~P { (/) , X } ( y ~<_ om -> U. y e. { (/) , X } ) )
110	3, 42, 109	3jca 1188	. 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 38175	. . 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 236	1 |- ( X e. V -> { (/) , X } e. SAlg )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   /\ wa 371   /\ w3a 985   = wceq 1444   e. wcel 1887   =/= wne 2622   A.wral 2737   _Vcvv 3045   \ cdif 3401   u. cun 3402   C_ wss 3404   (/)c0 3731   ~Pcpw 3951   {csn 3968   {cpr 3970   U.cuni 4198   class class class wbr 4402   omcom 6692   ~<_ cdom 7567  SAlgcsalg 38169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pr 4639

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-pw 3953  df-sn 3969  df-pr 3971  df-uni 4199  df-salg 38170

This theorem is referenced by: (None)