Theorem dfsalgen2 46947

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.)

Hypothesis

Ref	Expression
dfsalgen2.1	⊢ (𝜑 → 𝑋 ∈ 𝑉)

Assertion

Ref	Expression
dfsalgen2	⊢ (𝜑 → ((SalGen‘𝑋) = 𝑆 ↔ ((𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆) ∧ ∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦))))

Distinct variable groups:   𝑦,𝑆   𝑦,𝑋   𝜑,𝑦

Allowed substitution hint:   𝑉(𝑦)

Proof of Theorem dfsalgen2

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 23	. . . . . . . 8 ⊢ ((SalGen‘𝑋) = 𝑆 → (SalGen‘𝑋) = 𝑆)
2	1	eqcomd 2775	. . . . . . 7 ⊢ ((SalGen‘𝑋) = 𝑆 → 𝑆 = (SalGen‘𝑋))
3	2	adantl 486	. . . . . 6 ⊢ ((𝜑 ∧ (SalGen‘𝑋) = 𝑆) → 𝑆 = (SalGen‘𝑋))
4		dfsalgen2.1	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
5		salgencl 46938	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) ∈ SAlg)
6	4, 5	syl 18	. . . . . . 7 ⊢ (𝜑 → (SalGen‘𝑋) ∈ SAlg)
7	6	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ (SalGen‘𝑋) = 𝑆) → (SalGen‘𝑋) ∈ SAlg)
8	3, 7	eqeltrd 2869	. . . . 5 ⊢ ((𝜑 ∧ (SalGen‘𝑋) = 𝑆) → 𝑆 ∈ SAlg)
9		unieq 4887	. . . . . . 7 ⊢ ((SalGen‘𝑋) = 𝑆 → ∪ (SalGen‘𝑋) = ∪ 𝑆)
10	9	adantl 486	. . . . . 6 ⊢ ((𝜑 ∧ (SalGen‘𝑋) = 𝑆) → ∪ (SalGen‘𝑋) = ∪ 𝑆)
11	4	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ (SalGen‘𝑋) = 𝑆) → 𝑋 ∈ 𝑉)
12		eqid 2769	. . . . . . 7 ⊢ (SalGen‘𝑋) = (SalGen‘𝑋)
13		eqid 2769	. . . . . . 7 ⊢ ∪ 𝑋 = ∪ 𝑋
14	11, 12, 13	salgenuni 46943	. . . . . 6 ⊢ ((𝜑 ∧ (SalGen‘𝑋) = 𝑆) → ∪ (SalGen‘𝑋) = ∪ 𝑋)
15	10, 14	eqtr3d 2806	. . . . 5 ⊢ ((𝜑 ∧ (SalGen‘𝑋) = 𝑆) → ∪ 𝑆 = ∪ 𝑋)
16	12	sssalgen 46941	. . . . . . 7 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ⊆ (SalGen‘𝑋))
17	11, 16	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ (SalGen‘𝑋) = 𝑆) → 𝑋 ⊆ (SalGen‘𝑋))
18		simpr 489	. . . . . 6 ⊢ ((𝜑 ∧ (SalGen‘𝑋) = 𝑆) → (SalGen‘𝑋) = 𝑆)
19	17, 18	sseqtrd 3981	. . . . 5 ⊢ ((𝜑 ∧ (SalGen‘𝑋) = 𝑆) → 𝑋 ⊆ 𝑆)
20	8, 15, 19	3jca 1144	. . . 4 ⊢ ((𝜑 ∧ (SalGen‘𝑋) = 𝑆) → (𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆))
21	3	ad2antrr 738	. . . . . . . 8 ⊢ ((((𝜑 ∧ (SalGen‘𝑋) = 𝑆) ∧ 𝑦 ∈ SAlg) ∧ 𝑋 ⊆ 𝑦) → 𝑆 = (SalGen‘𝑋))
22	21	adantrl 728	. . . . . . 7 ⊢ ((((𝜑 ∧ (SalGen‘𝑋) = 𝑆) ∧ 𝑦 ∈ SAlg) ∧ (∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦)) → 𝑆 = (SalGen‘𝑋))
23	11	ad2antrr 738	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (SalGen‘𝑋) = 𝑆) ∧ 𝑦 ∈ SAlg) ∧ 𝑋 ⊆ 𝑦) → 𝑋 ∈ 𝑉)
24	23	adantrl 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ (SalGen‘𝑋) = 𝑆) ∧ 𝑦 ∈ SAlg) ∧ (∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦)) → 𝑋 ∈ 𝑉)
25		simplr 780	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (SalGen‘𝑋) = 𝑆) ∧ 𝑦 ∈ SAlg) ∧ 𝑋 ⊆ 𝑦) → 𝑦 ∈ SAlg)
26	25	adantrl 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ (SalGen‘𝑋) = 𝑆) ∧ 𝑦 ∈ SAlg) ∧ (∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦)) → 𝑦 ∈ SAlg)
27		simpr 489	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (SalGen‘𝑋) = 𝑆) ∧ 𝑦 ∈ SAlg) ∧ 𝑋 ⊆ 𝑦) → 𝑋 ⊆ 𝑦)
28	27	adantrl 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ (SalGen‘𝑋) = 𝑆) ∧ 𝑦 ∈ SAlg) ∧ (∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦)) → 𝑋 ⊆ 𝑦)
29		simprl 782	. . . . . . . 8 ⊢ ((((𝜑 ∧ (SalGen‘𝑋) = 𝑆) ∧ 𝑦 ∈ SAlg) ∧ (∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦)) → ∪ 𝑦 = ∪ 𝑋)
30	24, 12, 26, 28, 29	salgenss 46942	. . . . . . 7 ⊢ ((((𝜑 ∧ (SalGen‘𝑋) = 𝑆) ∧ 𝑦 ∈ SAlg) ∧ (∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦)) → (SalGen‘𝑋) ⊆ 𝑦)
31	22, 30	eqsstrd 3979	. . . . . 6 ⊢ ((((𝜑 ∧ (SalGen‘𝑋) = 𝑆) ∧ 𝑦 ∈ SAlg) ∧ (∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦)) → 𝑆 ⊆ 𝑦)
32	31	ex 417	. . . . 5 ⊢ (((𝜑 ∧ (SalGen‘𝑋) = 𝑆) ∧ 𝑦 ∈ SAlg) → ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦))
33	32	ralrimiva 3163	. . . 4 ⊢ ((𝜑 ∧ (SalGen‘𝑋) = 𝑆) → ∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦))
34	20, 33	jca 520	. . 3 ⊢ ((𝜑 ∧ (SalGen‘𝑋) = 𝑆) → ((𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆) ∧ ∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦)))
35	34	ex 417	. 2 ⊢ (𝜑 → ((SalGen‘𝑋) = 𝑆 → ((𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆) ∧ ∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦))))
36	4	adantr 485	. . . 4 ⊢ ((𝜑 ∧ ((𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆) ∧ ∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦))) → 𝑋 ∈ 𝑉)
37		simprl1 1235	. . . 4 ⊢ ((𝜑 ∧ ((𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆) ∧ ∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦))) → 𝑆 ∈ SAlg)
38		simprl2 1236	. . . 4 ⊢ ((𝜑 ∧ ((𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆) ∧ ∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦))) → ∪ 𝑆 = ∪ 𝑋)
39		simprl3 1237	. . . 4 ⊢ ((𝜑 ∧ ((𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆) ∧ ∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦))) → 𝑋 ⊆ 𝑆)
40		unieq 4887	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → ∪ 𝑦 = ∪ 𝑤)
41	40	eqeq1d 2771	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → (∪ 𝑦 = ∪ 𝑋 ↔ ∪ 𝑤 = ∪ 𝑋))
42		sseq2 3971	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → (𝑋 ⊆ 𝑦 ↔ 𝑋 ⊆ 𝑤))
43	41, 42	anbi12d 643	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) ↔ (∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤)))
44		sseq2 3971	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → (𝑆 ⊆ 𝑦 ↔ 𝑆 ⊆ 𝑤))
45	43, 44	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → (((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦) ↔ ((∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤) → 𝑆 ⊆ 𝑤)))
46	45	cbvralvw 3249	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦) ↔ ∀𝑤 ∈ SAlg ((∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤) → 𝑆 ⊆ 𝑤))
47	46	birani 508	. . . . . . . . 9 ⊢ ((∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦) ∧ 𝑤 ∈ SAlg) → ∀𝑤 ∈ SAlg ((∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤) → 𝑆 ⊆ 𝑤))
48		simpr 489	. . . . . . . . 9 ⊢ ((∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦) ∧ 𝑤 ∈ SAlg) → 𝑤 ∈ SAlg)
49	47, 48	jca 520	. . . . . . . 8 ⊢ ((∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦) ∧ 𝑤 ∈ SAlg) → (∀𝑤 ∈ SAlg ((∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤) → 𝑆 ⊆ 𝑤) ∧ 𝑤 ∈ SAlg))
50	49	3ad2antr1 1205	. . . . . . 7 ⊢ ((∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦) ∧ (𝑤 ∈ SAlg ∧ ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤)) → (∀𝑤 ∈ SAlg ((∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤) → 𝑆 ⊆ 𝑤) ∧ 𝑤 ∈ SAlg))
51		3simpc 1166	. . . . . . . 8 ⊢ ((𝑤 ∈ SAlg ∧ ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤) → (∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤))
52	51	adantl 486	. . . . . . 7 ⊢ ((∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦) ∧ (𝑤 ∈ SAlg ∧ ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤)) → (∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤))
53		rspa 3260	. . . . . . 7 ⊢ ((∀𝑤 ∈ SAlg ((∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤) → 𝑆 ⊆ 𝑤) ∧ 𝑤 ∈ SAlg) → ((∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤) → 𝑆 ⊆ 𝑤))
54	50, 52, 53	sylc 66	. . . . . 6 ⊢ ((∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦) ∧ (𝑤 ∈ SAlg ∧ ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤)) → 𝑆 ⊆ 𝑤)
55	54	adantll 726	. . . . 5 ⊢ ((((𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆) ∧ ∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦)) ∧ (𝑤 ∈ SAlg ∧ ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤)) → 𝑆 ⊆ 𝑤)
56	55	adantll 726	. . . 4 ⊢ (((𝜑 ∧ ((𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆) ∧ ∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦))) ∧ (𝑤 ∈ SAlg ∧ ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤)) → 𝑆 ⊆ 𝑤)
57	36, 37, 38, 39, 56	issalgend 46944	. . 3 ⊢ ((𝜑 ∧ ((𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆) ∧ ∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦))) → (SalGen‘𝑋) = 𝑆)
58	57	ex 417	. 2 ⊢ (𝜑 → (((𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆) ∧ ∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦)) → (SalGen‘𝑋) = 𝑆))
59	35, 58	impbid 215	1 ⊢ (𝜑 → ((SalGen‘𝑋) = 𝑆 ↔ ((𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆) ∧ ∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149  ∀wral 3085   ⊆ wss 3913  ∪ cuni 4876  ‘cfv 6537  SAlgcsalg 46914  SalGencsalgen 46918

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-int 4917  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-iota 6493  df-fun 6539  df-fv 6545  df-salg 46915  df-salgen 46919

This theorem is referenced by:  unisalgen2  46960