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 44560
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 1917 . 2 𝑠𝜑
2 nfv 1917 . 2 𝑠 𝐺 = 𝑋
3 intsaluni.gn0 . . 3 (𝜑𝐺 ≠ ∅)
4 n0 4306 . . . 4 (𝐺 ≠ ∅ ↔ ∃𝑠 𝑠𝐺)
54biimpi 215 . . 3 (𝐺 ≠ ∅ → ∃𝑠 𝑠𝐺)
63, 5syl 17 . 2 (𝜑 → ∃𝑠 𝑠𝐺)
7 intss1 4924 . . . . . . 7 (𝑠𝐺 𝐺𝑠)
87unissd 4875 . . . . . 6 (𝑠𝐺 𝐺 𝑠)
98adantl 482 . . . . 5 ((𝜑𝑠𝐺) → 𝐺 𝑠)
10 intsaluni.x . . . . 5 ((𝜑𝑠𝐺) → 𝑠 = 𝑋)
119, 10sseqtrd 3984 . . . 4 ((𝜑𝑠𝐺) → 𝐺𝑋)
1210adantr 481 . . . . . . . . . . 11 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑠 = 𝑋)
13 eleq1w 2820 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑡 → (𝑠𝐺𝑡𝐺))
1413anbi2d 629 . . . . . . . . . . . . . . 15 (𝑠 = 𝑡 → ((𝜑𝑠𝐺) ↔ (𝜑𝑡𝐺)))
15 unieq 4876 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑡 𝑠 = 𝑡)
1615eqeq1d 2738 . . . . . . . . . . . . . . 15 (𝑠 = 𝑡 → ( 𝑠 = 𝑋 𝑡 = 𝑋))
1714, 16imbi12d 344 . . . . . . . . . . . . . 14 (𝑠 = 𝑡 → (((𝜑𝑠𝐺) → 𝑠 = 𝑋) ↔ ((𝜑𝑡𝐺) → 𝑡 = 𝑋)))
1817, 10chvarvv 2002 . . . . . . . . . . . . 13 ((𝜑𝑡𝐺) → 𝑡 = 𝑋)
1918eqcomd 2742 . . . . . . . . . . . 12 ((𝜑𝑡𝐺) → 𝑋 = 𝑡)
2019adantlr 713 . . . . . . . . . . 11 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑋 = 𝑡)
2112, 20eqtrd 2776 . . . . . . . . . 10 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑠 = 𝑡)
22 intsaluni.ga . . . . . . . . . . . . 13 (𝜑𝐺 ⊆ SAlg)
2322sselda 3944 . . . . . . . . . . . 12 ((𝜑𝑡𝐺) → 𝑡 ∈ SAlg)
24 saluni 44556 . . . . . . . . . . . 12 (𝑡 ∈ SAlg → 𝑡𝑡)
2523, 24syl 17 . . . . . . . . . . 11 ((𝜑𝑡𝐺) → 𝑡𝑡)
2625adantlr 713 . . . . . . . . . 10 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑡𝑡)
2721, 26eqeltrd 2838 . . . . . . . . 9 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑠𝑡)
2827ralrimiva 3143 . . . . . . . 8 ((𝜑𝑠𝐺) → ∀𝑡𝐺 𝑠𝑡)
29 uniexg 7677 . . . . . . . . . 10 (𝑠𝐺 𝑠 ∈ V)
3029adantl 482 . . . . . . . . 9 ((𝜑𝑠𝐺) → 𝑠 ∈ V)
31 elintg 4915 . . . . . . . . 9 ( 𝑠 ∈ V → ( 𝑠 𝐺 ↔ ∀𝑡𝐺 𝑠𝑡))
3230, 31syl 17 . . . . . . . 8 ((𝜑𝑠𝐺) → ( 𝑠 𝐺 ↔ ∀𝑡𝐺 𝑠𝑡))
3328, 32mpbird 256 . . . . . . 7 ((𝜑𝑠𝐺) → 𝑠 𝐺)
3433adantr 481 . . . . . 6 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑠 𝐺)
35 simpr 485 . . . . . . 7 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑥𝑋)
3610eqcomd 2742 . . . . . . . 8 ((𝜑𝑠𝐺) → 𝑋 = 𝑠)
3736adantr 481 . . . . . . 7 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑋 = 𝑠)
3835, 37eleqtrd 2840 . . . . . 6 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑥 𝑠)
39 eleq2 2826 . . . . . . 7 (𝑦 = 𝑠 → (𝑥𝑦𝑥 𝑠))
4039rspcev 3581 . . . . . 6 (( 𝑠 𝐺𝑥 𝑠) → ∃𝑦 𝐺𝑥𝑦)
4134, 38, 40syl2anc 584 . . . . 5 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → ∃𝑦 𝐺𝑥𝑦)
42 eluni2 4869 . . . . 5 (𝑥 𝐺 ↔ ∃𝑦 𝐺𝑥𝑦)
4341, 42sylibr 233 . . . 4 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑥 𝐺)
4411, 43eqelssd 3965 . . 3 ((𝜑𝑠𝐺) → 𝐺 = 𝑋)
4544ex 413 . 2 (𝜑 → (𝑠𝐺 𝐺 = 𝑋))
461, 2, 6, 45exlimimdd 2212 1 (𝜑 𝐺 = 𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wex 1781  wcel 2106  wne 2943  wral 3064  wrex 3073  Vcvv 3445  wss 3910  c0 4282   cuni 4865   cint 4907  SAlgcsalg 44539
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-in 3917  df-ss 3927  df-nul 4283  df-pw 4562  df-uni 4866  df-int 4908  df-salg 44540
This theorem is referenced by:  intsal  44561  salgenuni  44568
  Copyright terms: Public domain W3C validator