Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  intsaluni Structured version   Visualization version   GIF version

Theorem intsaluni 44112
Description: The union of an arbitrary intersection of sigma-algebras on the same set 𝑋, is 𝑋. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
intsaluni.ga (𝜑𝐺 ⊆ SAlg)
intsaluni.gn0 (𝜑𝐺 ≠ ∅)
intsaluni.x ((𝜑𝑠𝐺) → 𝑠 = 𝑋)
Assertion
Ref Expression
intsaluni (𝜑 𝐺 = 𝑋)
Distinct variable groups:   𝐺,𝑠   𝑋,𝑠   𝜑,𝑠

Proof of Theorem intsaluni
Dummy variables 𝑡 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1916 . 2 𝑠𝜑
2 nfv 1916 . 2 𝑠 𝐺 = 𝑋
3 intsaluni.gn0 . . 3 (𝜑𝐺 ≠ ∅)
4 n0 4290 . . . 4 (𝐺 ≠ ∅ ↔ ∃𝑠 𝑠𝐺)
54biimpi 215 . . 3 (𝐺 ≠ ∅ → ∃𝑠 𝑠𝐺)
63, 5syl 17 . 2 (𝜑 → ∃𝑠 𝑠𝐺)
7 intss1 4905 . . . . . . 7 (𝑠𝐺 𝐺𝑠)
87unissd 4858 . . . . . 6 (𝑠𝐺 𝐺 𝑠)
98adantl 482 . . . . 5 ((𝜑𝑠𝐺) → 𝐺 𝑠)
10 intsaluni.x . . . . 5 ((𝜑𝑠𝐺) → 𝑠 = 𝑋)
119, 10sseqtrd 3970 . . . 4 ((𝜑𝑠𝐺) → 𝐺𝑋)
1210adantr 481 . . . . . . . . . . 11 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑠 = 𝑋)
13 eleq1w 2820 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑡 → (𝑠𝐺𝑡𝐺))
1413anbi2d 629 . . . . . . . . . . . . . . 15 (𝑠 = 𝑡 → ((𝜑𝑠𝐺) ↔ (𝜑𝑡𝐺)))
15 unieq 4859 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑡 𝑠 = 𝑡)
1615eqeq1d 2739 . . . . . . . . . . . . . . 15 (𝑠 = 𝑡 → ( 𝑠 = 𝑋 𝑡 = 𝑋))
1714, 16imbi12d 344 . . . . . . . . . . . . . 14 (𝑠 = 𝑡 → (((𝜑𝑠𝐺) → 𝑠 = 𝑋) ↔ ((𝜑𝑡𝐺) → 𝑡 = 𝑋)))
1817, 10chvarvv 2001 . . . . . . . . . . . . 13 ((𝜑𝑡𝐺) → 𝑡 = 𝑋)
1918eqcomd 2743 . . . . . . . . . . . 12 ((𝜑𝑡𝐺) → 𝑋 = 𝑡)
2019adantlr 712 . . . . . . . . . . 11 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑋 = 𝑡)
2112, 20eqtrd 2777 . . . . . . . . . 10 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑠 = 𝑡)
22 intsaluni.ga . . . . . . . . . . . . 13 (𝜑𝐺 ⊆ SAlg)
2322sselda 3930 . . . . . . . . . . . 12 ((𝜑𝑡𝐺) → 𝑡 ∈ SAlg)
24 saluni 44109 . . . . . . . . . . . 12 (𝑡 ∈ SAlg → 𝑡𝑡)
2523, 24syl 17 . . . . . . . . . . 11 ((𝜑𝑡𝐺) → 𝑡𝑡)
2625adantlr 712 . . . . . . . . . 10 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑡𝑡)
2721, 26eqeltrd 2838 . . . . . . . . 9 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑠𝑡)
2827ralrimiva 3140 . . . . . . . 8 ((𝜑𝑠𝐺) → ∀𝑡𝐺 𝑠𝑡)
29 uniexg 7631 . . . . . . . . . 10 (𝑠𝐺 𝑠 ∈ V)
3029adantl 482 . . . . . . . . 9 ((𝜑𝑠𝐺) → 𝑠 ∈ V)
31 elintg 4898 . . . . . . . . 9 ( 𝑠 ∈ V → ( 𝑠 𝐺 ↔ ∀𝑡𝐺 𝑠𝑡))
3230, 31syl 17 . . . . . . . 8 ((𝜑𝑠𝐺) → ( 𝑠 𝐺 ↔ ∀𝑡𝐺 𝑠𝑡))
3328, 32mpbird 256 . . . . . . 7 ((𝜑𝑠𝐺) → 𝑠 𝐺)
3433adantr 481 . . . . . 6 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑠 𝐺)
35 simpr 485 . . . . . . 7 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑥𝑋)
3610eqcomd 2743 . . . . . . . 8 ((𝜑𝑠𝐺) → 𝑋 = 𝑠)
3736adantr 481 . . . . . . 7 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑋 = 𝑠)
3835, 37eleqtrd 2840 . . . . . 6 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑥 𝑠)
39 eleq2 2826 . . . . . . 7 (𝑦 = 𝑠 → (𝑥𝑦𝑥 𝑠))
4039rspcev 3570 . . . . . 6 (( 𝑠 𝐺𝑥 𝑠) → ∃𝑦 𝐺𝑥𝑦)
4134, 38, 40syl2anc 584 . . . . 5 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → ∃𝑦 𝐺𝑥𝑦)
42 eluni2 4852 . . . . 5 (𝑥 𝐺 ↔ ∃𝑦 𝐺𝑥𝑦)
4341, 42sylibr 233 . . . 4 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑥 𝐺)
4411, 43eqelssd 3951 . . 3 ((𝜑𝑠𝐺) → 𝐺 = 𝑋)
4544ex 413 . 2 (𝜑 → (𝑠𝐺 𝐺 = 𝑋))
461, 2, 6, 45exlimimdd 2211 1 (𝜑 𝐺 = 𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1540  wex 1780  wcel 2105  wne 2941  wral 3062  wrex 3071  Vcvv 3441  wss 3896  c0 4266   cuni 4848   cint 4890  SAlgcsalg 44093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-12 2170  ax-ext 2708  ax-sep 5236  ax-un 7626
This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-dif 3899  df-in 3903  df-ss 3913  df-nul 4267  df-pw 4545  df-uni 4849  df-int 4891  df-salg 44094
This theorem is referenced by:  intsal  44113  salgenuni  44120
  Copyright terms: Public domain W3C validator