Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-0int Structured version   Visualization version   GIF version

Theorem bj-0int 33357
 Description: If 𝐴 is a collection of subsets of 𝑋, like a topology, two equivalent ways to say that arbitrary intersections of elements of 𝐴 relative to 𝑋 belong to some class 𝐵 (in typical applications, 𝐴 itself). (Contributed by BJ, 7-Dec-2021.)
Assertion
Ref Expression
bj-0int (𝐴 ⊆ 𝒫 𝑋 → ((𝑋𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵) ↔ ∀𝑥 ∈ 𝒫 𝐴(𝑋 𝑥) ∈ 𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝑋

Proof of Theorem bj-0int
StepHypRef Expression
1 ssv 3762 . . . . . . . . 9 𝑋 ⊆ V
2 int0 4638 . . . . . . . . 9 ∅ = V
31, 2sseqtr4i 3775 . . . . . . . 8 𝑋
4 df-ss 3725 . . . . . . . 8 (𝑋 ∅ ↔ (𝑋 ∅) = 𝑋)
53, 4mpbi 220 . . . . . . 7 (𝑋 ∅) = 𝑋
65eqcomi 2765 . . . . . 6 𝑋 = (𝑋 ∅)
76eleq1i 2826 . . . . 5 (𝑋𝐵 ↔ (𝑋 ∅) ∈ 𝐵)
87a1i 11 . . . 4 (𝐴 ⊆ 𝒫 𝑋 → (𝑋𝐵 ↔ (𝑋 ∅) ∈ 𝐵))
9 eldifsn 4458 . . . . . . . 8 (𝑥 ∈ (𝒫 𝐴 ∖ {∅}) ↔ (𝑥 ∈ 𝒫 𝐴𝑥 ≠ ∅))
10 sstr2 3747 . . . . . . . . . . 11 (𝑥𝐴 → (𝐴 ⊆ 𝒫 𝑋𝑥 ⊆ 𝒫 𝑋))
11 bj-intss 33355 . . . . . . . . . . 11 (𝑥 ⊆ 𝒫 𝑋 → (𝑥 ≠ ∅ → 𝑥𝑋))
1210, 11syl6 35 . . . . . . . . . 10 (𝑥𝐴 → (𝐴 ⊆ 𝒫 𝑋 → (𝑥 ≠ ∅ → 𝑥𝑋)))
13 elpwi 4308 . . . . . . . . . 10 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
1412, 13syl11 33 . . . . . . . . 9 (𝐴 ⊆ 𝒫 𝑋 → (𝑥 ∈ 𝒫 𝐴 → (𝑥 ≠ ∅ → 𝑥𝑋)))
1514impd 446 . . . . . . . 8 (𝐴 ⊆ 𝒫 𝑋 → ((𝑥 ∈ 𝒫 𝐴𝑥 ≠ ∅) → 𝑥𝑋))
169, 15syl5bi 232 . . . . . . 7 (𝐴 ⊆ 𝒫 𝑋 → (𝑥 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑥𝑋))
17 df-ss 3725 . . . . . . . . 9 ( 𝑥𝑋 ↔ ( 𝑥𝑋) = 𝑥)
18 incom 3944 . . . . . . . . . . 11 ( 𝑥𝑋) = (𝑋 𝑥)
1918eqeq1i 2761 . . . . . . . . . 10 (( 𝑥𝑋) = 𝑥 ↔ (𝑋 𝑥) = 𝑥)
20 eqcom 2763 . . . . . . . . . 10 ((𝑋 𝑥) = 𝑥 𝑥 = (𝑋 𝑥))
2119, 20sylbb 209 . . . . . . . . 9 (( 𝑥𝑋) = 𝑥 𝑥 = (𝑋 𝑥))
2217, 21sylbi 207 . . . . . . . 8 ( 𝑥𝑋 𝑥 = (𝑋 𝑥))
23 eleq1 2823 . . . . . . . . 9 ( 𝑥 = (𝑋 𝑥) → ( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵))
2423a1i 11 . . . . . . . 8 (𝐴 ⊆ 𝒫 𝑋 → ( 𝑥 = (𝑋 𝑥) → ( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵)))
2522, 24syl5 34 . . . . . . 7 (𝐴 ⊆ 𝒫 𝑋 → ( 𝑥𝑋 → ( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵)))
2616, 25syld 47 . . . . . 6 (𝐴 ⊆ 𝒫 𝑋 → (𝑥 ∈ (𝒫 𝐴 ∖ {∅}) → ( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵)))
2726ralrimiv 3099 . . . . 5 (𝐴 ⊆ 𝒫 𝑋 → ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵))
28 ralbi 3202 . . . . 5 (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵) → (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵 ↔ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵))
2927, 28syl 17 . . . 4 (𝐴 ⊆ 𝒫 𝑋 → (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵 ↔ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵))
308, 29anbi12d 749 . . 3 (𝐴 ⊆ 𝒫 𝑋 → ((𝑋𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵) ↔ ((𝑋 ∅) ∈ 𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵)))
31 ancom 465 . . 3 (((𝑋 ∅) ∈ 𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵) ↔ (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵 ∧ (𝑋 ∅) ∈ 𝐵))
3230, 31syl6bb 276 . 2 (𝐴 ⊆ 𝒫 𝑋 → ((𝑋𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵) ↔ (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵 ∧ (𝑋 ∅) ∈ 𝐵)))
33 0elpw 4979 . . 3 ∅ ∈ 𝒫 𝐴
34 inteq 4626 . . . . 5 (𝑥 = ∅ → 𝑥 = ∅)
35 ineq2 3947 . . . . 5 ( 𝑥 = ∅ → (𝑋 𝑥) = (𝑋 ∅))
36 eleq1 2823 . . . . 5 ((𝑋 𝑥) = (𝑋 ∅) → ((𝑋 𝑥) ∈ 𝐵 ↔ (𝑋 ∅) ∈ 𝐵))
3734, 35, 363syl 18 . . . 4 (𝑥 = ∅ → ((𝑋 𝑥) ∈ 𝐵 ↔ (𝑋 ∅) ∈ 𝐵))
3837bj-raldifsn 33356 . . 3 (∅ ∈ 𝒫 𝐴 → (∀𝑥 ∈ 𝒫 𝐴(𝑋 𝑥) ∈ 𝐵 ↔ (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵 ∧ (𝑋 ∅) ∈ 𝐵)))
3933, 38ax-mp 5 . 2 (∀𝑥 ∈ 𝒫 𝐴(𝑋 𝑥) ∈ 𝐵 ↔ (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵 ∧ (𝑋 ∅) ∈ 𝐵))
4032, 39syl6bbr 278 1 (𝐴 ⊆ 𝒫 𝑋 → ((𝑋𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵) ↔ ∀𝑥 ∈ 𝒫 𝐴(𝑋 𝑥) ∈ 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1628   ∈ wcel 2135   ≠ wne 2928  ∀wral 3046  Vcvv 3336   ∖ cdif 3708   ∩ cin 3710   ⊆ wss 3711  ∅c0 4054  𝒫 cpw 4298  {csn 4317  ∩ cint 4623 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-nul 4937 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-rab 3055  df-v 3338  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-nul 4055  df-pw 4300  df-sn 4318  df-uni 4585  df-int 4624 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator