unelldsys

Description: Lambda-systems are closed under disjoint set unions. (Contributed by Thierry Arnoux, 21-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))\}$
	unelldsys.s	$⊢ φ \to S \in L$
	unelldsys.a	$⊢ φ \to A \in S$
	unelldsys.b	$⊢ φ \to B \in S$
	unelldsys.c	$⊢ φ \to A \cap B = \emptyset$
Assertion	unelldsys	$⊢ φ \to A \cup B \in S$

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		unelldsys.s	$⊢ φ \to S \in L$
3		unelldsys.a	$⊢ φ \to A \in S$
4		unelldsys.b	$⊢ φ \to B \in S$
5		unelldsys.c	$⊢ φ \to A \cap B = \emptyset$
6		uneq1	$⊢ A = \emptyset \to A \cup B = \emptyset \cup B$
7	6	adantl	$⊢ (φ \land A = \emptyset) \to A \cup B = \emptyset \cup B$
8		uncom	$⊢ B \cup \emptyset = \emptyset \cup B$
9		un0	$⊢ B \cup \emptyset = B$
10	8 9	eqtr3i	$⊢ \emptyset \cup B = B$
11	7 10	eqtrdi	$⊢ (φ \land A = \emptyset) \to A \cup B = B$
12	4	adantr	$⊢ (φ \land A = \emptyset) \to B \in S$
13	11 12	eqeltrd	$⊢ (φ \land A = \emptyset) \to A \cup B \in S$
14		uniprg	$⊢ (A \in S \land B \in S) \to ⋃ \{A, B\} = A \cup B$
15	3 4 14	syl2anc	$⊢ φ \to ⋃ \{A, B\} = A \cup B$
16	15	adantr	$⊢ (φ \land A \neq \emptyset) \to ⋃ \{A, B\} = A \cup B$
17		prct	$⊢ (A \in S \land B \in S) \to \{A, B\} ≼ ω$
18	3 4 17	syl2anc	$⊢ φ \to \{A, B\} ≼ ω$
19	18	adantr	$⊢ (φ \land A \neq \emptyset) \to \{A, B\} ≼ ω$
20	5	adantr	$⊢ (φ \land A \neq \emptyset) \to A \cap B = \emptyset$
21	3	adantr	$⊢ (φ \land A \neq \emptyset) \to A \in S$
22	4	adantr	$⊢ (φ \land A \neq \emptyset) \to B \in S$
23		n0	$⊢ A \neq \emptyset \leftrightarrow \exists z z \in A$
24	23	bilani	$⊢ (φ \land A \neq \emptyset) \to \exists z z \in A$
25		disjel	$⊢ (A \cap B = \emptyset \land z \in A) \to \neg z \in B$
26	5 25	sylan	$⊢ (φ \land z \in A) \to \neg z \in B$
27		nelne1	$⊢ (z \in A \land \neg z \in B) \to A \neq B$
28	27	adantll	$⊢ ((φ \land z \in A) \land \neg z \in B) \to A \neq B$
29	26 28	mpdan	$⊢ (φ \land z \in A) \to A \neq B$
30	29	adantlr	$⊢ ((φ \land A \neq \emptyset) \land z \in A) \to A \neq B$
31	24 30	exlimddv	$⊢ (φ \land A \neq \emptyset) \to A \neq B$
32		id	$⊢ y = A \to y = A$
33		id	$⊢ y = B \to y = B$
34	32 33	disjprg	$⊢ (A \in S \land B \in S \land A \neq B) \to (\underset{y \in \{A, B\}}{Disj} y \leftrightarrow A \cap B = \emptyset)$
35	21 22 31 34	syl3anc	$⊢ (φ \land A \neq \emptyset) \to (\underset{y \in \{A, B\}}{Disj} y \leftrightarrow A \cap B = \emptyset)$
36	20 35	mpbird	$⊢ (φ \land A \neq \emptyset) \to \underset{y \in \{A, B\}}{Disj} y$
37		breq1	$⊢ z = \{A, B\} \to (z ≼ ω \leftrightarrow \{A, B\} ≼ ω)$
38		disjeq1	$⊢ z = \{A, B\} \to (\underset{y \in z}{Disj} y \leftrightarrow \underset{y \in \{A, B\}}{Disj} y)$
39	37 38	anbi12d	$⊢ z = \{A, B\} \to ((z ≼ ω \land \underset{y \in z}{Disj} y) \leftrightarrow (\{A, B\} ≼ ω \land \underset{y \in \{A, B\}}{Disj} y))$
40		unieq	$⊢ z = \{A, B\} \to ⋃ z = ⋃ \{A, B\}$
41	40	eleq1d	$⊢ z = \{A, B\} \to (⋃ z \in S \leftrightarrow ⋃ \{A, B\} \in S)$
42	39 41	imbi12d	$⊢ z = \{A, B\} \to (((z ≼ ω \land \underset{y \in z}{Disj} y) \to ⋃ z \in S) \leftrightarrow ((\{A, B\} ≼ ω \land \underset{y \in \{A, B\}}{Disj} y) \to ⋃ \{A, B\} \in S))$
43		biid	$⊢ \emptyset \in s \leftrightarrow \emptyset \in s$
44		difeq2	$⊢ x = z \to O ∖ x = O ∖ z$
45	44	eleq1d	$⊢ x = z \to (O ∖ x \in s \leftrightarrow O ∖ z \in s)$
46	45	cbvralvw	$⊢ \forall x \in s O ∖ x \in s \leftrightarrow \forall z \in s O ∖ z \in s$
47		breq1	$⊢ x = z \to (x ≼ ω \leftrightarrow z ≼ ω)$
48		disjeq1	$⊢ x = z \to (\underset{y \in x}{Disj} y \leftrightarrow \underset{y \in z}{Disj} y)$
49	47 48	anbi12d	$⊢ x = z \to ((x ≼ ω \land \underset{y \in x}{Disj} y) \leftrightarrow (z ≼ ω \land \underset{y \in z}{Disj} y))$
50		unieq	$⊢ x = z \to ⋃ x = ⋃ z$
51	50	eleq1d	$⊢ x = z \to (⋃ x \in s \leftrightarrow ⋃ z \in s)$
52	49 51	imbi12d	$⊢ x = z \to (((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in s) \leftrightarrow ((z ≼ ω \land \underset{y \in z}{Disj} y) \to ⋃ z \in s))$
53	52	cbvralvw	$⊢ \forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in s) \leftrightarrow \forall z \in 𝒫 s ((z ≼ ω \land \underset{y \in z}{Disj} y) \to ⋃ z \in s)$
54	43 46 53	3anbi123i	$⊢ (\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)) \leftrightarrow (\emptyset \in s \land \forall z \in s O ∖ z \in s \land \forall z \in 𝒫 s ((z ≼ ω \land \underset{y \in z}{Disj} y) \to ⋃ z \in s))$
55	54	rabbii	$⊢ \{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))\} = \{s \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall z \in s O ∖ z \in s \land \forall z \in 𝒫 s ((z ≼ ω \land \underset{y \in z}{Disj} y) \to ⋃ z \in s))\}$
56	1 55	eqtri	$⊢ L = \{s \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall z \in s O ∖ z \in s \land \forall z \in 𝒫 s ((z ≼ ω \land \underset{y \in z}{Disj} y) \to ⋃ z \in s))\}$
57	56	isldsys	$⊢ S \in L \leftrightarrow (S \in 𝒫 𝒫 O \land (\emptyset \in S \land \forall z \in S O ∖ z \in S \land \forall z \in 𝒫 S ((z ≼ ω \land \underset{y \in z}{Disj} y) \to ⋃ z \in S)))$
58	2 57	sylib	$⊢ φ \to (S \in 𝒫 𝒫 O \land (\emptyset \in S \land \forall z \in S O ∖ z \in S \land \forall z \in 𝒫 S ((z ≼ ω \land \underset{y \in z}{Disj} y) \to ⋃ z \in S)))$
59	58	simprd	$⊢ φ \to (\emptyset \in S \land \forall z \in S O ∖ z \in S \land \forall z \in 𝒫 S ((z ≼ ω \land \underset{y \in z}{Disj} y) \to ⋃ z \in S))$
60	59	simp3d	$⊢ φ \to \forall z \in 𝒫 S ((z ≼ ω \land \underset{y \in z}{Disj} y) \to ⋃ z \in S)$
61		prelpwi	$⊢ (A \in S \land B \in S) \to \{A, B\} \in 𝒫 S$
62	3 4 61	syl2anc	$⊢ φ \to \{A, B\} \in 𝒫 S$
63	42 60 62	rspcdva	$⊢ φ \to ((\{A, B\} ≼ ω \land \underset{y \in \{A, B\}}{Disj} y) \to ⋃ \{A, B\} \in S)$
64	63	adantr	$⊢ (φ \land A \neq \emptyset) \to ((\{A, B\} ≼ ω \land \underset{y \in \{A, B\}}{Disj} y) \to ⋃ \{A, B\} \in S)$
65	19 36 64	mp2and	$⊢ (φ \land A \neq \emptyset) \to ⋃ \{A, B\} \in S$
66	16 65	eqeltrrd	$⊢ (φ \land A \neq \emptyset) \to A \cup B \in S$
67	13 66	pm2.61dane	$⊢ φ \to A \cup B \in S$

Metamath Proof Explorer

Theorem unelldsys

Proof