Mathbox for Richard Penner < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ntrk0kbimka Structured version   Visualization version   GIF version

Theorem ntrk0kbimka 41115
 Description: If the interiors of disjoint sets are disjoint and the interior of the base set is the base set, then the interior of the empty set is the empty set. Obsolete version of ntrkbimka 41114. (Contributed by RP, 12-Jun-2021.)
Assertion
Ref Expression
ntrk0kbimka ((𝐵𝑉𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵)) → (((𝐼𝐵) = 𝐵 ∧ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = ∅ → ((𝐼𝑠) ∩ (𝐼𝑡)) = ∅)) → (𝐼‘∅) = ∅))
Distinct variable groups:   𝐵,𝑠,𝑡   𝐼,𝑠,𝑡
Allowed substitution hints:   𝑉(𝑡,𝑠)

Proof of Theorem ntrk0kbimka
StepHypRef Expression
1 pwidg 4516 . . . . 5 (𝐵𝑉𝐵 ∈ 𝒫 𝐵)
21ad2antrr 725 . . . 4 (((𝐵𝑉𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵)) ∧ ((𝐼𝐵) = 𝐵 ∧ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = ∅ → ((𝐼𝑠) ∩ (𝐼𝑡)) = ∅))) → 𝐵 ∈ 𝒫 𝐵)
3 0elpw 5224 . . . . 5 ∅ ∈ 𝒫 𝐵
43a1i 11 . . . 4 (((𝐵𝑉𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵)) ∧ ((𝐼𝐵) = 𝐵 ∧ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = ∅ → ((𝐼𝑠) ∩ (𝐼𝑡)) = ∅))) → ∅ ∈ 𝒫 𝐵)
5 simprr 772 . . . 4 (((𝐵𝑉𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵)) ∧ ((𝐼𝐵) = 𝐵 ∧ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = ∅ → ((𝐼𝑠) ∩ (𝐼𝑡)) = ∅))) → ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = ∅ → ((𝐼𝑠) ∩ (𝐼𝑡)) = ∅))
6 ineq1 4109 . . . . . . 7 (𝑠 = 𝐵 → (𝑠𝑡) = (𝐵𝑡))
76eqeq1d 2760 . . . . . 6 (𝑠 = 𝐵 → ((𝑠𝑡) = ∅ ↔ (𝐵𝑡) = ∅))
8 fveq2 6658 . . . . . . . 8 (𝑠 = 𝐵 → (𝐼𝑠) = (𝐼𝐵))
98ineq1d 4116 . . . . . . 7 (𝑠 = 𝐵 → ((𝐼𝑠) ∩ (𝐼𝑡)) = ((𝐼𝐵) ∩ (𝐼𝑡)))
109eqeq1d 2760 . . . . . 6 (𝑠 = 𝐵 → (((𝐼𝑠) ∩ (𝐼𝑡)) = ∅ ↔ ((𝐼𝐵) ∩ (𝐼𝑡)) = ∅))
117, 10imbi12d 348 . . . . 5 (𝑠 = 𝐵 → (((𝑠𝑡) = ∅ → ((𝐼𝑠) ∩ (𝐼𝑡)) = ∅) ↔ ((𝐵𝑡) = ∅ → ((𝐼𝐵) ∩ (𝐼𝑡)) = ∅)))
12 ineq2 4111 . . . . . . . 8 (𝑡 = ∅ → (𝐵𝑡) = (𝐵 ∩ ∅))
1312eqeq1d 2760 . . . . . . 7 (𝑡 = ∅ → ((𝐵𝑡) = ∅ ↔ (𝐵 ∩ ∅) = ∅))
14 fveq2 6658 . . . . . . . . 9 (𝑡 = ∅ → (𝐼𝑡) = (𝐼‘∅))
1514ineq2d 4117 . . . . . . . 8 (𝑡 = ∅ → ((𝐼𝐵) ∩ (𝐼𝑡)) = ((𝐼𝐵) ∩ (𝐼‘∅)))
1615eqeq1d 2760 . . . . . . 7 (𝑡 = ∅ → (((𝐼𝐵) ∩ (𝐼𝑡)) = ∅ ↔ ((𝐼𝐵) ∩ (𝐼‘∅)) = ∅))
1713, 16imbi12d 348 . . . . . 6 (𝑡 = ∅ → (((𝐵𝑡) = ∅ → ((𝐼𝐵) ∩ (𝐼𝑡)) = ∅) ↔ ((𝐵 ∩ ∅) = ∅ → ((𝐼𝐵) ∩ (𝐼‘∅)) = ∅)))
18 in0 4287 . . . . . . 7 (𝐵 ∩ ∅) = ∅
19 pm5.5 365 . . . . . . 7 ((𝐵 ∩ ∅) = ∅ → (((𝐵 ∩ ∅) = ∅ → ((𝐼𝐵) ∩ (𝐼‘∅)) = ∅) ↔ ((𝐼𝐵) ∩ (𝐼‘∅)) = ∅))
2018, 19mp1i 13 . . . . . 6 (𝑡 = ∅ → (((𝐵 ∩ ∅) = ∅ → ((𝐼𝐵) ∩ (𝐼‘∅)) = ∅) ↔ ((𝐼𝐵) ∩ (𝐼‘∅)) = ∅))
2117, 20bitrd 282 . . . . 5 (𝑡 = ∅ → (((𝐵𝑡) = ∅ → ((𝐼𝐵) ∩ (𝐼𝑡)) = ∅) ↔ ((𝐼𝐵) ∩ (𝐼‘∅)) = ∅))
2211, 21rspc2va 3552 . . . 4 (((𝐵 ∈ 𝒫 𝐵 ∧ ∅ ∈ 𝒫 𝐵) ∧ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = ∅ → ((𝐼𝑠) ∩ (𝐼𝑡)) = ∅)) → ((𝐼𝐵) ∩ (𝐼‘∅)) = ∅)
232, 4, 5, 22syl21anc 836 . . 3 (((𝐵𝑉𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵)) ∧ ((𝐼𝐵) = 𝐵 ∧ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = ∅ → ((𝐼𝑠) ∩ (𝐼𝑡)) = ∅))) → ((𝐼𝐵) ∩ (𝐼‘∅)) = ∅)
2423ex 416 . 2 ((𝐵𝑉𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵)) → (((𝐼𝐵) = 𝐵 ∧ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = ∅ → ((𝐼𝑠) ∩ (𝐼𝑡)) = ∅)) → ((𝐼𝐵) ∩ (𝐼‘∅)) = ∅))
25 elmapi 8438 . . . . . 6 (𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
2625adantl 485 . . . . 5 ((𝐵𝑉𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵)) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
273a1i 11 . . . . 5 ((𝐵𝑉𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵)) → ∅ ∈ 𝒫 𝐵)
2826, 27ffvelrnd 6843 . . . 4 ((𝐵𝑉𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵)) → (𝐼‘∅) ∈ 𝒫 𝐵)
2928elpwid 4505 . . 3 ((𝐵𝑉𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵)) → (𝐼‘∅) ⊆ 𝐵)
30 simpl 486 . . 3 (((𝐼𝐵) = 𝐵 ∧ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = ∅ → ((𝐼𝑠) ∩ (𝐼𝑡)) = ∅)) → (𝐼𝐵) = 𝐵)
31 ineq1 4109 . . . . . . . 8 ((𝐼𝐵) = 𝐵 → ((𝐼𝐵) ∩ (𝐼‘∅)) = (𝐵 ∩ (𝐼‘∅)))
32 incom 4106 . . . . . . . 8 (𝐵 ∩ (𝐼‘∅)) = ((𝐼‘∅) ∩ 𝐵)
3331, 32eqtrdi 2809 . . . . . . 7 ((𝐼𝐵) = 𝐵 → ((𝐼𝐵) ∩ (𝐼‘∅)) = ((𝐼‘∅) ∩ 𝐵))
3433eqeq1d 2760 . . . . . 6 ((𝐼𝐵) = 𝐵 → (((𝐼𝐵) ∩ (𝐼‘∅)) = ∅ ↔ ((𝐼‘∅) ∩ 𝐵) = ∅))
3534biimpd 232 . . . . 5 ((𝐼𝐵) = 𝐵 → (((𝐼𝐵) ∩ (𝐼‘∅)) = ∅ → ((𝐼‘∅) ∩ 𝐵) = ∅))
36 reldisj 4348 . . . . . . 7 ((𝐼‘∅) ⊆ 𝐵 → (((𝐼‘∅) ∩ 𝐵) = ∅ ↔ (𝐼‘∅) ⊆ (𝐵𝐵)))
3736biimpd 232 . . . . . 6 ((𝐼‘∅) ⊆ 𝐵 → (((𝐼‘∅) ∩ 𝐵) = ∅ → (𝐼‘∅) ⊆ (𝐵𝐵)))
38 difid 4269 . . . . . . . 8 (𝐵𝐵) = ∅
3938sseq2i 3921 . . . . . . 7 ((𝐼‘∅) ⊆ (𝐵𝐵) ↔ (𝐼‘∅) ⊆ ∅)
40 ss0 4294 . . . . . . 7 ((𝐼‘∅) ⊆ ∅ → (𝐼‘∅) = ∅)
4139, 40sylbi 220 . . . . . 6 ((𝐼‘∅) ⊆ (𝐵𝐵) → (𝐼‘∅) = ∅)
4237, 41syl6com 37 . . . . 5 (((𝐼‘∅) ∩ 𝐵) = ∅ → ((𝐼‘∅) ⊆ 𝐵 → (𝐼‘∅) = ∅))
4335, 42syl6com 37 . . . 4 (((𝐼𝐵) ∩ (𝐼‘∅)) = ∅ → ((𝐼𝐵) = 𝐵 → ((𝐼‘∅) ⊆ 𝐵 → (𝐼‘∅) = ∅)))
4443com13 88 . . 3 ((𝐼‘∅) ⊆ 𝐵 → ((𝐼𝐵) = 𝐵 → (((𝐼𝐵) ∩ (𝐼‘∅)) = ∅ → (𝐼‘∅) = ∅)))
4529, 30, 44syl2im 40 . 2 ((𝐵𝑉𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵)) → (((𝐼𝐵) = 𝐵 ∧ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = ∅ → ((𝐼𝑠) ∩ (𝐼𝑡)) = ∅)) → (((𝐼𝐵) ∩ (𝐼‘∅)) = ∅ → (𝐼‘∅) = ∅)))
4624, 45mpdd 43 1 ((𝐵𝑉𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵)) → (((𝐼𝐵) = 𝐵 ∧ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = ∅ → ((𝐼𝑠) ∩ (𝐼𝑡)) = ∅)) → (𝐼‘∅) = ∅))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3070   ∖ cdif 3855   ∩ cin 3857   ⊆ wss 3858  ∅c0 4225  𝒫 cpw 4494  ⟶wf 6331  ‘cfv 6335  (class class class)co 7150   ↑m cmap 8416 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-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459 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-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-fv 6343  df-ov 7153  df-oprab 7154  df-mpo 7155  df-1st 7693  df-2nd 7694  df-map 8418 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator