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	biimpi	$⊢ A \neq \emptyset \to \exists z z \in A$
25	24	adantl	$⊢ (φ \land A \neq \emptyset) \to \exists z z \in A$
26		disjel	$⊢ (A \cap B = \emptyset \land z \in A) \to \neg z \in B$
27	5 26	sylan	$⊢ (φ \land z \in A) \to \neg z \in B$
28		nelne1	$⊢ (z \in A \land \neg z \in B) \to A \neq B$
29	28	adantll	$⊢ ((φ \land z \in A) \land \neg z \in B) \to A \neq B$
30	27 29	mpdan	$⊢ (φ \land z \in A) \to A \neq B$
31	30	adantlr	$⊢ ((φ \land A \neq \emptyset) \land z \in A) \to A \neq B$
32	25 31	exlimddv	$⊢ (φ \land A \neq \emptyset) \to A \neq B$
33		id	$⊢ y = A \to y = A$
34		id	$⊢ y = B \to y = B$
35	33 34	disjprgw	$⊢ (A \in S \land B \in S \land A \neq B) \to (\underset{y \in \{A, B\}}{Disj} y \leftrightarrow A \cap B = \emptyset)$
36	21 22 32 35	syl3anc	$⊢ (φ \land A \neq \emptyset) \to (\underset{y \in \{A, B\}}{Disj} y \leftrightarrow A \cap B = \emptyset)$
37	20 36	mpbird	$⊢ (φ \land A \neq \emptyset) \to \underset{y \in \{A, B\}}{Disj} y$
38		breq1	$⊢ z = \{A, B\} \to (z ≼ ω \leftrightarrow \{A, B\} ≼ ω)$
39		disjeq1	$⊢ z = \{A, B\} \to (\underset{y \in z}{Disj} y \leftrightarrow \underset{y \in \{A, B\}}{Disj} y)$
40	38 39	anbi12d	$⊢ z = \{A, B\} \to ((z ≼ ω \land \underset{y \in z}{Disj} y) \leftrightarrow (\{A, B\} ≼ ω \land \underset{y \in \{A, B\}}{Disj} y))$
41		unieq	$⊢ z = \{A, B\} \to ⋃ z = ⋃ \{A, B\}$
42	41	eleq1d	$⊢ z = \{A, B\} \to (⋃ z \in S \leftrightarrow ⋃ \{A, B\} \in S)$
43	40 42	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))$
44		biid	$⊢ \emptyset \in s \leftrightarrow \emptyset \in s$
45		difeq2	$⊢ x = z \to O ∖ x = O ∖ z$
46	45	eleq1d	$⊢ x = z \to (O ∖ x \in s \leftrightarrow O ∖ z \in s)$
47	46	cbvralvw	$⊢ \forall x \in s O ∖ x \in s \leftrightarrow \forall z \in s O ∖ z \in s$
48		breq1	$⊢ x = z \to (x ≼ ω \leftrightarrow z ≼ ω)$
49		disjeq1	$⊢ x = z \to (\underset{y \in x}{Disj} y \leftrightarrow \underset{y \in z}{Disj} y)$
50	48 49	anbi12d	$⊢ x = z \to ((x ≼ ω \land \underset{y \in x}{Disj} y) \leftrightarrow (z ≼ ω \land \underset{y \in z}{Disj} y))$
51		unieq	$⊢ x = z \to ⋃ x = ⋃ z$
52	51	eleq1d	$⊢ x = z \to (⋃ x \in s \leftrightarrow ⋃ z \in s)$
53	50 52	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))$
54	53	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)$
55	44 47 54	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))$
56	55	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))\}$
57	1 56	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))\}$
58	57	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)))$
59	2 58	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)))$
60	59	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))$
61	60	simp3d	$⊢ φ \to \forall z \in 𝒫 S ((z ≼ ω \land \underset{y \in z}{Disj} y) \to ⋃ z \in S)$
62		prelpwi	$⊢ (A \in S \land B \in S) \to \{A, B\} \in 𝒫 S$
63	3 4 62	syl2anc	$⊢ φ \to \{A, B\} \in 𝒫 S$
64	43 61 63	rspcdva	$⊢ φ \to ((\{A, B\} ≼ ω \land \underset{y \in \{A, B\}}{Disj} y) \to ⋃ \{A, B\} \in S)$
65	64	adantr	$⊢ (φ \land A \neq \emptyset) \to ((\{A, B\} ≼ ω \land \underset{y \in \{A, B\}}{Disj} y) \to ⋃ \{A, B\} \in S)$
66	19 37 65	mp2and	$⊢ (φ \land A \neq \emptyset) \to ⋃ \{A, B\} \in S$
67	16 66	eqeltrrd	$⊢ (φ \land A \neq \emptyset) \to A \cup B \in S$
68	13 67	pm2.61dane	$⊢ φ \to A \cup B \in S$

Metamath Proof Explorer

Theorem unelldsys

Proof