dfsalgen2

Description: Alternate characterization of the sigma-algebra generated by a set. It is the smallest sigma-algebra, on the same base set, that includes the set. (Contributed by Glauco Siliprandi, 3-Jan-2021)

		Ref	Expression
	Hypothesis	dfsalgen2.1	$⊢ φ \to X \in V$
	Assertion	dfsalgen2	$⊢ φ \to (SalGen (X) = S \leftrightarrow ((S \in SAlg \land ⋃ S = ⋃ X \land X \subseteq S) \land \forall y \in SAlg ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y)))$

Proof

Step	Hyp	Ref	Expression
1		dfsalgen2.1	$⊢ φ \to X \in V$
2		id	$⊢ SalGen (X) = S \to SalGen (X) = S$
3	2	eqcomd	$⊢ SalGen (X) = S \to S = SalGen (X)$
4	3	adantl	$⊢ (φ \land SalGen (X) = S) \to S = SalGen (X)$
5		salgencl	$⊢ X \in V \to SalGen (X) \in SAlg$
6	1 5	syl	$⊢ φ \to SalGen (X) \in SAlg$
7	6	adantr	$⊢ (φ \land SalGen (X) = S) \to SalGen (X) \in SAlg$
8	4 7	eqeltrd	$⊢ (φ \land SalGen (X) = S) \to S \in SAlg$
9		unieq	$⊢ SalGen (X) = S \to ⋃ SalGen (X) = ⋃ S$
10	9	adantl	$⊢ (φ \land SalGen (X) = S) \to ⋃ SalGen (X) = ⋃ S$
11	1	adantr	$⊢ (φ \land SalGen (X) = S) \to X \in V$
12		eqid	$⊢ SalGen (X) = SalGen (X)$
13		eqid	$⊢ ⋃ X = ⋃ X$
14	11 12 13	salgenuni	$⊢ (φ \land SalGen (X) = S) \to ⋃ SalGen (X) = ⋃ X$
15	10 14	eqtr3d	$⊢ (φ \land SalGen (X) = S) \to ⋃ S = ⋃ X$
16	12	sssalgen	$⊢ X \in V \to X \subseteq SalGen (X)$
17	11 16	syl	$⊢ (φ \land SalGen (X) = S) \to X \subseteq SalGen (X)$
18		simpr	$⊢ (φ \land SalGen (X) = S) \to SalGen (X) = S$
19	17 18	sseqtrd	$⊢ (φ \land SalGen (X) = S) \to X \subseteq S$
20	8 15 19	3jca	$⊢ (φ \land SalGen (X) = S) \to (S \in SAlg \land ⋃ S = ⋃ X \land X \subseteq S)$
21	4	ad2antrr	$⊢ (((φ \land SalGen (X) = S) \land y \in SAlg) \land X \subseteq y) \to S = SalGen (X)$
22	21	adantrl	$⊢ (((φ \land SalGen (X) = S) \land y \in SAlg) \land (⋃ y = ⋃ X \land X \subseteq y)) \to S = SalGen (X)$
23	11	ad2antrr	$⊢ (((φ \land SalGen (X) = S) \land y \in SAlg) \land X \subseteq y) \to X \in V$
24	23	adantrl	$⊢ (((φ \land SalGen (X) = S) \land y \in SAlg) \land (⋃ y = ⋃ X \land X \subseteq y)) \to X \in V$
25		simplr	$⊢ (((φ \land SalGen (X) = S) \land y \in SAlg) \land X \subseteq y) \to y \in SAlg$
26	25	adantrl	$⊢ (((φ \land SalGen (X) = S) \land y \in SAlg) \land (⋃ y = ⋃ X \land X \subseteq y)) \to y \in SAlg$
27		simpr	$⊢ (((φ \land SalGen (X) = S) \land y \in SAlg) \land X \subseteq y) \to X \subseteq y$
28	27	adantrl	$⊢ (((φ \land SalGen (X) = S) \land y \in SAlg) \land (⋃ y = ⋃ X \land X \subseteq y)) \to X \subseteq y$
29		simprl	$⊢ (((φ \land SalGen (X) = S) \land y \in SAlg) \land (⋃ y = ⋃ X \land X \subseteq y)) \to ⋃ y = ⋃ X$
30	24 12 26 28 29	salgenss	$⊢ (((φ \land SalGen (X) = S) \land y \in SAlg) \land (⋃ y = ⋃ X \land X \subseteq y)) \to SalGen (X) \subseteq y$
31	22 30	eqsstrd	$⊢ (((φ \land SalGen (X) = S) \land y \in SAlg) \land (⋃ y = ⋃ X \land X \subseteq y)) \to S \subseteq y$
32	31	ex	$⊢ ((φ \land SalGen (X) = S) \land y \in SAlg) \to ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y)$
33	32	ralrimiva	$⊢ (φ \land SalGen (X) = S) \to \forall y \in SAlg ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y)$
34	20 33	jca	$⊢ (φ \land SalGen (X) = S) \to ((S \in SAlg \land ⋃ S = ⋃ X \land X \subseteq S) \land \forall y \in SAlg ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y))$
35	34	ex	$⊢ φ \to (SalGen (X) = S \to ((S \in SAlg \land ⋃ S = ⋃ X \land X \subseteq S) \land \forall y \in SAlg ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y)))$
36	1	adantr	$⊢ (φ \land ((S \in SAlg \land ⋃ S = ⋃ X \land X \subseteq S) \land \forall y \in SAlg ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y))) \to X \in V$
37		simprl1	$⊢ (φ \land ((S \in SAlg \land ⋃ S = ⋃ X \land X \subseteq S) \land \forall y \in SAlg ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y))) \to S \in SAlg$
38		simprl2	$⊢ (φ \land ((S \in SAlg \land ⋃ S = ⋃ X \land X \subseteq S) \land \forall y \in SAlg ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y))) \to ⋃ S = ⋃ X$
39		simprl3	$⊢ (φ \land ((S \in SAlg \land ⋃ S = ⋃ X \land X \subseteq S) \land \forall y \in SAlg ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y))) \to X \subseteq S$
40		unieq	$⊢ y = w \to ⋃ y = ⋃ w$
41	40	eqeq1d	$⊢ y = w \to (⋃ y = ⋃ X \leftrightarrow ⋃ w = ⋃ X)$
42		sseq2	$⊢ y = w \to (X \subseteq y \leftrightarrow X \subseteq w)$
43	41 42	anbi12d	$⊢ y = w \to ((⋃ y = ⋃ X \land X \subseteq y) \leftrightarrow (⋃ w = ⋃ X \land X \subseteq w))$
44		sseq2	$⊢ y = w \to (S \subseteq y \leftrightarrow S \subseteq w)$
45	43 44	imbi12d	$⊢ y = w \to (((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y) \leftrightarrow ((⋃ w = ⋃ X \land X \subseteq w) \to S \subseteq w))$
46	45	cbvralvw	$⊢ \forall y \in SAlg ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y) \leftrightarrow \forall w \in SAlg ((⋃ w = ⋃ X \land X \subseteq w) \to S \subseteq w)$
47	46	birani	$⊢ (\forall y \in SAlg ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y) \land w \in SAlg) \to \forall w \in SAlg ((⋃ w = ⋃ X \land X \subseteq w) \to S \subseteq w)$
48		simpr	$⊢ (\forall y \in SAlg ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y) \land w \in SAlg) \to w \in SAlg$
49	47 48	jca	$⊢ (\forall y \in SAlg ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y) \land w \in SAlg) \to (\forall w \in SAlg ((⋃ w = ⋃ X \land X \subseteq w) \to S \subseteq w) \land w \in SAlg)$
50	49	3ad2antr1	$⊢ (\forall y \in SAlg ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y) \land (w \in SAlg \land ⋃ w = ⋃ X \land X \subseteq w)) \to (\forall w \in SAlg ((⋃ w = ⋃ X \land X \subseteq w) \to S \subseteq w) \land w \in SAlg)$
51		3simpc	$⊢ (w \in SAlg \land ⋃ w = ⋃ X \land X \subseteq w) \to (⋃ w = ⋃ X \land X \subseteq w)$
52	51	adantl	$⊢ (\forall y \in SAlg ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y) \land (w \in SAlg \land ⋃ w = ⋃ X \land X \subseteq w)) \to (⋃ w = ⋃ X \land X \subseteq w)$
53		rspa	$⊢ (\forall w \in SAlg ((⋃ w = ⋃ X \land X \subseteq w) \to S \subseteq w) \land w \in SAlg) \to ((⋃ w = ⋃ X \land X \subseteq w) \to S \subseteq w)$
54	50 52 53	sylc	$⊢ (\forall y \in SAlg ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y) \land (w \in SAlg \land ⋃ w = ⋃ X \land X \subseteq w)) \to S \subseteq w$
55	54	adantll	$⊢ (((S \in SAlg \land ⋃ S = ⋃ X \land X \subseteq S) \land \forall y \in SAlg ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y)) \land (w \in SAlg \land ⋃ w = ⋃ X \land X \subseteq w)) \to S \subseteq w$
56	55	adantll	$⊢ ((φ \land ((S \in SAlg \land ⋃ S = ⋃ X \land X \subseteq S) \land \forall y \in SAlg ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y))) \land (w \in SAlg \land ⋃ w = ⋃ X \land X \subseteq w)) \to S \subseteq w$
57	36 37 38 39 56	issalgend	$⊢ (φ \land ((S \in SAlg \land ⋃ S = ⋃ X \land X \subseteq S) \land \forall y \in SAlg ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y))) \to SalGen (X) = S$
58	57	ex	$⊢ φ \to (((S \in SAlg \land ⋃ S = ⋃ X \land X \subseteq S) \land \forall y \in SAlg ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y)) \to SalGen (X) = S)$
59	35 58	impbid	$⊢ φ \to (SalGen (X) = S \leftrightarrow ((S \in SAlg \land ⋃ S = ⋃ X \land X \subseteq S) \land \forall y \in SAlg ((⋃ y = ⋃ X \land X \subseteq y) \to S \subseteq y)))$

Metamath Proof Explorer

Theorem dfsalgen2

Proof