sigapildsyslem

	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))\}$
	sigapildsyslem.n	$⊢ Ⅎ n φ$
	sigapildsyslem.1	$⊢ φ \to t \in (P \cap L)$
	sigapildsyslem.2	$⊢ φ \to A \in t$
	sigapildsyslem.3	$⊢ φ \to N \in Fin$
	sigapildsyslem.4	$⊢ (φ \land n \in N) \to B \in t$
Assertion	sigapildsyslem	$⊢ φ \to A ∖ ⋃_{n \in N} B \in t$

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		sigapildsyslem.n	$⊢ Ⅎ n φ$
4		sigapildsyslem.1	$⊢ φ \to t \in (P \cap L)$
5		sigapildsyslem.2	$⊢ φ \to A \in t$
6		sigapildsyslem.3	$⊢ φ \to N \in Fin$
7		sigapildsyslem.4	$⊢ (φ \land n \in N) \to B \in t$
8		iuneq1	$⊢ N = \emptyset \to ⋃_{n \in N} B = ⋃_{n \in \emptyset} B$
9		0iun	$⊢ ⋃_{n \in \emptyset} B = \emptyset$
10	8 9	eqtrdi	$⊢ N = \emptyset \to ⋃_{n \in N} B = \emptyset$
11	10	difeq2d	$⊢ N = \emptyset \to A ∖ ⋃_{n \in N} B = A ∖ \emptyset$
12		dif0	$⊢ A ∖ \emptyset = A$
13	11 12	eqtrdi	$⊢ N = \emptyset \to A ∖ ⋃_{n \in N} B = A$
14	13	adantl	$⊢ (φ \land N = \emptyset) \to A ∖ ⋃_{n \in N} B = A$
15	5	adantr	$⊢ (φ \land N = \emptyset) \to A \in t$
16	14 15	eqeltrd	$⊢ (φ \land N = \emptyset) \to A ∖ ⋃_{n \in N} B \in t$
17		iindif2	$⊢ N \neq \emptyset \to ⋂_{n \in N} (A ∖ B) = A ∖ ⋃_{n \in N} B$
18	17	adantl	$⊢ (φ \land N \neq \emptyset) \to ⋂_{n \in N} (A ∖ B) = A ∖ ⋃_{n \in N} B$
19	4	adantr	$⊢ (φ \land N \neq \emptyset) \to t \in (P \cap L)$
20	19	elin1d	$⊢ (φ \land N \neq \emptyset) \to t \in P$
21	1	ispisys	$⊢ t \in P \leftrightarrow (t \in 𝒫 𝒫 O \land fi (t) \subseteq t)$
22	20 21	sylib	$⊢ (φ \land N \neq \emptyset) \to (t \in 𝒫 𝒫 O \land fi (t) \subseteq t)$
23	22	simprd	$⊢ (φ \land N \neq \emptyset) \to fi (t) \subseteq t$
24		nfv	$⊢ Ⅎ n N \neq \emptyset$
25	3 24	nfan	$⊢ Ⅎ n (φ \land N \neq \emptyset)$
26	22	simpld	$⊢ (φ \land N \neq \emptyset) \to t \in 𝒫 𝒫 O$
27	26	elpwid	$⊢ (φ \land N \neq \emptyset) \to t \subseteq 𝒫 O$
28	5	adantr	$⊢ (φ \land N \neq \emptyset) \to A \in t$
29	27 28	sseldd	$⊢ (φ \land N \neq \emptyset) \to A \in 𝒫 O$
30	29	elpwid	$⊢ (φ \land N \neq \emptyset) \to A \subseteq O$
31	30	adantr	$⊢ ((φ \land N \neq \emptyset) \land n \in N) \to A \subseteq O$
32		difin2	$⊢ A \subseteq O \to A ∖ B = (O ∖ B) \cap A$
33	31 32	syl	$⊢ ((φ \land N \neq \emptyset) \land n \in N) \to A ∖ B = (O ∖ B) \cap A$
34	23	adantr	$⊢ ((φ \land N \neq \emptyset) \land n \in N) \to fi (t) \subseteq t$
35	19	adantr	$⊢ ((φ \land N \neq \emptyset) \land n \in N) \to t \in (P \cap L)$
36	19	elin2d	$⊢ (φ \land N \neq \emptyset) \to t \in L$
37	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)))$
38	36 37	sylib	$⊢ (φ \land N \neq \emptyset) \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)))$
39	38	simprd	$⊢ (φ \land N \neq \emptyset) \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))$
40	39	simp2d	$⊢ (φ \land N \neq \emptyset) \to \forall x \in t O ∖ x \in t$
41	40	adantr	$⊢ ((φ \land N \neq \emptyset) \land n \in N) \to \forall x \in t O ∖ x \in t$
42	7	adantlr	$⊢ ((φ \land N \neq \emptyset) \land n \in N) \to B \in t$
43		nfv	$⊢ Ⅎ x O ∖ B \in t$
44		difeq2	$⊢ x = B \to O ∖ x = O ∖ B$
45	44	eleq1d	$⊢ x = B \to (O ∖ x \in t \leftrightarrow O ∖ B \in t)$
46	43 45	rspc	$⊢ B \in t \to (\forall x \in t O ∖ x \in t \to O ∖ B \in t)$
47	42 46	syl	$⊢ ((φ \land N \neq \emptyset) \land n \in N) \to (\forall x \in t O ∖ x \in t \to O ∖ B \in t)$
48	41 47	mpd	$⊢ ((φ \land N \neq \emptyset) \land n \in N) \to O ∖ B \in t$
49	28	adantr	$⊢ ((φ \land N \neq \emptyset) \land n \in N) \to A \in t$
50		inelfi	$⊢ (t \in (P \cap L) \land O ∖ B \in t \land A \in t) \to (O ∖ B) \cap A \in fi (t)$
51	35 48 49 50	syl3anc	$⊢ ((φ \land N \neq \emptyset) \land n \in N) \to (O ∖ B) \cap A \in fi (t)$
52	34 51	sseldd	$⊢ ((φ \land N \neq \emptyset) \land n \in N) \to (O ∖ B) \cap A \in t$
53	33 52	eqeltrd	$⊢ ((φ \land N \neq \emptyset) \land n \in N) \to A ∖ B \in t$
54	53	ex	$⊢ (φ \land N \neq \emptyset) \to (n \in N \to A ∖ B \in t)$
55	25 54	ralrimi	$⊢ (φ \land N \neq \emptyset) \to \forall n \in N A ∖ B \in t$
56		simpr	$⊢ (φ \land N \neq \emptyset) \to N \neq \emptyset$
57	6	adantr	$⊢ (φ \land N \neq \emptyset) \to N \in Fin$
58		vex	$⊢ t \in V$
59		iinfi	$⊢ (t \in V \land (\forall n \in N A ∖ B \in t \land N \neq \emptyset \land N \in Fin)) \to ⋂_{n \in N} (A ∖ B) \in fi (t)$
60	58 59	mpan	$⊢ (\forall n \in N A ∖ B \in t \land N \neq \emptyset \land N \in Fin) \to ⋂_{n \in N} (A ∖ B) \in fi (t)$
61	55 56 57 60	syl3anc	$⊢ (φ \land N \neq \emptyset) \to ⋂_{n \in N} (A ∖ B) \in fi (t)$
62	23 61	sseldd	$⊢ (φ \land N \neq \emptyset) \to ⋂_{n \in N} (A ∖ B) \in t$
63	18 62	eqeltrrd	$⊢ (φ \land N \neq \emptyset) \to A ∖ ⋃_{n \in N} B \in t$
64	16 63	pm2.61dane	$⊢ φ \to A ∖ ⋃_{n \in N} B \in t$

Metamath Proof Explorer

Theorem sigapildsyslem

Proof