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 39841
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 3912 . . . 4 (𝐺 ≠ ∅ ↔ ∃𝑠 𝑠𝐺)
32biimpi 206 . . 3 (𝐺 ≠ ∅ → ∃𝑠 𝑠𝐺)
41, 3syl 17 . 2 (𝜑 → ∃𝑠 𝑠𝐺)
5 nfv 1845 . . 3 𝑠𝜑
6 nfv 1845 . . 3 𝑠 𝐺 = 𝑋
7 intss1 4462 . . . . . . . 8 (𝑠𝐺 𝐺𝑠)
8 uniss 4429 . . . . . . . 8 ( 𝐺𝑠 𝐺 𝑠)
97, 8syl 17 . . . . . . 7 (𝑠𝐺 𝐺 𝑠)
109adantl 482 . . . . . 6 ((𝜑𝑠𝐺) → 𝐺 𝑠)
11 intsaluni.x . . . . . 6 ((𝜑𝑠𝐺) → 𝑠 = 𝑋)
1210, 11sseqtrd 3625 . . . . 5 ((𝜑𝑠𝐺) → 𝐺𝑋)
1311adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑠 = 𝑋)
14 eleq1 2692 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 → (𝑠𝐺𝑡𝐺))
1514anbi2d 739 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑡 → ((𝜑𝑠𝐺) ↔ (𝜑𝑡𝐺)))
16 unieq 4415 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 𝑠 = 𝑡)
1716eqeq1d 2628 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑡 → ( 𝑠 = 𝑋 𝑡 = 𝑋))
1815, 17imbi12d 334 . . . . . . . . . . . . . . . . 17 (𝑠 = 𝑡 → (((𝜑𝑠𝐺) → 𝑠 = 𝑋) ↔ ((𝜑𝑡𝐺) → 𝑡 = 𝑋)))
1918, 11chvarv 2267 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝐺) → 𝑡 = 𝑋)
2019eqcomd 2632 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝐺) → 𝑋 = 𝑡)
2120adantlr 750 . . . . . . . . . . . . . 14 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑋 = 𝑡)
2213, 21eqtrd 2660 . . . . . . . . . . . . 13 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑠 = 𝑡)
23 intsaluni.ga . . . . . . . . . . . . . . . 16 (𝜑𝐺 ⊆ SAlg)
2423sselda 3588 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝐺) → 𝑡 ∈ SAlg)
25 saluni 39838 . . . . . . . . . . . . . . 15 (𝑡 ∈ SAlg → 𝑡𝑡)
2624, 25syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑡𝐺) → 𝑡𝑡)
2726adantlr 750 . . . . . . . . . . . . 13 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑡𝑡)
2822, 27eqeltrd 2704 . . . . . . . . . . . 12 (((𝜑𝑠𝐺) ∧ 𝑡𝐺) → 𝑠𝑡)
2928ralrimiva 2965 . . . . . . . . . . 11 ((𝜑𝑠𝐺) → ∀𝑡𝐺 𝑠𝑡)
30 uniexg 6909 . . . . . . . . . . . . 13 (𝑠𝐺 𝑠 ∈ V)
3130adantl 482 . . . . . . . . . . . 12 ((𝜑𝑠𝐺) → 𝑠 ∈ V)
32 elintg 4453 . . . . . . . . . . . 12 ( 𝑠 ∈ V → ( 𝑠 𝐺 ↔ ∀𝑡𝐺 𝑠𝑡))
3331, 32syl 17 . . . . . . . . . . 11 ((𝜑𝑠𝐺) → ( 𝑠 𝐺 ↔ ∀𝑡𝐺 𝑠𝑡))
3429, 33mpbird 247 . . . . . . . . . 10 ((𝜑𝑠𝐺) → 𝑠 𝐺)
3534adantr 481 . . . . . . . . 9 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑠 𝐺)
36 simpr 477 . . . . . . . . . 10 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑥𝑋)
3711eqcomd 2632 . . . . . . . . . . 11 ((𝜑𝑠𝐺) → 𝑋 = 𝑠)
3837adantr 481 . . . . . . . . . 10 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑋 = 𝑠)
3936, 38eleqtrd 2706 . . . . . . . . 9 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑥 𝑠)
40 eleq2 2693 . . . . . . . . . 10 (𝑦 = 𝑠 → (𝑥𝑦𝑥 𝑠))
4140rspcev 3300 . . . . . . . . 9 (( 𝑠 𝐺𝑥 𝑠) → ∃𝑦 𝐺𝑥𝑦)
4235, 39, 41syl2anc 692 . . . . . . . 8 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → ∃𝑦 𝐺𝑥𝑦)
43 eluni2 4411 . . . . . . . 8 (𝑥 𝐺 ↔ ∃𝑦 𝐺𝑥𝑦)
4442, 43sylibr 224 . . . . . . 7 (((𝜑𝑠𝐺) ∧ 𝑥𝑋) → 𝑥 𝐺)
4544ralrimiva 2965 . . . . . 6 ((𝜑𝑠𝐺) → ∀𝑥𝑋 𝑥 𝐺)
46 dfss3 3578 . . . . . 6 (𝑋 𝐺 ↔ ∀𝑥𝑋 𝑥 𝐺)
4745, 46sylibr 224 . . . . 5 ((𝜑𝑠𝐺) → 𝑋 𝐺)
4812, 47eqssd 3605 . . . 4 ((𝜑𝑠𝐺) → 𝐺 = 𝑋)
4948ex 450 . . 3 (𝜑 → (𝑠𝐺 𝐺 = 𝑋))
505, 6, 49exlimd 2090 . 2 (𝜑 → (∃𝑠 𝑠𝐺 𝐺 = 𝑋))
514, 50mpd 15 1 (𝜑 𝐺 = 𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wex 1701  wcel 1992  wne 2796  wral 2912  wrex 2913  Vcvv 3191  wss 3560  c0 3896   cuni 4407   cint 4445  SAlgcsalg 39822
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-un 6903
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-dif 3563  df-in 3567  df-ss 3574  df-nul 3897  df-pw 4137  df-uni 4408  df-int 4446  df-salg 39823
This theorem is referenced by:  intsal  39842  salgenuni  39849
  Copyright terms: Public domain W3C validator