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 \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall x \in s O ∖ x \in s \land \forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in s))\}$
	ldsysgenld.1	$⊢ φ \to O \in V$
	ldsysgenld.2	$⊢ φ \to A \subseteq 𝒫 O$
Assertion	ldsysgenld	$⊢ φ \to ⋂ \{t \in L \| A \subseteq t\} \in L$

Proof

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

Metamath Proof Explorer

Theorem ldsysgenld

Proof