issalnnd

Description: Sufficient condition to prove that S is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	issalnnd.s	$⊢ φ \to S \in V$
	issalnnd.z	$⊢ φ \to \emptyset \in S$
	issalnnd.x	$⊢ X = ⋃ S$
	issalnnd.d	$⊢ (φ \land y \in S) \to X ∖ y \in S$
	issalnnd.i	$⊢ (φ \land e : ℕ ⟶ S) \to ⋃_{n \in ℕ} e (n) \in S$
Assertion	issalnnd	$⊢ φ \to S \in SAlg$

Proof

Step	Hyp	Ref	Expression
1		issalnnd.s	$⊢ φ \to S \in V$
2		issalnnd.z	$⊢ φ \to \emptyset \in S$
3		issalnnd.x	$⊢ X = ⋃ S$
4		issalnnd.d	$⊢ (φ \land y \in S) \to X ∖ y \in S$
5		issalnnd.i	$⊢ (φ \land e : ℕ ⟶ S) \to ⋃_{n \in ℕ} e (n) \in S$
6		unieq	$⊢ y = \emptyset \to ⋃ y = ⋃ \emptyset$
7		uni0	$⊢ ⋃ \emptyset = \emptyset$
8	7	a1i	$⊢ y = \emptyset \to ⋃ \emptyset = \emptyset$
9	6 8	eqtrd	$⊢ y = \emptyset \to ⋃ y = \emptyset$
10	9	adantl	$⊢ (φ \land y = \emptyset) \to ⋃ y = \emptyset$
11	2	adantr	$⊢ (φ \land y = \emptyset) \to \emptyset \in S$
12	10 11	eqeltrd	$⊢ (φ \land y = \emptyset) \to ⋃ y \in S$
13	12	3ad2antl1	$⊢ ((φ \land y \in 𝒫 S \land y ≼ ω) \land y = \emptyset) \to ⋃ y \in S$
14		neqne	$⊢ \neg y = \emptyset \to y \neq \emptyset$
15	14	adantl	$⊢ ((φ \land y \in 𝒫 S \land y ≼ ω) \land \neg y = \emptyset) \to y \neq \emptyset$
16		nnfoctb	$⊢ (y ≼ ω \land y \neq \emptyset) \to \exists e e : ℕ \underset{onto}{⟶} y$
17	16	3ad2antl3	$⊢ ((φ \land y \in 𝒫 S \land y ≼ ω) \land y \neq \emptyset) \to \exists e e : ℕ \underset{onto}{⟶} y$
18		founiiun	$⊢ e : ℕ \underset{onto}{⟶} y \to ⋃ y = ⋃_{n \in ℕ} e (n)$
19	18	adantl	$⊢ ((φ \land y \in 𝒫 S) \land e : ℕ \underset{onto}{⟶} y) \to ⋃ y = ⋃_{n \in ℕ} e (n)$
20		simpll	$⊢ ((φ \land y \in 𝒫 S) \land e : ℕ \underset{onto}{⟶} y) \to φ$
21		fof	$⊢ e : ℕ \underset{onto}{⟶} y \to e : ℕ ⟶ y$
22	21	adantl	$⊢ (y \in 𝒫 S \land e : ℕ \underset{onto}{⟶} y) \to e : ℕ ⟶ y$
23		elpwi	$⊢ y \in 𝒫 S \to y \subseteq S$
24	23	adantr	$⊢ (y \in 𝒫 S \land e : ℕ \underset{onto}{⟶} y) \to y \subseteq S$
25	22 24	fssd	$⊢ (y \in 𝒫 S \land e : ℕ \underset{onto}{⟶} y) \to e : ℕ ⟶ S$
26	25	adantll	$⊢ ((φ \land y \in 𝒫 S) \land e : ℕ \underset{onto}{⟶} y) \to e : ℕ ⟶ S$
27	20 26 5	syl2anc	$⊢ ((φ \land y \in 𝒫 S) \land e : ℕ \underset{onto}{⟶} y) \to ⋃_{n \in ℕ} e (n) \in S$
28	19 27	eqeltrd	$⊢ ((φ \land y \in 𝒫 S) \land e : ℕ \underset{onto}{⟶} y) \to ⋃ y \in S$
29	28	ex	$⊢ (φ \land y \in 𝒫 S) \to (e : ℕ \underset{onto}{⟶} y \to ⋃ y \in S)$
30	29	adantr	$⊢ ((φ \land y \in 𝒫 S) \land y \neq \emptyset) \to (e : ℕ \underset{onto}{⟶} y \to ⋃ y \in S)$
31	30	3adantl3	$⊢ ((φ \land y \in 𝒫 S \land y ≼ ω) \land y \neq \emptyset) \to (e : ℕ \underset{onto}{⟶} y \to ⋃ y \in S)$
32	31	exlimdv	$⊢ ((φ \land y \in 𝒫 S \land y ≼ ω) \land y \neq \emptyset) \to (\exists e e : ℕ \underset{onto}{⟶} y \to ⋃ y \in S)$
33	17 32	mpd	$⊢ ((φ \land y \in 𝒫 S \land y ≼ ω) \land y \neq \emptyset) \to ⋃ y \in S$
34	15 33	syldan	$⊢ ((φ \land y \in 𝒫 S \land y ≼ ω) \land \neg y = \emptyset) \to ⋃ y \in S$
35	13 34	pm2.61dan	$⊢ (φ \land y \in 𝒫 S \land y ≼ ω) \to ⋃ y \in S$
36	1 2 3 4 35	issald	$⊢ φ \to S \in SAlg$

Metamath Proof Explorer

Theorem issalnnd

Proof