Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion dfsalgen2 ( 𝜑 → ( ( SalGen ‘ 𝑋 ) = 𝑆 ↔ ( ( 𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆 ) ∧ ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 dfsalgen2.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2 id ⊢ ( ( SalGen ‘ 𝑋 ) = 𝑆 → ( SalGen ‘ 𝑋 ) = 𝑆 )
3 2 eqcomd ⊢ ( ( SalGen ‘ 𝑋 ) = 𝑆 → 𝑆 = ( SalGen ‘ 𝑋 ) )
4 3 adantl ⊢ ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) → 𝑆 = ( SalGen ‘ 𝑋 ) )
5 salgencl ⊢ ( 𝑋 ∈ 𝑉 → ( SalGen ‘ 𝑋 ) ∈ SAlg )
6 1 5 syl ⊢ ( 𝜑 → ( SalGen ‘ 𝑋 ) ∈ SAlg )
7 6 adantr ⊢ ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) → ( SalGen ‘ 𝑋 ) ∈ SAlg )
8 4 7 eqeltrd ⊢ ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) → 𝑆 ∈ SAlg )
9 unieq ⊢ ( ( SalGen ‘ 𝑋 ) = 𝑆 → ∪ ( SalGen ‘ 𝑋 ) = ∪ 𝑆 )
10 9 adantl ⊢ ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) → ∪ ( SalGen ‘ 𝑋 ) = ∪ 𝑆 )
11 1 adantr ⊢ ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) → 𝑋 ∈ 𝑉 )
12 eqid ⊢ ( SalGen ‘ 𝑋 ) = ( SalGen ‘ 𝑋 )
13 eqid ⊢ ∪ 𝑋 = ∪ 𝑋
14 11 12 13 salgenuni ⊢ ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) → ∪ ( SalGen ‘ 𝑋 ) = ∪ 𝑋 )
15 10 14 eqtr3d ⊢ ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) → ∪ 𝑆 = ∪ 𝑋 )
16 12 sssalgen ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ⊆ ( SalGen ‘ 𝑋 ) )
17 11 16 syl ⊢ ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) → 𝑋 ⊆ ( SalGen ‘ 𝑋 ) )
18 simpr ⊢ ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) → ( SalGen ‘ 𝑋 ) = 𝑆 )
19 17 18 sseqtrd ⊢ ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) → 𝑋 ⊆ 𝑆 )
20 8 15 19 3jca ⊢ ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) → ( 𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆 ) )
21 4 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) ∧ 𝑦 ∈ SAlg ) ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 = ( SalGen ‘ 𝑋 ) )
22 21 adantrl ⊢ ( ( ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) ∧ 𝑦 ∈ SAlg ) ∧ ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) ) → 𝑆 = ( SalGen ‘ 𝑋 ) )
23 11 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) ∧ 𝑦 ∈ SAlg ) ∧ 𝑋 ⊆ 𝑦 ) → 𝑋 ∈ 𝑉 )
24 23 adantrl ⊢ ( ( ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) ∧ 𝑦 ∈ SAlg ) ∧ ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) ) → 𝑋 ∈ 𝑉 )
25 simplr ⊢ ( ( ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) ∧ 𝑦 ∈ SAlg ) ∧ 𝑋 ⊆ 𝑦 ) → 𝑦 ∈ SAlg )
26 25 adantrl ⊢ ( ( ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) ∧ 𝑦 ∈ SAlg ) ∧ ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) ) → 𝑦 ∈ SAlg )
27 simpr ⊢ ( ( ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) ∧ 𝑦 ∈ SAlg ) ∧ 𝑋 ⊆ 𝑦 ) → 𝑋 ⊆ 𝑦 )
28 27 adantrl ⊢ ( ( ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) ∧ 𝑦 ∈ SAlg ) ∧ ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) ) → 𝑋 ⊆ 𝑦 )
29 simprl ⊢ ( ( ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) ∧ 𝑦 ∈ SAlg ) ∧ ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) ) → ∪ 𝑦 = ∪ 𝑋 )
30 24 12 26 28 29 salgenss ⊢ ( ( ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) ∧ 𝑦 ∈ SAlg ) ∧ ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) ) → ( SalGen ‘ 𝑋 ) ⊆ 𝑦 )
31 22 30 eqsstrd ⊢ ( ( ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) ∧ 𝑦 ∈ SAlg ) ∧ ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) ) → 𝑆 ⊆ 𝑦 )
32 31 ex ⊢ ( ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) ∧ 𝑦 ∈ SAlg ) → ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) )
33 32 ralrimiva ⊢ ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) → ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) )
34 20 33 jca ⊢ ( ( 𝜑 ∧ ( SalGen ‘ 𝑋 ) = 𝑆 ) → ( ( 𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆 ) ∧ ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) ) )
35 34 ex ⊢ ( 𝜑 → ( ( SalGen ‘ 𝑋 ) = 𝑆 → ( ( 𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆 ) ∧ ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) ) ) )
36 1 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆 ) ∧ ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) ) ) → 𝑋 ∈ 𝑉 )
37 simprl1 ⊢ ( ( 𝜑 ∧ ( ( 𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆 ) ∧ ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) ) ) → 𝑆 ∈ SAlg )
38 simprl2 ⊢ ( ( 𝜑 ∧ ( ( 𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆 ) ∧ ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) ) ) → ∪ 𝑆 = ∪ 𝑋 )
39 simprl3 ⊢ ( ( 𝜑 ∧ ( ( 𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆 ) ∧ ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) ) ) → 𝑋 ⊆ 𝑆 )
40 unieq ⊢ ( 𝑦 = 𝑤 → ∪ 𝑦 = ∪ 𝑤 )
41 40 eqeq1d ⊢ ( 𝑦 = 𝑤 → ( ∪ 𝑦 = ∪ 𝑋 ↔ ∪ 𝑤 = ∪ 𝑋 ) )
42 sseq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑋 ⊆ 𝑦 ↔ 𝑋 ⊆ 𝑤 ) )
43 41 42 anbi12d ⊢ ( 𝑦 = 𝑤 → ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) ↔ ( ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤 ) ) )
44 sseq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑆 ⊆ 𝑦 ↔ 𝑆 ⊆ 𝑤 ) )
45 43 44 imbi12d ⊢ ( 𝑦 = 𝑤 → ( ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) ↔ ( ( ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤 ) → 𝑆 ⊆ 𝑤 ) ) )
46 45 cbvralvw ⊢ ( ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) ↔ ∀ 𝑤 ∈ SAlg ( ( ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤 ) → 𝑆 ⊆ 𝑤 ) )
47 46 biimpi ⊢ ( ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) → ∀ 𝑤 ∈ SAlg ( ( ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤 ) → 𝑆 ⊆ 𝑤 ) )
48 47 adantr ⊢ ( ( ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) ∧ 𝑤 ∈ SAlg ) → ∀ 𝑤 ∈ SAlg ( ( ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤 ) → 𝑆 ⊆ 𝑤 ) )
49 simpr ⊢ ( ( ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) ∧ 𝑤 ∈ SAlg ) → 𝑤 ∈ SAlg )
50 48 49 jca ⊢ ( ( ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) ∧ 𝑤 ∈ SAlg ) → ( ∀ 𝑤 ∈ SAlg ( ( ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤 ) → 𝑆 ⊆ 𝑤 ) ∧ 𝑤 ∈ SAlg ) )
51 50 3ad2antr1 ⊢ ( ( ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) ∧ ( 𝑤 ∈ SAlg ∧ ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤 ) ) → ( ∀ 𝑤 ∈ SAlg ( ( ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤 ) → 𝑆 ⊆ 𝑤 ) ∧ 𝑤 ∈ SAlg ) )
52 3simpc ⊢ ( ( 𝑤 ∈ SAlg ∧ ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤 ) → ( ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤 ) )
53 52 adantl ⊢ ( ( ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) ∧ ( 𝑤 ∈ SAlg ∧ ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤 ) ) → ( ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤 ) )
54 rspa ⊢ ( ( ∀ 𝑤 ∈ SAlg ( ( ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤 ) → 𝑆 ⊆ 𝑤 ) ∧ 𝑤 ∈ SAlg ) → ( ( ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤 ) → 𝑆 ⊆ 𝑤 ) )
55 51 53 54 sylc ⊢ ( ( ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) ∧ ( 𝑤 ∈ SAlg ∧ ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤 ) ) → 𝑆 ⊆ 𝑤 )
56 55 adantll ⊢ ( ( ( ( 𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆 ) ∧ ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) ) ∧ ( 𝑤 ∈ SAlg ∧ ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤 ) ) → 𝑆 ⊆ 𝑤 )
57 56 adantll ⊢ ( ( ( 𝜑 ∧ ( ( 𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆 ) ∧ ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) ) ) ∧ ( 𝑤 ∈ SAlg ∧ ∪ 𝑤 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑤 ) ) → 𝑆 ⊆ 𝑤 )
58 36 37 38 39 57 issalgend ⊢ ( ( 𝜑 ∧ ( ( 𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆 ) ∧ ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) ) ) → ( SalGen ‘ 𝑋 ) = 𝑆 )
59 58 ex ⊢ ( 𝜑 → ( ( ( 𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆 ) ∧ ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) ) → ( SalGen ‘ 𝑋 ) = 𝑆 ) )
60 35 59 impbid ⊢ ( 𝜑 → ( ( SalGen ‘ 𝑋 ) = 𝑆 ↔ ( ( 𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆 ) ∧ ∀ 𝑦 ∈ SAlg ( ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) → 𝑆 ⊆ 𝑦 ) ) ) )