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 40865
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 intsaluni.gn0 . . 3 (𝜑𝐺 ≠ ∅)
2 n0 3964 . . . 4 (𝐺 ≠ ∅ ↔ ∃𝑠 𝑠𝐺)
32biimpi 206 . . 3 (𝐺 ≠ ∅ → ∃𝑠 𝑠𝐺)
41, 3syl 17 . 2 (𝜑 → ∃𝑠 𝑠𝐺)
5 nfv 1883 . . 3 𝑠𝜑
6 nfv 1883 . . 3 𝑠 𝐺 = 𝑋
7 intss1 4524 . . . . . . . 8 (𝑠𝐺 𝐺𝑠)
8 uniss 4490 . . . . . . . 8 ( 𝐺𝑠 𝐺 𝑠)
97, 8syl 17 . . . . . . 7 (𝑠𝐺 𝐺 𝑠)
109adantl 481 . . . . . 6 ((𝜑𝑠𝐺) → 𝐺 𝑠)
11 intsaluni.x . . . . . 6 ((𝜑𝑠𝐺) → 𝑠 = 𝑋)
1210, 11sseqtrd 3674 . . . . 5 ((𝜑𝑠𝐺) → 𝐺𝑋)
1311adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑠 = 𝑋)
14 eleq1 2718 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 → (𝑠𝐺𝑡𝐺))
1514anbi2d 740 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑡 → ((𝜑𝑠𝐺) ↔ (𝜑𝑡𝐺)))
16 unieq 4476 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 𝑠 = 𝑡)
1716eqeq1d 2653 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑡 → ( 𝑠 = 𝑋 𝑡 = 𝑋))
1815, 17imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑠 = 𝑡 → (((𝜑𝑠𝐺) → 𝑠 = 𝑋) ↔ ((𝜑𝑡𝐺) → 𝑡 = 𝑋)))
1918, 11chvarv 2299 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝐺) → 𝑡 = 𝑋)
2019eqcomd 2657 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝐺) → 𝑋 = 𝑡)
2120adantlr 751 . . . . . . . . . . . . . 14 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑋 = 𝑡)
2213, 21eqtrd 2685 . . . . . . . . . . . . 13 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑠 = 𝑡)
23 intsaluni.ga . . . . . . . . . . . . . . . 16 (𝜑𝐺 ⊆ SAlg)
2423sselda 3636 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝐺) → 𝑡 ∈ SAlg)
25 saluni 40862 . . . . . . . . . . . . . . 15 (𝑡 ∈ SAlg → 𝑡𝑡)
2624, 25syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑡𝐺) → 𝑡𝑡)
2726adantlr 751 . . . . . . . . . . . . 13 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑡𝑡)
2822, 27eqeltrd 2730 . . . . . . . . . . . 12 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑠𝑡)
2928ralrimiva 2995 . . . . . . . . . . 11 ((𝜑𝑠𝐺) → ∀𝑡𝐺 𝑠𝑡)
30 uniexg 6997 . . . . . . . . . . . . 13 (𝑠𝐺 𝑠 ∈ V)
3130adantl 481 . . . . . . . . . . . 12 ((𝜑𝑠𝐺) → 𝑠 ∈ V)
32 elintg 4515 . . . . . . . . . . . 12 ( 𝑠 ∈ V → ( 𝑠 𝐺 ↔ ∀𝑡𝐺 𝑠𝑡))
3331, 32syl 17 . . . . . . . . . . 11 ((𝜑𝑠𝐺) → ( 𝑠 𝐺 ↔ ∀𝑡𝐺 𝑠𝑡))
3429, 33mpbird 247 . . . . . . . . . 10 ((𝜑𝑠𝐺) → 𝑠 𝐺)
3534adantr 480 . . . . . . . . 9 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑠 𝐺)
36 simpr 476 . . . . . . . . . 10 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑥𝑋)
3711eqcomd 2657 . . . . . . . . . . 11 ((𝜑𝑠𝐺) → 𝑋 = 𝑠)
3837adantr 480 . . . . . . . . . 10 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑋 = 𝑠)
3936, 38eleqtrd 2732 . . . . . . . . 9 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑥 𝑠)
40 eleq2 2719 . . . . . . . . . 10 (𝑦 = 𝑠 → (𝑥𝑦𝑥 𝑠))
4140rspcev 3340 . . . . . . . . 9 (( 𝑠 𝐺𝑥 𝑠) → ∃𝑦 𝐺𝑥𝑦)
4235, 39, 41syl2anc 694 . . . . . . . 8 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → ∃𝑦 𝐺𝑥𝑦)
43 eluni2 4472 . . . . . . . 8 (𝑥 𝐺 ↔ ∃𝑦 𝐺𝑥𝑦)
4442, 43sylibr 224 . . . . . . 7 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑥 𝐺)
4544ralrimiva 2995 . . . . . 6 ((𝜑𝑠𝐺) → ∀𝑥𝑋 𝑥 𝐺)
46 dfss3 3625 . . . . . 6 (𝑋 𝐺 ↔ ∀𝑥𝑋 𝑥 𝐺)
4745, 46sylibr 224 . . . . 5 ((𝜑𝑠𝐺) → 𝑋 𝐺)
4812, 47eqssd 3653 . . . 4 ((𝜑𝑠𝐺) → 𝐺 = 𝑋)
4948ex 449 . . 3 (𝜑 → (𝑠𝐺 𝐺 = 𝑋))
505, 6, 49exlimd 2125 . 2 (𝜑 → (∃𝑠 𝑠𝐺 𝐺 = 𝑋))
514, 50mpd 15 1 (𝜑 𝐺 = 𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wex 1744  wcel 2030  wne 2823  wral 2941  wrex 2942  Vcvv 3231  wss 3607  c0 3948   cuni 4468   cint 4507  SAlgcsalg 40846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-in 3614  df-ss 3621  df-nul 3949  df-pw 4193  df-uni 4469  df-int 4508  df-salg 40847
This theorem is referenced by:  intsal  40866  salgenuni  40873
  Copyright terms: Public domain W3C validator