Theorem prsal 38024

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 4554	. . . . 5 |- (/) e. _V
2	1	prid1 4106	. . . 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 23	. . . . . . . . 9 |- ( X e. V -> X e. V )
6		uniprg 4231	. . . . . . . . 9 |- ( ( (/) e. _V /\ X e. V ) -> U. { (/) , X } = ( (/) u. X ) )
7	4, 5, 6	syl2anc 666	. . . . . . . 8 |- ( X e. V -> U. { (/) , X } = ( (/) u. X ) )
8		uncom 3611	. . . . . . . . . 10 |- ( (/) u. X ) = ( X u. (/) )
9		un0 3788	. . . . . . . . . 10 |- ( X u. (/) ) = X
10	8, 9	eqtri 2452	. . . . . . . . 9 |- ( (/) u. X ) = X
11	10	a1i 11	. . . . . . . 8 |- ( X e. V -> ( (/) u. X ) = X )
12		eqidd 2424	. . . . . . . 8 |- ( X e. V -> X = X )
13	7, 11, 12	3eqtrd 2468	. . . . . . 7 |- ( X e. V -> U. { (/) , X } = X )
14	13	difeq1d 3583	. . . . . 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 3578	. . . . . . . . . 10 |- ( y = (/) -> ( X \ y ) = ( X \ (/) ) )
17	16	adantl 468	. . . . . . . . 9 |- ( ( X e. V /\ y = (/) ) -> ( X \ y ) = ( X \ (/) ) )
18		dif0 3866	. . . . . . . . . 10 |- ( X \ (/) ) = X
19	18	a1i 11	. . . . . . . . 9 |- ( ( X e. V /\ y = (/) ) -> ( X \ (/) ) = X )
20	17, 19	eqtrd 2464	. . . . . . . 8 |- ( ( X e. V /\ y = (/) ) -> ( X \ y ) = X )
21		prid2g 4105	. . . . . . . . 9 |- ( X e. V -> X e. { (/) , X } )
22	21	adantr 467	. . . . . . . 8 |- ( ( X e. V /\ y = (/) ) -> X e. { (/) , X } )
23	20, 22	eqeltrd 2511	. . . . . . 7 |- ( ( X e. V /\ y = (/) ) -> ( X \ y ) e. { (/) , X } )
24	23	adantlr 720	. . . . . 6 |- ( ( ( X e. V /\ y e. { (/) , X } ) /\ y = (/) ) -> ( X \ y ) e. { (/) , X } )
25		simpll 759	. . . . . . 7 |- ( ( ( X e. V /\ y e. { (/) , X } ) /\ -. y = (/) ) -> X e. V )
26		simpl 459	. . . . . . . . 9 |- ( ( y e. { (/) , X } /\ -. y = (/) ) -> y e. { (/) , X } )
27		neqne 37279	. . . . . . . . . 10 |- ( -. y = (/) -> y =/= (/) )
28	27	adantl 468	. . . . . . . . 9 |- ( ( y e. { (/) , X } /\ -. y = (/) ) -> y =/= (/) )
29		elprn1 37577	. . . . . . . . 9 |- ( ( y e. { (/) , X } /\ y =/= (/) ) -> y = X )
30	26, 28, 29	syl2anc 666	. . . . . . . 8 |- ( ( y e. { (/) , X } /\ -. y = (/) ) -> y = X )
31	30	adantll 719	. . . . . . 7 |- ( ( ( X e. V /\ y e. { (/) , X } ) /\ -. y = (/) ) -> y = X )
32		difeq2 3578	. . . . . . . . . 10 |- ( y = X -> ( X \ y ) = ( X \ X ) )
33		difid 3864	. . . . . . . . . . 11 |- ( X \ X ) = (/)
34	33	a1i 11	. . . . . . . . . 10 |- ( y = X -> ( X \ X ) = (/) )
35	32, 34	eqtrd 2464	. . . . . . . . 9 |- ( y = X -> ( X \ y ) = (/) )
36	2	a1i 11	. . . . . . . . 9 |- ( y = X -> (/) e. { (/) , X } )
37	35, 36	eqeltrd 2511	. . . . . . . 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 666	. . . . . 6 |- ( ( ( X e. V /\ y e. { (/) , X } ) /\ -. y = (/) ) -> ( X \ y ) e. { (/) , X } )
40	24, 39	pm2.61dan 799	. . . . 5 |- ( ( X e. V /\ y e. { (/) , X } ) -> ( X \ y ) e. { (/) , X } )
41	15, 40	eqeltrd 2511	. . . 4 |- ( ( X e. V /\ y e. { (/) , X } ) -> ( U. { (/) , X } \ y ) e. { (/) , X } )
42	41	ralrimiva 2840	. . 3 |- ( X e. V -> A. y e. { (/) , X } ( U. { (/) , X } \ y ) e. { (/) , X } )
43		elpwi 3989	. . . . . . . . . . . . 13 |- ( y e. ~P { (/) , X } -> y C_ { (/) , X } )
44		uniss 4238	. . . . . . . . . . . . 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 3501	. . . . . . . . . 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 4246	. . . . . . . . . 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 3480	. . . . . . . 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 731	. . . . . . 7 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ X e. y ) -> X e. { (/) , X } )
56	54, 55	eqeltrd 2511	. . . . . 6 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ X e. y ) -> U. y e. { (/) , X } )
57		id 23	. . . . . . . . . . . 12 |- ( y e. ~P { (/) , X } -> y e. ~P { (/) , X } )
58		pwpr 4213	. . . . . . . . . . . 12 |- ~P { (/) , X } = ( { (/) , { (/) } } u. { { X } , { (/) , X } } )
59	57, 58	syl6eleq 2521	. . . . . . . . . . 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 719	. . . . . . . . 9 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ -. X e. y ) -> y e. ( { (/) , { (/) } } u. { { X } , { (/) , X } } ) )
62		snidg 4023	. . . . . . . . . . . . . . . 16 |- ( X e. V -> X e. { X } )
63	62	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( X e. V /\ y = { X } ) -> X e. { X } )
64		id 23	. . . . . . . . . . . . . . . . 17 |- ( y = { X } -> y = { X } )
65	64	eqcomd 2431	. . . . . . . . . . . . . . . 16 |- ( y = { X } -> { X } = y )
66	65	adantl 468	. . . . . . . . . . . . . . 15 |- ( ( X e. V /\ y = { X } ) -> { X } = y )
67	63, 66	eleqtrd 2513	. . . . . . . . . . . . . 14 |- ( ( X e. V /\ y = { X } ) -> X e. y )
68	67	adantlr 720	. . . . . . . . . . . . 13 |- ( ( ( X e. V /\ y e. { { X } , { (/) , X } } ) /\ y = { X } ) -> X e. y )
69	5	ad2antrr 731	. . . . . . . . . . . . . 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 2654	. . . . . . . . . . . . . . . . 17 |- ( -. y = { X } -> y =/= { X } )
72	71	adantl 468	. . . . . . . . . . . . . . . 16 |- ( ( y e. { { X } , { (/) , X } } /\ -. y = { X } ) -> y =/= { X } )
73		elprn1 37577	. . . . . . . . . . . . . . . 16 |- ( ( y e. { { X } , { (/) , X } } /\ y =/= { X } ) -> y = { (/) , X } )
74	70, 72, 73	syl2anc 666	. . . . . . . . . . . . . . 15 |- ( ( y e. { { X } , { (/) , X } } /\ -. y = { X } ) -> y = { (/) , X } )
75	74	adantll 719	. . . . . . . . . . . . . 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 23	. . . . . . . . . . . . . . . . 17 |- ( y = { (/) , X } -> y = { (/) , X } )
78	77	eqcomd 2431	. . . . . . . . . . . . . . . 16 |- ( y = { (/) , X } -> { (/) , X } = y )
79	78	adantl 468	. . . . . . . . . . . . . . 15 |- ( ( X e. V /\ y = { (/) , X } ) -> { (/) , X } = y )
80	76, 79	eleqtrd 2513	. . . . . . . . . . . . . 14 |- ( ( X e. V /\ y = { (/) , X } ) -> X e. y )
81	69, 75, 80	syl2anc 666	. . . . . . . . . . . . 13 |- ( ( ( X e. V /\ y e. { { X } , { (/) , X } } ) /\ -. y = { X } ) -> X e. y )
82	68, 81	pm2.61dan 799	. . . . . . . . . . . 12 |- ( ( X e. V /\ y e. { { X } , { (/) , X } } ) -> X e. y )
83	82	adantlr 720	. . . . . . . . . . 11 |- ( ( ( X e. V /\ -. X e. y ) /\ y e. { { X } , { (/) , X } } ) -> X e. y )
84		simplr 761	. . . . . . . . . . 11 |- ( ( ( X e. V /\ -. X e. y ) /\ y e. { { X } , { (/) , X } } ) -> -. X e. y )
85	83, 84	pm2.65da 579	. . . . . . . . . 10 |- ( ( X e. V /\ -. X e. y ) -> -. y e. { { X } , { (/) , X } } )
86	85	adantlr 720	. . . . . . . . 9 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ -. X e. y ) -> -. y e. { { X } , { (/) , X } } )
87		elunnel2 37265	. . . . . . . . 9 |- ( ( y e. ( { (/) , { (/) } } u. { { X } , { (/) , X } } ) /\ -. y e. { { X } , { (/) , X } } ) -> y e. { (/) , { (/) } } )
88	61, 86, 87	syl2anc 666	. . . . . . . 8 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ -. X e. y ) -> y e. { (/) , { (/) } } )
89		unieq 4225	. . . . . . . . . . 11 |- ( y = (/) -> U. y = U. (/) )
90		uni0 4244	. . . . . . . . . . . 12 |- U. (/) = (/)
91	90	a1i 11	. . . . . . . . . . 11 |- ( y = (/) -> U. (/) = (/) )
92	89, 91	eqtrd 2464	. . . . . . . . . 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 37577	. . . . . . . . . . 11 |- ( ( y e. { (/) , { (/) } } /\ y =/= (/) ) -> y = { (/) } )
97	94, 95, 96	syl2anc 666	. . . . . . . . . 10 |- ( ( y e. { (/) , { (/) } } /\ -. y = (/) ) -> y = { (/) } )
98		unieq 4225	. . . . . . . . . . 11 |- ( y = { (/) } -> U. y = U. { (/) } )
99	1	unisn 4232	. . . . . . . . . . . 12 |- U. { (/) } = (/)
100	99	a1i 11	. . . . . . . . . . 11 |- ( y = { (/) } -> U. { (/) } = (/) )
101	98, 100	eqtrd 2464	. . . . . . . . . 10 |- ( y = { (/) } -> U. y = (/) )
102	97, 101	syl 17	. . . . . . . . 9 |- ( ( y e. { (/) , { (/) } } /\ -. y = (/) ) -> U. y = (/) )
103	93, 102	pm2.61dan 799	. . . . . . . 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 2511	. . . . . 6 |- ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ -. X e. y ) -> U. y e. { (/) , X } )
107	56, 106	pm2.61dan 799	. . . . 5 |- ( ( X e. V /\ y e. ~P { (/) , X } ) -> U. y e. { (/) , X } )
108	107	a1d 27	. . . 4 |- ( ( X e. V /\ y e. ~P { (/) , X } ) -> ( y ~<_ om -> U. y e. { (/) , X } ) )
109	108	ralrimiva 2840	. . 3 |- ( X e. V -> A. y e. ~P { (/) , X } ( y ~<_ om -> U. y e. { (/) , X } ) )
110	3, 42, 109	3jca 1186	. 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 4661	. . . 4 |- { (/) , X } e. _V
112	111	a1i 11	. . 3 |- ( X e. V -> { (/) , X } e. _V )
113		issal 38020	. . 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 983   = wceq 1438   e. wcel 1869   =/= wne 2619   A.wral 2776   _Vcvv 3082   \ cdif 3434   u. cun 3435   C_ wss 3437   (/)c0 3762   ~Pcpw 3980   {csn 3997   {cpr 3999   U.cuni 4217   class class class wbr 4421   omcom 6704   ~<_ cdom 7573  SAlgcsalg 38014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-pw 3982  df-sn 3998  df-pr 4000  df-uni 4218  df-salg 38015

This theorem is referenced by: (None)