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 42835
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 4293 . . . 4 (𝐺 ≠ ∅ ↔ ∃𝑠 𝑠𝐺)
54biimpi 219 . . 3 (𝐺 ≠ ∅ → ∃𝑠 𝑠𝐺)
63, 5syl 17 . 2 (𝜑 → ∃𝑠 𝑠𝐺)
7 intss1 4878 . . . . . . 7 (𝑠𝐺 𝐺𝑠)
87unissd 4835 . . . . . 6 (𝑠𝐺 𝐺 𝑠)
98adantl 485 . . . . 5 ((𝜑𝑠𝐺) → 𝐺 𝑠)
10 intsaluni.x . . . . 5 ((𝜑𝑠𝐺) → 𝑠 = 𝑋)
119, 10sseqtrd 3993 . . . 4 ((𝜑𝑠𝐺) → 𝐺𝑋)
1210adantr 484 . . . . . . . . . . 11 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑠 = 𝑋)
13 eleq1w 2898 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑡 → (𝑠𝐺𝑡𝐺))
1413anbi2d 631 . . . . . . . . . . . . . . 15 (𝑠 = 𝑡 → ((𝜑𝑠𝐺) ↔ (𝜑𝑡𝐺)))
15 unieq 4836 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑡 𝑠 = 𝑡)
1615eqeq1d 2826 . . . . . . . . . . . . . . 15 (𝑠 = 𝑡 → ( 𝑠 = 𝑋 𝑡 = 𝑋))
1714, 16imbi12d 348 . . . . . . . . . . . . . 14 (𝑠 = 𝑡 → (((𝜑𝑠𝐺) → 𝑠 = 𝑋) ↔ ((𝜑𝑡𝐺) → 𝑡 = 𝑋)))
1817, 10chvarvv 2006 . . . . . . . . . . . . 13 ((𝜑𝑡𝐺) → 𝑡 = 𝑋)
1918eqcomd 2830 . . . . . . . . . . . 12 ((𝜑𝑡𝐺) → 𝑋 = 𝑡)
2019adantlr 714 . . . . . . . . . . 11 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑋 = 𝑡)
2112, 20eqtrd 2859 . . . . . . . . . 10 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑠 = 𝑡)
22 intsaluni.ga . . . . . . . . . . . . 13 (𝜑𝐺 ⊆ SAlg)
2322sselda 3953 . . . . . . . . . . . 12 ((𝜑𝑡𝐺) → 𝑡 ∈ SAlg)
24 saluni 42832 . . . . . . . . . . . 12 (𝑡 ∈ SAlg → 𝑡𝑡)
2523, 24syl 17 . . . . . . . . . . 11 ((𝜑𝑡𝐺) → 𝑡𝑡)
2625adantlr 714 . . . . . . . . . 10 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑡𝑡)
2721, 26eqeltrd 2916 . . . . . . . . 9 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑠𝑡)
2827ralrimiva 3177 . . . . . . . 8 ((𝜑𝑠𝐺) → ∀𝑡𝐺 𝑠𝑡)
29 uniexg 7457 . . . . . . . . . 10 (𝑠𝐺 𝑠 ∈ V)
3029adantl 485 . . . . . . . . 9 ((𝜑𝑠𝐺) → 𝑠 ∈ V)
31 elintg 4871 . . . . . . . . 9 ( 𝑠 ∈ V → ( 𝑠 𝐺 ↔ ∀𝑡𝐺 𝑠𝑡))
3230, 31syl 17 . . . . . . . 8 ((𝜑𝑠𝐺) → ( 𝑠 𝐺 ↔ ∀𝑡𝐺 𝑠𝑡))
3328, 32mpbird 260 . . . . . . 7 ((𝜑𝑠𝐺) → 𝑠 𝐺)
3433adantr 484 . . . . . 6 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑠 𝐺)
35 simpr 488 . . . . . . 7 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑥𝑋)
3610eqcomd 2830 . . . . . . . 8 ((𝜑𝑠𝐺) → 𝑋 = 𝑠)
3736adantr 484 . . . . . . 7 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑋 = 𝑠)
3835, 37eleqtrd 2918 . . . . . 6 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑥 𝑠)
39 eleq2 2904 . . . . . . 7 (𝑦 = 𝑠 → (𝑥𝑦𝑥 𝑠))
4039rspcev 3609 . . . . . 6 (( 𝑠 𝐺𝑥 𝑠) → ∃𝑦 𝐺𝑥𝑦)
4134, 38, 40syl2anc 587 . . . . 5 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → ∃𝑦 𝐺𝑥𝑦)
42 eluni2 4829 . . . . 5 (𝑥 𝐺 ↔ ∃𝑦 𝐺𝑥𝑦)
4341, 42sylibr 237 . . . 4 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑥 𝐺)
4411, 43eqelssd 3974 . . 3 ((𝜑𝑠𝐺) → 𝐺 = 𝑋)
4544ex 416 . 2 (𝜑 → (𝑠𝐺 𝐺 = 𝑋))
461, 2, 6, 45exlimimdd 2221 1 (𝜑 𝐺 = 𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wex 1781  wcel 2115  wne 3014  wral 3133  wrex 3134  Vcvv 3480  wss 3919  c0 4276   cuni 4825   cint 4863  SAlgcsalg 42816
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-un 7452
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-dif 3922  df-in 3926  df-ss 3936  df-nul 4277  df-pw 4524  df-uni 4826  df-int 4864  df-salg 42817
This theorem is referenced by:  intsal  42836  salgenuni  42843
  Copyright terms: Public domain W3C validator