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 36285
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 2739 . . . . . 6 𝑋 = (𝑋 ∅)
76eleq1i 2822 . . . . 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 409 . . . . . . . 8 (𝐴 ⊆ 𝒫 𝑋 → ((𝑥 ∈ 𝒫 𝐴𝑥 ≠ ∅) → 𝑥𝑋))
169, 15biimtrid 241 . . . . . . 7 (𝐴 ⊆ 𝒫 𝑋 → (𝑥 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑥𝑋))
17 df-ss 3964 . . . . . . . . 9 ( 𝑥𝑋 ↔ ( 𝑥𝑋) = 𝑥)
18 incom 4200 . . . . . . . . . . 11 ( 𝑥𝑋) = (𝑋 𝑥)
1918eqeq1i 2735 . . . . . . . . . 10 (( 𝑥𝑋) = 𝑥 ↔ (𝑋 𝑥) = 𝑥)
20 eqcom 2737 . . . . . . . . . 10 ((𝑋 𝑥) = 𝑥 𝑥 = (𝑋 𝑥))
2119, 20sylbb 218 . . . . . . . . 9 (( 𝑥𝑋) = 𝑥 𝑥 = (𝑋 𝑥))
2217, 21sylbi 216 . . . . . . . 8 ( 𝑥𝑋 𝑥 = (𝑋 𝑥))
23 eleq1 2819 . . . . . . . . 9 ( 𝑥 = (𝑋 𝑥) → ( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵))
2423a1i 11 . . . . . . . 8 (𝐴 ⊆ 𝒫 𝑋 → ( 𝑥 = (𝑋 𝑥) → ( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵)))
2522, 24syl5 34 . . . . . . 7 (𝐴 ⊆ 𝒫 𝑋 → ( 𝑥𝑋 → ( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵)))
2616, 25syld 47 . . . . . 6 (𝐴 ⊆ 𝒫 𝑋 → (𝑥 ∈ (𝒫 𝐴 ∖ {∅}) → ( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵)))
2726ralrimiv 3143 . . . . 5 (𝐴 ⊆ 𝒫 𝑋 → ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵))
28 ralbi 3101 . . . . 5 (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵) → (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵 ↔ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵))
2927, 28syl 17 . . . 4 (𝐴 ⊆ 𝒫 𝑋 → (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵 ↔ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵))
308, 29anbi12d 629 . . 3 (𝐴 ⊆ 𝒫 𝑋 → ((𝑋𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵) ↔ ((𝑋 ∅) ∈ 𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵)))
3130biancomd 462 . 2 (𝐴 ⊆ 𝒫 𝑋 → ((𝑋𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵) ↔ (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵 ∧ (𝑋 ∅) ∈ 𝐵)))
32 0elpw 5353 . . 3 ∅ ∈ 𝒫 𝐴
33 inteq 4952 . . . . 5 (𝑥 = ∅ → 𝑥 = ∅)
34 ineq2 4205 . . . . 5 ( 𝑥 = ∅ → (𝑋 𝑥) = (𝑋 ∅))
35 eleq1 2819 . . . . 5 ((𝑋 𝑥) = (𝑋 ∅) → ((𝑋 𝑥) ∈ 𝐵 ↔ (𝑋 ∅) ∈ 𝐵))
3633, 34, 353syl 18 . . . 4 (𝑥 = ∅ → ((𝑋 𝑥) ∈ 𝐵 ↔ (𝑋 ∅) ∈ 𝐵))
3736bj-raldifsn 36284 . . 3 (∅ ∈ 𝒫 𝐴 → (∀𝑥 ∈ 𝒫 𝐴(𝑋 𝑥) ∈ 𝐵 ↔ (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵 ∧ (𝑋 ∅) ∈ 𝐵)))
3832, 37ax-mp 5 . 2 (∀𝑥 ∈ 𝒫 𝐴(𝑋 𝑥) ∈ 𝐵 ↔ (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵 ∧ (𝑋 ∅) ∈ 𝐵))
3931, 38bitr4di 288 1 (𝐴 ⊆ 𝒫 𝑋 → ((𝑋𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵) ↔ ∀𝑥 ∈ 𝒫 𝐴(𝑋 𝑥) ∈ 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1539  wcel 2104  wne 2938  wral 3059  Vcvv 3472  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 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-nul 5305
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  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