sigaclcuni

Description: A sigma-algebra is closed under countable union: indexed union version. (Contributed by Thierry Arnoux, 8-Jun-2017)

		Ref	Expression
	Hypothesis	sigaclcuni.1	$⊢ \underline{Ⅎ} k A$
	Assertion	sigaclcuni	$⊢ (S \in ⋃ ran sigAlgebra \land \forall k \in A B \in S \land A ≼ ω) \to ⋃_{k \in A} B \in S$

Proof

Step	Hyp	Ref	Expression
1		sigaclcuni.1	$⊢ \underline{Ⅎ} k A$
2		dfiun2g	$⊢ \forall k \in A B \in S \to ⋃_{k \in A} B = ⋃ \{z \| \exists k \in A z = B\}$
3	2	3ad2ant2	$⊢ (S \in ⋃ ran sigAlgebra \land \forall k \in A B \in S \land A ≼ ω) \to ⋃_{k \in A} B = ⋃ \{z \| \exists k \in A z = B\}$
4		simp1	$⊢ (S \in ⋃ ran sigAlgebra \land \forall k \in A B \in S \land A ≼ ω) \to S \in ⋃ ran sigAlgebra$
5		r19.29	$⊢ (\forall k \in A B \in S \land \exists k \in A z = B) \to \exists k \in A (B \in S \land z = B)$
6		simpr	$⊢ (B \in S \land z = B) \to z = B$
7		simpl	$⊢ (B \in S \land z = B) \to B \in S$
8	6 7	eqeltrd	$⊢ (B \in S \land z = B) \to z \in S$
9	8	rexlimivw	$⊢ \exists k \in A (B \in S \land z = B) \to z \in S$
10	5 9	syl	$⊢ (\forall k \in A B \in S \land \exists k \in A z = B) \to z \in S$
11	10	ex	$⊢ \forall k \in A B \in S \to (\exists k \in A z = B \to z \in S)$
12	11	abssdv	$⊢ \forall k \in A B \in S \to \{z \| \exists k \in A z = B\} \subseteq S$
13	12	3ad2ant2	$⊢ (S \in ⋃ ran sigAlgebra \land \forall k \in A B \in S \land A ≼ ω) \to \{z \| \exists k \in A z = B\} \subseteq S$
14		elpw2g	$⊢ S \in ⋃ ran sigAlgebra \to (\{z \| \exists k \in A z = B\} \in 𝒫 S \leftrightarrow \{z \| \exists k \in A z = B\} \subseteq S)$
15	4 14	syl	$⊢ (S \in ⋃ ran sigAlgebra \land \forall k \in A B \in S \land A ≼ ω) \to (\{z \| \exists k \in A z = B\} \in 𝒫 S \leftrightarrow \{z \| \exists k \in A z = B\} \subseteq S)$
16	13 15	mpbird	$⊢ (S \in ⋃ ran sigAlgebra \land \forall k \in A B \in S \land A ≼ ω) \to \{z \| \exists k \in A z = B\} \in 𝒫 S$
17	1	abrexctf	$⊢ A ≼ ω \to \{z \| \exists k \in A z = B\} ≼ ω$
18	17	3ad2ant3	$⊢ (S \in ⋃ ran sigAlgebra \land \forall k \in A B \in S \land A ≼ ω) \to \{z \| \exists k \in A z = B\} ≼ ω$
19		sigaclcu	$⊢ (S \in ⋃ ran sigAlgebra \land \{z \| \exists k \in A z = B\} \in 𝒫 S \land \{z \| \exists k \in A z = B\} ≼ ω) \to ⋃ \{z \| \exists k \in A z = B\} \in S$
20	4 16 18 19	syl3anc	$⊢ (S \in ⋃ ran sigAlgebra \land \forall k \in A B \in S \land A ≼ ω) \to ⋃ \{z \| \exists k \in A z = B\} \in S$
21	3 20	eqeltrd	$⊢ (S \in ⋃ ran sigAlgebra \land \forall k \in A B \in S \land A ≼ ω) \to ⋃_{k \in A} B \in S$

Metamath Proof Explorer

Theorem sigaclcuni

Proof