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 35970
Description: If 𝐴 is a collection of subsets of 𝑋, like a Moore collection or a topology, two equivalent ways to say that arbitrary intersections of elements of 𝐴 relative to 𝑋 belong to some class 𝐵: the LHS singles out the empty intersection (the empty intersection relative to 𝑋 is 𝑋 and the intersection of a nonempty family of subsets of 𝑋 is included in 𝑋, so there is no need to intersect it with 𝑋). In typical applications, 𝐵 is 𝐴 itself. (Contributed by BJ, 7-Dec-2021.)
Assertion
Ref Expression
bj-0int (𝐴 ⊆ 𝒫 𝑋 → ((𝑋𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵) ↔ ∀𝑥 ∈ 𝒫 𝐴(𝑋 𝑥) ∈ 𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝑋

Proof of Theorem bj-0int
StepHypRef Expression
1 ssv 4005 . . . . . . . . 9 𝑋 ⊆ V
2 int0 4965 . . . . . . . . 9 ∅ = V
31, 2sseqtrri 4018 . . . . . . . 8 𝑋
4 df-ss 3964 . . . . . . . 8 (𝑋 ∅ ↔ (𝑋 ∅) = 𝑋)
53, 4mpbi 229 . . . . . . 7 (𝑋 ∅) = 𝑋
65eqcomi 2741 . . . . . 6 𝑋 = (𝑋 ∅)
76eleq1i 2824 . . . . 5 (𝑋𝐵 ↔ (𝑋 ∅) ∈ 𝐵)
87a1i 11 . . . 4 (𝐴 ⊆ 𝒫 𝑋 → (𝑋𝐵 ↔ (𝑋 ∅) ∈ 𝐵))
9 eldifsn 4789 . . . . . . . 8 (𝑥 ∈ (𝒫 𝐴 ∖ {∅}) ↔ (𝑥 ∈ 𝒫 𝐴𝑥 ≠ ∅))
10 sstr2 3988 . . . . . . . . . . 11 (𝑥𝐴 → (𝐴 ⊆ 𝒫 𝑋𝑥 ⊆ 𝒫 𝑋))
11 intss2 5110 . . . . . . . . . . 11 (𝑥 ⊆ 𝒫 𝑋 → (𝑥 ≠ ∅ → 𝑥𝑋))
1210, 11syl6 35 . . . . . . . . . 10 (𝑥𝐴 → (𝐴 ⊆ 𝒫 𝑋 → (𝑥 ≠ ∅ → 𝑥𝑋)))
13 elpwi 4608 . . . . . . . . . 10 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
1412, 13syl11 33 . . . . . . . . 9 (𝐴 ⊆ 𝒫 𝑋 → (𝑥 ∈ 𝒫 𝐴 → (𝑥 ≠ ∅ → 𝑥𝑋)))
1514impd 411 . . . . . . . 8 (𝐴 ⊆ 𝒫 𝑋 → ((𝑥 ∈ 𝒫 𝐴𝑥 ≠ ∅) → 𝑥𝑋))
169, 15biimtrid 241 . . . . . . 7 (𝐴 ⊆ 𝒫 𝑋 → (𝑥 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑥𝑋))
17 df-ss 3964 . . . . . . . . 9 ( 𝑥𝑋 ↔ ( 𝑥𝑋) = 𝑥)
18 incom 4200 . . . . . . . . . . 11 ( 𝑥𝑋) = (𝑋 𝑥)
1918eqeq1i 2737 . . . . . . . . . 10 (( 𝑥𝑋) = 𝑥 ↔ (𝑋 𝑥) = 𝑥)
20 eqcom 2739 . . . . . . . . . 10 ((𝑋 𝑥) = 𝑥 𝑥 = (𝑋 𝑥))
2119, 20sylbb 218 . . . . . . . . 9 (( 𝑥𝑋) = 𝑥 𝑥 = (𝑋 𝑥))
2217, 21sylbi 216 . . . . . . . 8 ( 𝑥𝑋 𝑥 = (𝑋 𝑥))
23 eleq1 2821 . . . . . . . . 9 ( 𝑥 = (𝑋 𝑥) → ( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵))
2423a1i 11 . . . . . . . 8 (𝐴 ⊆ 𝒫 𝑋 → ( 𝑥 = (𝑋 𝑥) → ( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵)))
2522, 24syl5 34 . . . . . . 7 (𝐴 ⊆ 𝒫 𝑋 → ( 𝑥𝑋 → ( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵)))
2616, 25syld 47 . . . . . 6 (𝐴 ⊆ 𝒫 𝑋 → (𝑥 ∈ (𝒫 𝐴 ∖ {∅}) → ( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵)))
2726ralrimiv 3145 . . . . 5 (𝐴 ⊆ 𝒫 𝑋 → ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵))
28 ralbi 3103 . . . . 5 (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵) → (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵 ↔ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵))
2927, 28syl 17 . . . 4 (𝐴 ⊆ 𝒫 𝑋 → (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵 ↔ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵))
308, 29anbi12d 631 . . 3 (𝐴 ⊆ 𝒫 𝑋 → ((𝑋𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵) ↔ ((𝑋 ∅) ∈ 𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵)))
3130biancomd 464 . 2 (𝐴 ⊆ 𝒫 𝑋 → ((𝑋𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵) ↔ (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵 ∧ (𝑋 ∅) ∈ 𝐵)))
32 0elpw 5353 . . 3 ∅ ∈ 𝒫 𝐴
33 inteq 4952 . . . . 5 (𝑥 = ∅ → 𝑥 = ∅)
34 ineq2 4205 . . . . 5 ( 𝑥 = ∅ → (𝑋 𝑥) = (𝑋 ∅))
35 eleq1 2821 . . . . 5 ((𝑋 𝑥) = (𝑋 ∅) → ((𝑋 𝑥) ∈ 𝐵 ↔ (𝑋 ∅) ∈ 𝐵))
3633, 34, 353syl 18 . . . 4 (𝑥 = ∅ → ((𝑋 𝑥) ∈ 𝐵 ↔ (𝑋 ∅) ∈ 𝐵))
3736bj-raldifsn 35969 . . 3 (∅ ∈ 𝒫 𝐴 → (∀𝑥 ∈ 𝒫 𝐴(𝑋 𝑥) ∈ 𝐵 ↔ (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵 ∧ (𝑋 ∅) ∈ 𝐵)))
3832, 37ax-mp 5 . 2 (∀𝑥 ∈ 𝒫 𝐴(𝑋 𝑥) ∈ 𝐵 ↔ (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵 ∧ (𝑋 ∅) ∈ 𝐵))
3931, 38bitr4di 288 1 (𝐴 ⊆ 𝒫 𝑋 → ((𝑋𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵) ↔ ∀𝑥 ∈ 𝒫 𝐴(𝑋 𝑥) ∈ 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wne 2940  wral 3061  Vcvv 3474  cdif 3944  cin 3946  wss 3947  c0 4321  𝒫 cpw 4601  {csn 4627   cint 4949
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-ext 2703  ax-nul 5305
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-pw 4603  df-sn 4628  df-uni 4908  df-int 4950
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator