Users' Mathboxes 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 33483
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 3785 . . . . . . . . 9 𝑋 ⊆ V
2 int0 4647 . . . . . . . . 9 ∅ = V
31, 2sseqtr4i 3798 . . . . . . . 8 𝑋
4 df-ss 3746 . . . . . . . 8 (𝑋 ∅ ↔ (𝑋 ∅) = 𝑋)
53, 4mpbi 221 . . . . . . 7 (𝑋 ∅) = 𝑋
65eqcomi 2774 . . . . . 6 𝑋 = (𝑋 ∅)
76eleq1i 2835 . . . . 5 (𝑋𝐵 ↔ (𝑋 ∅) ∈ 𝐵)
87a1i 11 . . . 4 (𝐴 ⊆ 𝒫 𝑋 → (𝑋𝐵 ↔ (𝑋 ∅) ∈ 𝐵))
9 eldifsn 4472 . . . . . . . 8 (𝑥 ∈ (𝒫 𝐴 ∖ {∅}) ↔ (𝑥 ∈ 𝒫 𝐴𝑥 ≠ ∅))
10 sstr2 3768 . . . . . . . . . . 11 (𝑥𝐴 → (𝐴 ⊆ 𝒫 𝑋𝑥 ⊆ 𝒫 𝑋))
11 bj-intss 33481 . . . . . . . . . . 11 (𝑥 ⊆ 𝒫 𝑋 → (𝑥 ≠ ∅ → 𝑥𝑋))
1210, 11syl6 35 . . . . . . . . . 10 (𝑥𝐴 → (𝐴 ⊆ 𝒫 𝑋 → (𝑥 ≠ ∅ → 𝑥𝑋)))
13 elpwi 4325 . . . . . . . . . 10 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
1412, 13syl11 33 . . . . . . . . 9 (𝐴 ⊆ 𝒫 𝑋 → (𝑥 ∈ 𝒫 𝐴 → (𝑥 ≠ ∅ → 𝑥𝑋)))
1514impd 398 . . . . . . . 8 (𝐴 ⊆ 𝒫 𝑋 → ((𝑥 ∈ 𝒫 𝐴𝑥 ≠ ∅) → 𝑥𝑋))
169, 15syl5bi 233 . . . . . . 7 (𝐴 ⊆ 𝒫 𝑋 → (𝑥 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑥𝑋))
17 df-ss 3746 . . . . . . . . 9 ( 𝑥𝑋 ↔ ( 𝑥𝑋) = 𝑥)
18 incom 3967 . . . . . . . . . . 11 ( 𝑥𝑋) = (𝑋 𝑥)
1918eqeq1i 2770 . . . . . . . . . 10 (( 𝑥𝑋) = 𝑥 ↔ (𝑋 𝑥) = 𝑥)
20 eqcom 2772 . . . . . . . . . 10 ((𝑋 𝑥) = 𝑥 𝑥 = (𝑋 𝑥))
2119, 20sylbb 210 . . . . . . . . 9 (( 𝑥𝑋) = 𝑥 𝑥 = (𝑋 𝑥))
2217, 21sylbi 208 . . . . . . . 8 ( 𝑥𝑋 𝑥 = (𝑋 𝑥))
23 eleq1 2832 . . . . . . . . 9 ( 𝑥 = (𝑋 𝑥) → ( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵))
2423a1i 11 . . . . . . . 8 (𝐴 ⊆ 𝒫 𝑋 → ( 𝑥 = (𝑋 𝑥) → ( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵)))
2522, 24syl5 34 . . . . . . 7 (𝐴 ⊆ 𝒫 𝑋 → ( 𝑥𝑋 → ( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵)))
2616, 25syld 47 . . . . . 6 (𝐴 ⊆ 𝒫 𝑋 → (𝑥 ∈ (𝒫 𝐴 ∖ {∅}) → ( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵)))
2726ralrimiv 3112 . . . . 5 (𝐴 ⊆ 𝒫 𝑋 → ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵))
28 ralbi 3215 . . . . 5 (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵) → (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵 ↔ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵))
2927, 28syl 17 . . . 4 (𝐴 ⊆ 𝒫 𝑋 → (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵 ↔ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵))
308, 29anbi12d 624 . . 3 (𝐴 ⊆ 𝒫 𝑋 → ((𝑋𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵) ↔ ((𝑋 ∅) ∈ 𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵)))
31 ancom 452 . . 3 (((𝑋 ∅) ∈ 𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵) ↔ (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵 ∧ (𝑋 ∅) ∈ 𝐵))
3230, 31syl6bb 278 . 2 (𝐴 ⊆ 𝒫 𝑋 → ((𝑋𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵) ↔ (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵 ∧ (𝑋 ∅) ∈ 𝐵)))
33 0elpw 4992 . . 3 ∅ ∈ 𝒫 𝐴
34 inteq 4636 . . . . 5 (𝑥 = ∅ → 𝑥 = ∅)
35 ineq2 3970 . . . . 5 ( 𝑥 = ∅ → (𝑋 𝑥) = (𝑋 ∅))
36 eleq1 2832 . . . . 5 ((𝑋 𝑥) = (𝑋 ∅) → ((𝑋 𝑥) ∈ 𝐵 ↔ (𝑋 ∅) ∈ 𝐵))
3734, 35, 363syl 18 . . . 4 (𝑥 = ∅ → ((𝑋 𝑥) ∈ 𝐵 ↔ (𝑋 ∅) ∈ 𝐵))
3837bj-raldifsn 33482 . . 3 (∅ ∈ 𝒫 𝐴 → (∀𝑥 ∈ 𝒫 𝐴(𝑋 𝑥) ∈ 𝐵 ↔ (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵 ∧ (𝑋 ∅) ∈ 𝐵)))
3933, 38ax-mp 5 . 2 (∀𝑥 ∈ 𝒫 𝐴(𝑋 𝑥) ∈ 𝐵 ↔ (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵 ∧ (𝑋 ∅) ∈ 𝐵))
4032, 39syl6bbr 280 1 (𝐴 ⊆ 𝒫 𝑋 → ((𝑋𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵) ↔ ∀𝑥 ∈ 𝒫 𝐴(𝑋 𝑥) ∈ 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wne 2937  wral 3055  Vcvv 3350  cdif 3729  cin 3731  wss 3732  c0 4079  𝒫 cpw 4315  {csn 4334   cint 4633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-nul 4949
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-pw 4317  df-sn 4335  df-uni 4595  df-int 4634
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator