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	bilanri	$⊢ (((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \to \emptyset ≺ x$
35		simplr	$⊢ (((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \to x ≼ ω$
36		nnenom	$⊢ ℕ \approx ω$
37	36	ensymi	$⊢ ω \approx ℕ$
38		domentr	$⊢ (x ≼ ω \land ω \approx ℕ) \to x ≼ ℕ$
39	35 37 38	sylancl	$⊢ (((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \to x ≼ ℕ$
40		fodomr	$⊢ (\emptyset ≺ x \land x ≼ ℕ) \to \exists f f : ℕ \underset{onto}{⟶} x$
41	34 39 40	syl2anc	$⊢ (((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \to \exists f f : ℕ \underset{onto}{⟶} x$
42		fveq2	$⊢ n = i \to f (n) = f (i)$
43	42	iundisj	$⊢ ⋃_{n \in ℕ} f (n) = ⋃_{n \in ℕ} (f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
44		fofn	$⊢ f : ℕ \underset{onto}{⟶} x \to f Fn ℕ$
45		fniunfv	$⊢ f Fn ℕ \to ⋃_{n \in ℕ} f (n) = ⋃ ran f$
46	44 45	syl	$⊢ f : ℕ \underset{onto}{⟶} x \to ⋃_{n \in ℕ} f (n) = ⋃ ran f$
47		forn	$⊢ f : ℕ \underset{onto}{⟶} x \to ran f = x$
48	47	unieqd	$⊢ f : ℕ \underset{onto}{⟶} x \to ⋃ ran f = ⋃ x$
49	46 48	eqtrd	$⊢ f : ℕ \underset{onto}{⟶} x \to ⋃_{n \in ℕ} f (n) = ⋃ x$
50	43 49	eqtr3id	$⊢ f : ℕ \underset{onto}{⟶} x \to ⋃_{n \in ℕ} (f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) = ⋃ x$
51	50	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$
52		fvex	$⊢ f (n) \in V$
53		difexg	$⊢ f (n) \in V \to f (n) ∖ ⋃_{i \in (1 ..^n)} f (i) \in V$
54	52 53	ax-mp	$⊢ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i) \in V$
55	54	dfiun3	$⊢ ⋃_{n \in ℕ} (f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) = ⋃ ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
56		nfv	$⊢ Ⅎ n ((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x)$
57		nfcv	$⊢ \underline{Ⅎ} n y$
58		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
59	58	nfrn	$⊢ \underline{Ⅎ} n ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
60	57 59	nfel	$⊢ Ⅎ n y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
61	56 60	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)))$
62		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)$
63		nfv	$⊢ Ⅎ i ((((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \land f : ℕ \underset{onto}{⟶} x)$
64		nfcv	$⊢ \underline{Ⅎ} i y$
65		nfcv	$⊢ \underline{Ⅎ} i ℕ$
66		nfcv	$⊢ \underline{Ⅎ} i f (n)$
67		nfiu1	$⊢ \underline{Ⅎ} i ⋃_{i \in (1 ..^n)} f (i)$
68	66 67	nfdif	$⊢ \underline{Ⅎ} i (f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
69	65 68	nfmpt	$⊢ \underline{Ⅎ} i (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
70	69	nfrn	$⊢ \underline{Ⅎ} i ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
71	64 70	nfel	$⊢ Ⅎ i y \in ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
72	63 71	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)))$
73		nfv	$⊢ Ⅎ i n \in ℕ$
74	72 73	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 ℕ)$
75	64 68	nfeq	$⊢ Ⅎ i y = f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)$
76	74 75	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))$
77	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)$
78		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$
79	78	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$
80	79	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$
81		fof	$⊢ f : ℕ \underset{onto}{⟶} x \to f : ℕ ⟶ x$
82	81	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$
83		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 ℕ$
84	82 83	ffvelcdmd	$⊢ (((((((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$
85	80 84	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$
86		fzofi	$⊢ (1 ..^n) \in Fin$
87	86	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$
88	80	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$
89	82	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$
90		fzossnn	$⊢ (1 ..^n) \subseteq ℕ$
91	90	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 ℕ$
92	91	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 ℕ$
93	89 92	ffvelcdmd	$⊢ ((((((((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$
94	88 93	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$
95	1 2 76 77 85 87 94	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$
96	62 95	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$
97		eqid	$⊢ (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) = (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
98	97 54	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)$
99	98	bilani	$⊢ (((((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)$
100	61 96 99	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$
101	100	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)$
102	101	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$
103		nnex	$⊢ ℕ \in V$
104	103	mptex	$⊢ (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \in V$
105	104	rnex	$⊢ ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) \in V$
106		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)$
107	105 106	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$
108	102 107	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$
109	16	simp3d	$⊢ t \in (P \cap L) \to \forall x \in 𝒫 t ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in t)$
110	109	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)$
111		nnct	$⊢ ℕ ≼ ω$
112		mptct	$⊢ ℕ ≼ ω \to (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) ≼ ω$
113	111 112	ax-mp	$⊢ (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) ≼ ω$
114		rnct	$⊢ (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) ≼ ω \to ran (n \in ℕ ⟼ f (n) ∖ ⋃_{i \in (1 ..^n)} f (i)) ≼ ω$
115	113 114	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)) ≼ ω$
116	42	iundisj2	$⊢ \underset{n \in ℕ}{Disj} (f (n) ∖ ⋃_{i \in (1 ..^n)} f (i))$
117		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$
118	116 117	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$
119		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)) ≼ ω)$
120		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)$
121	119 120	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))$
122		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))$
123	122	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)$
124	121 123	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))$
125	124	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))$
126	125	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)$
127	126	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$
128	108 110 115 118 127	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$
129	55 128	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$
130	51 129	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$
131	41 130	exlimddv	$⊢ (((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \land x \neq \emptyset) \to ⋃ x \in t$
132	31 131	pm2.61dane	$⊢ ((t \in (P \cap L) \land x \in 𝒫 t) \land x ≼ ω) \to ⋃ x \in t$
133	132	ex	$⊢ (t \in (P \cap L) \land x \in 𝒫 t) \to (x ≼ ω \to ⋃ x \in t)$
134	133	ralrimiva	$⊢ t \in (P \cap L) \to \forall x \in 𝒫 t (x ≼ ω \to ⋃ x \in t)$
135	25 17 134	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))$
136	11 135	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)))$
137		vex	$⊢ t \in V$
138		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))))$
139	137 138	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)))$
140	136 139	sylibr	$⊢ t \in (P \cap L) \to t \in sigAlgebra (O)$
141	140	ssriv	$⊢ P \cap L \subseteq sigAlgebra (O)$
142	5 141	eqssi	$⊢ sigAlgebra (O) = P \cap L$

Metamath Proof Explorer

Theorem sigapildsys

Proof