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 34830
 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 3918 . . . . . . . . 9 𝑋 ⊆ V
2 int0 4855 . . . . . . . . 9 ∅ = V
31, 2sseqtrri 3931 . . . . . . . 8 𝑋
4 df-ss 3877 . . . . . . . 8 (𝑋 ∅ ↔ (𝑋 ∅) = 𝑋)
53, 4mpbi 233 . . . . . . 7 (𝑋 ∅) = 𝑋
65eqcomi 2767 . . . . . 6 𝑋 = (𝑋 ∅)
76eleq1i 2842 . . . . 5 (𝑋𝐵 ↔ (𝑋 ∅) ∈ 𝐵)
87a1i 11 . . . 4 (𝐴 ⊆ 𝒫 𝑋 → (𝑋𝐵 ↔ (𝑋 ∅) ∈ 𝐵))
9 eldifsn 4680 . . . . . . . 8 (𝑥 ∈ (𝒫 𝐴 ∖ {∅}) ↔ (𝑥 ∈ 𝒫 𝐴𝑥 ≠ ∅))
10 sstr2 3901 . . . . . . . . . . 11 (𝑥𝐴 → (𝐴 ⊆ 𝒫 𝑋𝑥 ⊆ 𝒫 𝑋))
11 intss2 4999 . . . . . . . . . . 11 (𝑥 ⊆ 𝒫 𝑋 → (𝑥 ≠ ∅ → 𝑥𝑋))
1210, 11syl6 35 . . . . . . . . . 10 (𝑥𝐴 → (𝐴 ⊆ 𝒫 𝑋 → (𝑥 ≠ ∅ → 𝑥𝑋)))
13 elpwi 4506 . . . . . . . . . 10 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
1412, 13syl11 33 . . . . . . . . 9 (𝐴 ⊆ 𝒫 𝑋 → (𝑥 ∈ 𝒫 𝐴 → (𝑥 ≠ ∅ → 𝑥𝑋)))
1514impd 414 . . . . . . . 8 (𝐴 ⊆ 𝒫 𝑋 → ((𝑥 ∈ 𝒫 𝐴𝑥 ≠ ∅) → 𝑥𝑋))
169, 15syl5bi 245 . . . . . . 7 (𝐴 ⊆ 𝒫 𝑋 → (𝑥 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑥𝑋))
17 df-ss 3877 . . . . . . . . 9 ( 𝑥𝑋 ↔ ( 𝑥𝑋) = 𝑥)
18 incom 4108 . . . . . . . . . . 11 ( 𝑥𝑋) = (𝑋 𝑥)
1918eqeq1i 2763 . . . . . . . . . 10 (( 𝑥𝑋) = 𝑥 ↔ (𝑋 𝑥) = 𝑥)
20 eqcom 2765 . . . . . . . . . 10 ((𝑋 𝑥) = 𝑥 𝑥 = (𝑋 𝑥))
2119, 20sylbb 222 . . . . . . . . 9 (( 𝑥𝑋) = 𝑥 𝑥 = (𝑋 𝑥))
2217, 21sylbi 220 . . . . . . . 8 ( 𝑥𝑋 𝑥 = (𝑋 𝑥))
23 eleq1 2839 . . . . . . . . 9 ( 𝑥 = (𝑋 𝑥) → ( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵))
2423a1i 11 . . . . . . . 8 (𝐴 ⊆ 𝒫 𝑋 → ( 𝑥 = (𝑋 𝑥) → ( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵)))
2522, 24syl5 34 . . . . . . 7 (𝐴 ⊆ 𝒫 𝑋 → ( 𝑥𝑋 → ( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵)))
2616, 25syld 47 . . . . . 6 (𝐴 ⊆ 𝒫 𝑋 → (𝑥 ∈ (𝒫 𝐴 ∖ {∅}) → ( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵)))
2726ralrimiv 3112 . . . . 5 (𝐴 ⊆ 𝒫 𝑋 → ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵))
28 ralbi 3099 . . . . 5 (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})( 𝑥𝐵 ↔ (𝑋 𝑥) ∈ 𝐵) → (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵 ↔ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵))
2927, 28syl 17 . . . 4 (𝐴 ⊆ 𝒫 𝑋 → (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵 ↔ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵))
308, 29anbi12d 633 . . 3 (𝐴 ⊆ 𝒫 𝑋 → ((𝑋𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵) ↔ ((𝑋 ∅) ∈ 𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵)))
3130biancomd 467 . 2 (𝐴 ⊆ 𝒫 𝑋 → ((𝑋𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵) ↔ (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵 ∧ (𝑋 ∅) ∈ 𝐵)))
32 0elpw 5228 . . 3 ∅ ∈ 𝒫 𝐴
33 inteq 4844 . . . . 5 (𝑥 = ∅ → 𝑥 = ∅)
34 ineq2 4113 . . . . 5 ( 𝑥 = ∅ → (𝑋 𝑥) = (𝑋 ∅))
35 eleq1 2839 . . . . 5 ((𝑋 𝑥) = (𝑋 ∅) → ((𝑋 𝑥) ∈ 𝐵 ↔ (𝑋 ∅) ∈ 𝐵))
3633, 34, 353syl 18 . . . 4 (𝑥 = ∅ → ((𝑋 𝑥) ∈ 𝐵 ↔ (𝑋 ∅) ∈ 𝐵))
3736bj-raldifsn 34829 . . 3 (∅ ∈ 𝒫 𝐴 → (∀𝑥 ∈ 𝒫 𝐴(𝑋 𝑥) ∈ 𝐵 ↔ (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵 ∧ (𝑋 ∅) ∈ 𝐵)))
3832, 37ax-mp 5 . 2 (∀𝑥 ∈ 𝒫 𝐴(𝑋 𝑥) ∈ 𝐵 ↔ (∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})(𝑋 𝑥) ∈ 𝐵 ∧ (𝑋 ∅) ∈ 𝐵))
3931, 38bitr4di 292 1 (𝐴 ⊆ 𝒫 𝑋 → ((𝑋𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅}) 𝑥𝐵) ↔ ∀𝑥 ∈ 𝒫 𝐴(𝑋 𝑥) ∈ 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  ∀wral 3070  Vcvv 3409   ∖ cdif 3857   ∩ cin 3859   ⊆ wss 3860  ∅c0 4227  𝒫 cpw 4497  {csn 4525  ∩ cint 4841 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-nul 5180 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3699  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-pw 4499  df-sn 4526  df-uni 4802  df-int 4842 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator