Theorem ldsysgenld

Description: The intersection of all lambda-systems containing a given collection of sets A , which is called the lambda-system generated by A , is itself also a lambda-system. (Contributed by Thierry Arnoux, 16-Jun-2020)

	Ref	Expression
Hypotheses	isldsys.l	|- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. s ) ) }
	ldsysgenld.1	|- ( ph -> O e. V )
	ldsysgenld.2	|- ( ph -> A C_ ~P O )
Assertion	ldsysgenld	|- ( ph -> |^| { t e. L | A C_ t } e. L )

Proof

Step	Hyp	Ref	Expression
1		isldsys.l	|- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. s ) ) }
2		ldsysgenld.1	|- ( ph -> O e. V )
3		ldsysgenld.2	|- ( ph -> A C_ ~P O )
4		pwsiga	|- ( O e. V -> ~P O e. ( sigAlgebra ` O ) )
5	2 4	syl	|- ( ph -> ~P O e. ( sigAlgebra ` O ) )
6	1	sigaldsys	|- ( sigAlgebra ` O ) C_ L
7	6 5	sselid	|- ( ph -> ~P O e. L )
8		sseq2	|- ( t = ~P O -> ( A C_ t <-> A C_ ~P O ) )
9	8	elrab	|- ( ~P O e. { t e. L | A C_ t } <-> ( ~P O e. L /\ A C_ ~P O ) )
10	7 3 9	sylanbrc	|- ( ph -> ~P O e. { t e. L | A C_ t } )
11		intss1	|- ( ~P O e. { t e. L | A C_ t } -> |^| { t e. L | A C_ t } C_ ~P O )
12	10 11	syl	|- ( ph -> |^| { t e. L | A C_ t } C_ ~P O )
13	5 12	sselpwd	|- ( ph -> |^| { t e. L | A C_ t } e. ~P ~P O )
14	1	isldsys	|- ( t e. L <-> ( t e. ~P ~P O /\ ( (/) e. t /\ A. x e. t ( O \ x ) e. t /\ A. x e. ~P t ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) ) ) )
15	14	simprbi	|- ( t e. L -> ( (/) e. t /\ A. x e. t ( O \ x ) e. t /\ A. x e. ~P t ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) ) )
16	15	simp1d	|- ( t e. L -> (/) e. t )
17	16	adantl	|- ( ( ph /\ t e. L ) -> (/) e. t )
18	17	a1d	|- ( ( ph /\ t e. L ) -> ( A C_ t -> (/) e. t ) )
19	18	ralrimiva	|- ( ph -> A. t e. L ( A C_ t -> (/) e. t ) )
20		0ex	|- (/) e. _V
21	20	elintrab	|- ( (/) e. |^| { t e. L | A C_ t } <-> A. t e. L ( A C_ t -> (/) e. t ) )
22	19 21	sylibr	|- ( ph -> (/) e. |^| { t e. L | A C_ t } )
23		nfv	|- F/ t ph
24		nfcv	|- F/_ t x
25		nfrab1	|- F/_ t { t e. L | A C_ t }
26	25	nfint	|- F/_ t |^| { t e. L | A C_ t }
27	24 26	nfel	|- F/ t x e. |^| { t e. L | A C_ t }
28	23 27	nfan	|- F/ t ( ph /\ x e. |^| { t e. L | A C_ t } )
29		simplr	|- ( ( ( ( ph /\ x e. |^| { t e. L | A C_ t } ) /\ t e. L ) /\ A C_ t ) -> t e. L )
30		vex	|- x e. _V
31	30	elintrab	|- ( x e. |^| { t e. L | A C_ t } <-> A. t e. L ( A C_ t -> x e. t ) )
32	31	biimpi	|- ( x e. |^| { t e. L | A C_ t } -> A. t e. L ( A C_ t -> x e. t ) )
33	32	adantl	|- ( ( ph /\ x e. |^| { t e. L | A C_ t } ) -> A. t e. L ( A C_ t -> x e. t ) )
34	33	r19.21bi	|- ( ( ( ph /\ x e. |^| { t e. L | A C_ t } ) /\ t e. L ) -> ( A C_ t -> x e. t ) )
35	34	imp	|- ( ( ( ( ph /\ x e. |^| { t e. L | A C_ t } ) /\ t e. L ) /\ A C_ t ) -> x e. t )
36	15	simp2d	|- ( t e. L -> A. x e. t ( O \ x ) e. t )
37	36	r19.21bi	|- ( ( t e. L /\ x e. t ) -> ( O \ x ) e. t )
38	29 35 37	syl2anc	|- ( ( ( ( ph /\ x e. |^| { t e. L | A C_ t } ) /\ t e. L ) /\ A C_ t ) -> ( O \ x ) e. t )
39	38	ex	|- ( ( ( ph /\ x e. |^| { t e. L | A C_ t } ) /\ t e. L ) -> ( A C_ t -> ( O \ x ) e. t ) )
40	39	ex	|- ( ( ph /\ x e. |^| { t e. L | A C_ t } ) -> ( t e. L -> ( A C_ t -> ( O \ x ) e. t ) ) )
41	28 40	ralrimi	|- ( ( ph /\ x e. |^| { t e. L | A C_ t } ) -> A. t e. L ( A C_ t -> ( O \ x ) e. t ) )
42		difexg	|- ( O e. V -> ( O \ x ) e. _V )
43		elintrabg	|- ( ( O \ x ) e. _V -> ( ( O \ x ) e. |^| { t e. L | A C_ t } <-> A. t e. L ( A C_ t -> ( O \ x ) e. t ) ) )
44	2 42 43	3syl	|- ( ph -> ( ( O \ x ) e. |^| { t e. L | A C_ t } <-> A. t e. L ( A C_ t -> ( O \ x ) e. t ) ) )
45	44	adantr	|- ( ( ph /\ x e. |^| { t e. L | A C_ t } ) -> ( ( O \ x ) e. |^| { t e. L | A C_ t } <-> A. t e. L ( A C_ t -> ( O \ x ) e. t ) ) )
46	41 45	mpbird	|- ( ( ph /\ x e. |^| { t e. L | A C_ t } ) -> ( O \ x ) e. |^| { t e. L | A C_ t } )
47	46	ralrimiva	|- ( ph -> A. x e. |^| { t e. L | A C_ t } ( O \ x ) e. |^| { t e. L | A C_ t } )
48	26	nfpw	|- F/_ t ~P |^| { t e. L | A C_ t }
49	24 48	nfel	|- F/ t x e. ~P |^| { t e. L | A C_ t }
50	23 49	nfan	|- F/ t ( ph /\ x e. ~P |^| { t e. L | A C_ t } )
51		nfv	|- F/ t ( x ~<_ _om /\ Disj_ y e. x y )
52	50 51	nfan	|- F/ t ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) )
53		simplr	|- ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) -> t e. L )
54		simpr	|- ( ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) /\ u e. |^| { t e. L | A C_ t } ) -> u e. |^| { t e. L | A C_ t } )
55		simpllr	|- ( ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) /\ u e. |^| { t e. L | A C_ t } ) -> t e. L )
56		simplr	|- ( ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) /\ u e. |^| { t e. L | A C_ t } ) -> A C_ t )
57		vex	|- u e. _V
58	57	elintrab	|- ( u e. |^| { t e. L | A C_ t } <-> A. t e. L ( A C_ t -> u e. t ) )
59	58	biimpi	|- ( u e. |^| { t e. L | A C_ t } -> A. t e. L ( A C_ t -> u e. t ) )
60	59	r19.21bi	|- ( ( u e. |^| { t e. L | A C_ t } /\ t e. L ) -> ( A C_ t -> u e. t ) )
61	60	imp	|- ( ( ( u e. |^| { t e. L | A C_ t } /\ t e. L ) /\ A C_ t ) -> u e. t )
62	54 55 56 61	syl21anc	|- ( ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) /\ u e. |^| { t e. L | A C_ t } ) -> u e. t )
63	62	ex	|- ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) -> ( u e. |^| { t e. L | A C_ t } -> u e. t ) )
64	63	ssrdv	|- ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) -> |^| { t e. L | A C_ t } C_ t )
65	64	sspwd	|- ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) -> ~P |^| { t e. L | A C_ t } C_ ~P t )
66		simp-4r	|- ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) -> x e. ~P |^| { t e. L | A C_ t } )
67	65 66	sseldd	|- ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) -> x e. ~P t )
68		simpllr	|- ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) -> ( x ~<_ _om /\ Disj_ y e. x y ) )
69	15	simp3d	|- ( t e. L -> A. x e. ~P t ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) )
70	69	r19.21bi	|- ( ( t e. L /\ x e. ~P t ) -> ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) )
71	70	imp	|- ( ( ( t e. L /\ x e. ~P t ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> U. x e. t )
72	53 67 68 71	syl21anc	|- ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) -> U. x e. t )
73	72	ex	|- ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) -> ( A C_ t -> U. x e. t ) )
74	73	ex	|- ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( t e. L -> ( A C_ t -> U. x e. t ) ) )
75	52 74	ralrimi	|- ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> A. t e. L ( A C_ t -> U. x e. t ) )
76		vuniex	|- U. x e. _V
77	76	elintrab	|- ( U. x e. |^| { t e. L | A C_ t } <-> A. t e. L ( A C_ t -> U. x e. t ) )
78	75 77	sylibr	|- ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> U. x e. |^| { t e. L | A C_ t } )
79	78	ex	|- ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) -> ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. |^| { t e. L | A C_ t } ) )
80	79	ralrimiva	|- ( ph -> A. x e. ~P |^| { t e. L | A C_ t } ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. |^| { t e. L | A C_ t } ) )
81	22 47 80	3jca	|- ( ph -> ( (/) e. |^| { t e. L | A C_ t } /\ A. x e. |^| { t e. L | A C_ t } ( O \ x ) e. |^| { t e. L | A C_ t } /\ A. x e. ~P |^| { t e. L | A C_ t } ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. |^| { t e. L | A C_ t } ) ) )
82	13 81	jca	|- ( ph -> ( |^| { t e. L | A C_ t } e. ~P ~P O /\ ( (/) e. |^| { t e. L | A C_ t } /\ A. x e. |^| { t e. L | A C_ t } ( O \ x ) e. |^| { t e. L | A C_ t } /\ A. x e. ~P |^| { t e. L | A C_ t } ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. |^| { t e. L | A C_ t } ) ) ) )
83	1	isldsys	|- ( |^| { t e. L | A C_ t } e. L <-> ( |^| { t e. L | A C_ t } e. ~P ~P O /\ ( (/) e. |^| { t e. L | A C_ t } /\ A. x e. |^| { t e. L | A C_ t } ( O \ x ) e. |^| { t e. L | A C_ t } /\ A. x e. ~P |^| { t e. L | A C_ t } ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. |^| { t e. L | A C_ t } ) ) ) )
84	82 83	sylibr	|- ( ph -> |^| { t e. L | A C_ t } e. L )