sigapildsys

Description: Sigma-algebra are exactly classes which are both lambda and pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020)

	Ref	Expression
Hypotheses	dynkin.p	$⊢ P = \{s \in 𝒫 𝒫 O \| fi (s) \subseteq s\}$
	dynkin.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))\}$
Assertion	sigapildsys	$⊢ sigAlgebra (O) = P \cap L$

Proof

Step	Hyp	Ref	Expression
1		dynkin.p	$⊢ P = \{s \in 𝒫 𝒫 O \| fi (s) \subseteq s\}$
2		dynkin.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))\}$
3	1	sigapisys	$⊢ sigAlgebra (O) \subseteq P$
4	2	sigaldsys	$⊢ sigAlgebra (O) \subseteq L$
5	3 4	ssini	$⊢ sigAlgebra (O) \subseteq P \cap L$
6		id	$⊢ t \in (P \cap L) \to t \in (P \cap L)$
7	6	elin1d	$⊢ t \in (P \cap L) \to t \in P$
8	1	ispisys	$⊢ t \in P \leftrightarrow (t \in 𝒫 𝒫 O \land fi (t) \subseteq t)$
9	7 8	sylib	$⊢ t \in (P \cap L) \to (t \in 𝒫 𝒫 O \land fi (t) \subseteq t)$
10	9	simpld	$⊢ t \in (P \cap L) \to t \in 𝒫 𝒫 O$
11	10	elpwid	$⊢ t \in (P \cap L) \to t \subseteq 𝒫 O$
12		dif0	$⊢ O ∖ \emptyset = O$
13	6	elin2d	$⊢ t \in (P \cap L) \to t \in L$
14	2	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	13 14	sylib	$⊢ t \in (P \cap L) \to (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)))$
16	15	simprd	$⊢ t \in (P \cap 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))$
17	16	simp2d	$⊢ t \in (P \cap L) \to \forall x \in t O ∖ x \in t$
18	16	simp1d	$⊢ t \in (P \cap L) \to \emptyset \in t$
19		difeq2	$⊢ x = \emptyset \to O ∖ x = O ∖ \emptyset$
20		eqidd	$⊢ x = \emptyset \to t = t$
21	19 20	eleq12d	$⊢ x = \emptyset \to (O ∖ x \in t \leftrightarrow O ∖ \emptyset \in t)$
22	21	rspcv	$⊢ \emptyset \in t \to (\forall x \in t O ∖ x \in t \to O ∖ \emptyset \in t)$
23	18 22	syl	$⊢ t \in (P \cap L) \to (\forall x \in t O ∖ x \in t \to O ∖ \emptyset \in t)$
24	17 23	mpd	$⊢ t \in (P \cap L) \to O ∖ \emptyset \in t$
25	12 24	eqeltrrid	$⊢ t \in (P \cap L) \to O \in t$
26		unieq	$⊢ x = \emptyset \to ⋃ x = ⋃ \emptyset$
27		uni0	$⊢ ⋃ \emptyset = \emptyset$
28	26 27	eqtrdi	$⊢ x = \emptyset \to ⋃ x = \emptyset$
29	28	adantl	$⊢ (((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x = \emptyset) \to ⋃ x = \emptyset$
30	18	ad3antrrr	$⊢ (((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x = \emptyset) \to \emptyset \in t$
31	29 30	eqeltrd	$⊢ (((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x = \emptyset) \to ⋃ x \in t$
32		vex	$⊢ x \in V$
33	32	0sdom	$⊢ \emptyset ≺ x \leftrightarrow x \neq \emptyset$
34	33	biimpri	$⊢ x \neq \emptyset \to \emptyset ≺ x$
35	34	adantl	$⊢ (((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \to \emptyset ≺ x$
36		simplr	$⊢ (((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \to x ≼ ω$
37		nnenom	$⊢ ℕ \approx ω$
38	37	ensymi	$⊢ ω \approx ℕ$
39		domentr	$⊢ (x ≼ ω \land ω \approx ℕ) \to x ≼ ℕ$
40	36 38 39	sylancl	$⊢ (((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \to x ≼ ℕ$
41		fodomr	$⊢ (\emptyset ≺ x \land x ≼ ℕ) \to \exists f f : ℕ \underset{onto}{⟶} x$
42	35 40 41	syl2anc	$⊢ (((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \to \exists f f : ℕ \underset{onto}{⟶} x$
43		fveq2	$⊢ n = i \to f (n) = f (i)$
44	43	iundisj	$⊢ ⋃_{n \in ℕ} f (n) = ⋃_{n \in ℕ} (f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
45		fofn	$⊢ f : ℕ \underset{onto}{⟶} x \to f Fn ℕ$
46		fniunfv	$⊢ f Fn ℕ \to ⋃_{n \in ℕ} f (n) = ⋃ ran f$
47	45 46	syl	$⊢ f : ℕ \underset{onto}{⟶} x \to ⋃_{n \in ℕ} f (n) = ⋃ ran f$
48		forn	$⊢ f : ℕ \underset{onto}{⟶} x \to ran f = x$
49	48	unieqd	$⊢ f : ℕ \underset{onto}{⟶} x \to ⋃ ran f = ⋃ x$
50	47 49	eqtrd	$⊢ f : ℕ \underset{onto}{⟶} x \to ⋃_{n \in ℕ} f (n) = ⋃ x$
51	44 50	syl5eqr	$⊢ f : ℕ \underset{onto}{⟶} x \to ⋃_{n \in ℕ} (f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) = ⋃ x$
52	51	adantl	$⊢ ((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \to ⋃_{n \in ℕ} (f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) = ⋃ x$
53		fvex	$⊢ f (n) \in V$
54		difexg	$⊢ f (n) \in V \to f (n) ∖ ⋃_{i \in (1 ..^n)} f (i) \in V$
55	53 54	ax-mp	$⊢ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i) \in V$
56	55	dfiun3	$⊢ ⋃_{n \in ℕ} (f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) = ⋃ ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
57		nfv	$⊢ Ⅎ n ((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x)$
58		nfcv	$⊢ \underline{Ⅎ} n y$
59		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
60	59	nfrn	$⊢ \underline{Ⅎ} n ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
61	58 60	nfel	$⊢ Ⅎ n y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
62	57 61	nfan	$⊢ Ⅎ n (((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)))$
63		simpr	$⊢ (((((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \land n \in ℕ) \land y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \to y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)$
64		nfv	$⊢ Ⅎ i ((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x)$
65		nfcv	$⊢ \underline{Ⅎ} i y$
66		nfcv	$⊢ \underline{Ⅎ} i ℕ$
67		nfcv	$⊢ \underline{Ⅎ} i f (n)$
68		nfiu1	$⊢ \underline{Ⅎ} i ⋃_{i \in (1 ..^n)} f (i)$
69	67 68	nfdif	$⊢ \underline{Ⅎ} i (f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
70	66 69	nfmpt	$⊢ \underline{Ⅎ} i (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
71	70	nfrn	$⊢ \underline{Ⅎ} i ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
72	65 71	nfel	$⊢ Ⅎ i y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
73	64 72	nfan	$⊢ Ⅎ i (((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)))$
74		nfv	$⊢ Ⅎ i n \in ℕ$
75	73 74	nfan	$⊢ Ⅎ i ((((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \land n \in ℕ)$
76	65 69	nfeq	$⊢ Ⅎ i y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)$
77	75 76	nfan	$⊢ Ⅎ i (((((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \land n \in ℕ) \land y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
78	6	ad7antr	$⊢ (((((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \land n \in ℕ) \land y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \to t \in (P \cap L)$
79		simp-4r	$⊢ ((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \to x \in 𝒫 t$
80	79	ad3antrrr	$⊢ (((((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \land n \in ℕ) \land y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \to x \in 𝒫 t$
81	80	elpwid	$⊢ (((((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \land n \in ℕ) \land y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \to x \subseteq t$
82		fof	$⊢ f : ℕ \underset{onto}{⟶} x \to f : ℕ ⟶ x$
83	82	ad4antlr	$⊢ (((((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \land n \in ℕ) \land y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \to f : ℕ ⟶ x$
84		simplr	$⊢ (((((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \land n \in ℕ) \land y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \to n \in ℕ$
85	83 84	ffvelrnd	$⊢ (((((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \land n \in ℕ) \land y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \to f (n) \in x$
86	81 85	sseldd	$⊢ (((((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \land n \in ℕ) \land y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \to f (n) \in t$
87		fzofi	$⊢ (1 ..^n) \in Fin$
88	87	a1i	$⊢ (((((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \land n \in ℕ) \land y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \to (1 ..^n) \in Fin$
89	81	adantr	$⊢ ((((((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \land n \in ℕ) \land y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \land i \in (1 ..^n)) \to x \subseteq t$
90	83	adantr	$⊢ ((((((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \land n \in ℕ) \land y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \land i \in (1 ..^n)) \to f : ℕ ⟶ x$
91		fzossnn	$⊢ (1 ..^n) \subseteq ℕ$
92	91	a1i	$⊢ (((((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \land n \in ℕ) \land y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \to (1 ..^n) \subseteq ℕ$
93	92	sselda	$⊢ ((((((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \land n \in ℕ) \land y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \land i \in (1 ..^n)) \to i \in ℕ$
94	90 93	ffvelrnd	$⊢ ((((((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \land n \in ℕ) \land y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \land i \in (1 ..^n)) \to f (i) \in x$
95	89 94	sseldd	$⊢ ((((((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \land n \in ℕ) \land y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \land i \in (1 ..^n)) \to f (i) \in t$
96	1 2 77 78 86 88 95	sigapildsyslem	$⊢ (((((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \land n \in ℕ) \land y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \to f (n) ∖ ⋃_{i \in (1 ..^n)} f (i) \in t$
97	63 96	eqeltrd	$⊢ (((((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \land n \in ℕ) \land y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \to y \in t$
98		simpr	$⊢ (((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \to y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
99		eqid	$⊢ (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) = (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
100	99 55	elrnmpti	$⊢ y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \leftrightarrow \exists n \in ℕ y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)$
101	98 100	sylib	$⊢ (((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \to \exists n \in ℕ y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)$
102	62 97 101	r19.29af	$⊢ (((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \land y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))) \to y \in t$
103	102	ex	$⊢ ((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \to (y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \to y \in t)$
104	103	ssrdv	$⊢ ((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \to ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \subseteq t$
105		nnex	$⊢ ℕ \in V$
106	105	mptex	$⊢ (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \in V$
107	106	rnex	$⊢ ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \in V$
108		elpwg	$⊢ ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \in V \to (ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \in 𝒫 t \leftrightarrow ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \subseteq t)$
109	107 108	ax-mp	$⊢ ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \in 𝒫 t \leftrightarrow ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \subseteq t$
110	104 109	sylibr	$⊢ ((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \to ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \in 𝒫 t$
111	16	simp3d	$⊢ t \in (P \cap L) \to \forall x \in 𝒫 t ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in t)$
112	111	ad4antr	$⊢ ((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \to \forall x \in 𝒫 t ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in t)$
113		nnct	$⊢ ℕ ≼ ω$
114		mptct	$⊢ ℕ ≼ ω \to (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) ≼ ω$
115	113 114	ax-mp	$⊢ (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) ≼ ω$
116		rnct	$⊢ (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) ≼ ω \to ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) ≼ ω$
117	115 116	mp1i	$⊢ ((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \to ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) ≼ ω$
118	43	iundisj2	$⊢ \underset{n \in ℕ}{Disj} (f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
119		disjrnmpt	$⊢ \underset{n \in ℕ}{Disj} (f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \to \underset{y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))}{Disj} y$
120	118 119	mp1i	$⊢ ((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \to \underset{y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))}{Disj} y$
121		breq1	$⊢ x = ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \to (x ≼ ω \leftrightarrow ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) ≼ ω)$
122		disjeq1	$⊢ x = ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \to (\underset{y \in x}{Disj} y \leftrightarrow \underset{y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))}{Disj} y)$
123	121 122	anbi12d	$⊢ x = ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \to ((x ≼ ω \land \underset{y \in x}{Disj} y) \leftrightarrow (ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) ≼ ω \land \underset{y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))}{Disj} y))$
124		unieq	$⊢ x = ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \to ⋃ x = ⋃ ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
125	124	eleq1d	$⊢ x = ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \to (⋃ x \in t \leftrightarrow ⋃ ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \in t)$
126	123 125	imbi12d	$⊢ x = ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \to (((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in t) \leftrightarrow ((ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) ≼ ω \land \underset{y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))}{Disj} y) \to ⋃ ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \in t))$
127	126	rspcv	$⊢ ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \in 𝒫 t \to (\forall x \in 𝒫 t ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in t) \to ((ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) ≼ ω \land \underset{y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))}{Disj} y) \to ⋃ ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \in t))$
128	127	imp	$⊢ (ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \in 𝒫 t \land \forall x \in 𝒫 t ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in t)) \to ((ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) ≼ ω \land \underset{y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))}{Disj} y) \to ⋃ ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \in t)$
129	128	imp	$⊢ ((ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \in 𝒫 t \land \forall x \in 𝒫 t ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in t)) \land (ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) ≼ ω \land \underset{y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))}{Disj} y)) \to ⋃ ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \in t$
130	110 112 117 120 129	syl22anc	$⊢ ((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \to ⋃ ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \in t$
131	56 130	eqeltrid	$⊢ ((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \to ⋃_{n \in ℕ} (f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \in t$
132	52 131	eqeltrrd	$⊢ ((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x) \to ⋃ x \in t$
133	42 132	exlimddv	$⊢ (((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \to ⋃ x \in t$
134	31 133	pm2.61dane	$⊢ ((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \to ⋃ x \in t$
135	134	ex	$⊢ (t \in (P \cap L) \land x \in 𝒫 t) \to (x ≼ ω \to ⋃ x \in t)$
136	135	ralrimiva	$⊢ t \in (P \cap L) \to \forall x \in 𝒫 t (x ≼ ω \to ⋃ x \in t)$
137	25 17 136	3jca	$⊢ t \in (P \cap L) \to (O \in t \land \forall x \in t O ∖ x \in t \land \forall x \in 𝒫 t (x ≼ ω \to ⋃ x \in t))$
138	11 137	jca	$⊢ t \in (P \cap L) \to (t \subseteq 𝒫 O \land (O \in t \land \forall x \in t O ∖ x \in t \land \forall x \in 𝒫 t (x ≼ ω \to ⋃ x \in t)))$
139		vex	$⊢ t \in V$
140		issiga	$⊢ t \in V \to (t \in sigAlgebra (O) \leftrightarrow (t \subseteq 𝒫 O \land (O \in t \land \forall x \in t O ∖ x \in t \land \forall x \in 𝒫 t (x ≼ ω \to ⋃ x \in t))))$
141	139 140	ax-mp	$⊢ t \in sigAlgebra (O) \leftrightarrow (t \subseteq 𝒫 O \land (O \in t \land \forall x \in t O ∖ x \in t \land \forall x \in 𝒫 t (x ≼ ω \to ⋃ x \in t)))$
142	138 141	sylibr	$⊢ t \in (P \cap L) \to t \in sigAlgebra (O)$
143	142	ssriv	$⊢ P \cap L \subseteq sigAlgebra (O)$
144	5 143	eqssi	$⊢ sigAlgebra (O) = P \cap L$

Metamath Proof Explorer

Theorem sigapildsys

Proof