Metamath Proof Explorer


Theorem intsaluni

Description: The union of an arbitrary intersection of sigma-algebras on the same set X , is X . (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses intsaluni.ga ( 𝜑𝐺 ⊆ SAlg )
intsaluni.gn0 ( 𝜑𝐺 ≠ ∅ )
intsaluni.x ( ( 𝜑𝑠𝐺 ) → 𝑠 = 𝑋 )
Assertion intsaluni ( 𝜑 𝐺 = 𝑋 )

Proof

Step Hyp Ref Expression
1 intsaluni.ga ( 𝜑𝐺 ⊆ SAlg )
2 intsaluni.gn0 ( 𝜑𝐺 ≠ ∅ )
3 intsaluni.x ( ( 𝜑𝑠𝐺 ) → 𝑠 = 𝑋 )
4 nfv 𝑠 𝜑
5 nfv 𝑠 𝐺 = 𝑋
6 n0 ( 𝐺 ≠ ∅ ↔ ∃ 𝑠 𝑠𝐺 )
7 6 biimpi ( 𝐺 ≠ ∅ → ∃ 𝑠 𝑠𝐺 )
8 2 7 syl ( 𝜑 → ∃ 𝑠 𝑠𝐺 )
9 intss1 ( 𝑠𝐺 𝐺𝑠 )
10 9 unissd ( 𝑠𝐺 𝐺 𝑠 )
11 10 adantl ( ( 𝜑𝑠𝐺 ) → 𝐺 𝑠 )
12 11 3 sseqtrd ( ( 𝜑𝑠𝐺 ) → 𝐺𝑋 )
13 3 adantr ( ( ( 𝜑𝑠𝐺 ) ∧ 𝑡𝐺 ) → 𝑠 = 𝑋 )
14 eleq1w ( 𝑠 = 𝑡 → ( 𝑠𝐺𝑡𝐺 ) )
15 14 anbi2d ( 𝑠 = 𝑡 → ( ( 𝜑𝑠𝐺 ) ↔ ( 𝜑𝑡𝐺 ) ) )
16 unieq ( 𝑠 = 𝑡 𝑠 = 𝑡 )
17 16 eqeq1d ( 𝑠 = 𝑡 → ( 𝑠 = 𝑋 𝑡 = 𝑋 ) )
18 15 17 imbi12d ( 𝑠 = 𝑡 → ( ( ( 𝜑𝑠𝐺 ) → 𝑠 = 𝑋 ) ↔ ( ( 𝜑𝑡𝐺 ) → 𝑡 = 𝑋 ) ) )
19 18 3 chvarvv ( ( 𝜑𝑡𝐺 ) → 𝑡 = 𝑋 )
20 19 eqcomd ( ( 𝜑𝑡𝐺 ) → 𝑋 = 𝑡 )
21 20 adantlr ( ( ( 𝜑𝑠𝐺 ) ∧ 𝑡𝐺 ) → 𝑋 = 𝑡 )
22 13 21 eqtrd ( ( ( 𝜑𝑠𝐺 ) ∧ 𝑡𝐺 ) → 𝑠 = 𝑡 )
23 1 sselda ( ( 𝜑𝑡𝐺 ) → 𝑡 ∈ SAlg )
24 saluni ( 𝑡 ∈ SAlg → 𝑡𝑡 )
25 23 24 syl ( ( 𝜑𝑡𝐺 ) → 𝑡𝑡 )
26 25 adantlr ( ( ( 𝜑𝑠𝐺 ) ∧ 𝑡𝐺 ) → 𝑡𝑡 )
27 22 26 eqeltrd ( ( ( 𝜑𝑠𝐺 ) ∧ 𝑡𝐺 ) → 𝑠𝑡 )
28 27 ralrimiva ( ( 𝜑𝑠𝐺 ) → ∀ 𝑡𝐺 𝑠𝑡 )
29 uniexg ( 𝑠𝐺 𝑠 ∈ V )
30 29 adantl ( ( 𝜑𝑠𝐺 ) → 𝑠 ∈ V )
31 elintg ( 𝑠 ∈ V → ( 𝑠 𝐺 ↔ ∀ 𝑡𝐺 𝑠𝑡 ) )
32 30 31 syl ( ( 𝜑𝑠𝐺 ) → ( 𝑠 𝐺 ↔ ∀ 𝑡𝐺 𝑠𝑡 ) )
33 28 32 mpbird ( ( 𝜑𝑠𝐺 ) → 𝑠 𝐺 )
34 33 adantr ( ( ( 𝜑𝑠𝐺 ) ∧ 𝑥𝑋 ) → 𝑠 𝐺 )
35 simpr ( ( ( 𝜑𝑠𝐺 ) ∧ 𝑥𝑋 ) → 𝑥𝑋 )
36 3 eqcomd ( ( 𝜑𝑠𝐺 ) → 𝑋 = 𝑠 )
37 36 adantr ( ( ( 𝜑𝑠𝐺 ) ∧ 𝑥𝑋 ) → 𝑋 = 𝑠 )
38 35 37 eleqtrd ( ( ( 𝜑𝑠𝐺 ) ∧ 𝑥𝑋 ) → 𝑥 𝑠 )
39 eleq2 ( 𝑦 = 𝑠 → ( 𝑥𝑦𝑥 𝑠 ) )
40 39 rspcev ( ( 𝑠 𝐺𝑥 𝑠 ) → ∃ 𝑦 𝐺 𝑥𝑦 )
41 34 38 40 syl2anc ( ( ( 𝜑𝑠𝐺 ) ∧ 𝑥𝑋 ) → ∃ 𝑦 𝐺 𝑥𝑦 )
42 eluni2 ( 𝑥 𝐺 ↔ ∃ 𝑦 𝐺 𝑥𝑦 )
43 41 42 sylibr ( ( ( 𝜑𝑠𝐺 ) ∧ 𝑥𝑋 ) → 𝑥 𝐺 )
44 12 43 eqelssd ( ( 𝜑𝑠𝐺 ) → 𝐺 = 𝑋 )
45 44 ex ( 𝜑 → ( 𝑠𝐺 𝐺 = 𝑋 ) )
46 4 5 8 45 exlimimdd ( 𝜑 𝐺 = 𝑋 )