MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ustn0 Structured version   Visualization version   GIF version

Theorem ustn0 22500
Description: The empty set is not an uniform structure. (Contributed by Thierry Arnoux, 3-Dec-2017.)
Assertion
Ref Expression
ustn0 ¬ ∅ ∈ ran UnifOn

Proof of Theorem ustn0
Dummy variables 𝑣 𝑢 𝑤 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 noel 4211 . . . . 5 ¬ (𝑥 × 𝑥) ∈ ∅
2 0ex 5096 . . . . . 6 ∅ ∈ V
3 eleq2 2869 . . . . . 6 (𝑢 = ∅ → ((𝑥 × 𝑥) ∈ 𝑢 ↔ (𝑥 × 𝑥) ∈ ∅))
42, 3elab 3600 . . . . 5 (∅ ∈ {𝑢 ∣ (𝑥 × 𝑥) ∈ 𝑢} ↔ (𝑥 × 𝑥) ∈ ∅)
51, 4mtbir 324 . . . 4 ¬ ∅ ∈ {𝑢 ∣ (𝑥 × 𝑥) ∈ 𝑢}
6 vex 3435 . . . . . . 7 𝑥 ∈ V
7 selpw 4454 . . . . . . . . . 10 (𝑢 ∈ 𝒫 𝒫 (𝑥 × 𝑥) ↔ 𝑢 ⊆ 𝒫 (𝑥 × 𝑥))
87abbii 2859 . . . . . . . . 9 {𝑢𝑢 ∈ 𝒫 𝒫 (𝑥 × 𝑥)} = {𝑢𝑢 ⊆ 𝒫 (𝑥 × 𝑥)}
9 abid2 2924 . . . . . . . . . 10 {𝑢𝑢 ∈ 𝒫 𝒫 (𝑥 × 𝑥)} = 𝒫 𝒫 (𝑥 × 𝑥)
106, 6xpex 7324 . . . . . . . . . . . 12 (𝑥 × 𝑥) ∈ V
1110pwex 5165 . . . . . . . . . . 11 𝒫 (𝑥 × 𝑥) ∈ V
1211pwex 5165 . . . . . . . . . 10 𝒫 𝒫 (𝑥 × 𝑥) ∈ V
139, 12eqeltri 2877 . . . . . . . . 9 {𝑢𝑢 ∈ 𝒫 𝒫 (𝑥 × 𝑥)} ∈ V
148, 13eqeltrri 2878 . . . . . . . 8 {𝑢𝑢 ⊆ 𝒫 (𝑥 × 𝑥)} ∈ V
15 simp1 1127 . . . . . . . . 9 ((𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣𝑤𝑤𝑢) ∧ ∀𝑤𝑢 (𝑣𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣𝑣𝑢 ∧ ∃𝑤𝑢 (𝑤𝑤) ⊆ 𝑣))) → 𝑢 ⊆ 𝒫 (𝑥 × 𝑥))
1615ss2abi 3959 . . . . . . . 8 {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣𝑤𝑤𝑢) ∧ ∀𝑤𝑢 (𝑣𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣𝑣𝑢 ∧ ∃𝑤𝑢 (𝑤𝑤) ⊆ 𝑣)))} ⊆ {𝑢𝑢 ⊆ 𝒫 (𝑥 × 𝑥)}
1714, 16ssexi 5110 . . . . . . 7 {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣𝑤𝑤𝑢) ∧ ∀𝑤𝑢 (𝑣𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣𝑣𝑢 ∧ ∃𝑤𝑢 (𝑤𝑤) ⊆ 𝑣)))} ∈ V
18 df-ust 22480 . . . . . . . 8 UnifOn = (𝑥 ∈ V ↦ {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣𝑤𝑤𝑢) ∧ ∀𝑤𝑢 (𝑣𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣𝑣𝑢 ∧ ∃𝑤𝑢 (𝑤𝑤) ⊆ 𝑣)))})
1918fvmpt2 6636 . . . . . . 7 ((𝑥 ∈ V ∧ {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣𝑤𝑤𝑢) ∧ ∀𝑤𝑢 (𝑣𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣𝑣𝑢 ∧ ∃𝑤𝑢 (𝑤𝑤) ⊆ 𝑣)))} ∈ V) → (UnifOn‘𝑥) = {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣𝑤𝑤𝑢) ∧ ∀𝑤𝑢 (𝑣𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣𝑣𝑢 ∧ ∃𝑤𝑢 (𝑤𝑤) ⊆ 𝑣)))})
206, 17, 19mp2an 688 . . . . . 6 (UnifOn‘𝑥) = {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣𝑤𝑤𝑢) ∧ ∀𝑤𝑢 (𝑣𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣𝑣𝑢 ∧ ∃𝑤𝑢 (𝑤𝑤) ⊆ 𝑣)))}
21 simp2 1128 . . . . . . 7 ((𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣𝑤𝑤𝑢) ∧ ∀𝑤𝑢 (𝑣𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣𝑣𝑢 ∧ ∃𝑤𝑢 (𝑤𝑤) ⊆ 𝑣))) → (𝑥 × 𝑥) ∈ 𝑢)
2221ss2abi 3959 . . . . . 6 {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣𝑤𝑤𝑢) ∧ ∀𝑤𝑢 (𝑣𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣𝑣𝑢 ∧ ∃𝑤𝑢 (𝑤𝑤) ⊆ 𝑣)))} ⊆ {𝑢 ∣ (𝑥 × 𝑥) ∈ 𝑢}
2320, 22eqsstri 3917 . . . . 5 (UnifOn‘𝑥) ⊆ {𝑢 ∣ (𝑥 × 𝑥) ∈ 𝑢}
2423sseli 3880 . . . 4 (∅ ∈ (UnifOn‘𝑥) → ∅ ∈ {𝑢 ∣ (𝑥 × 𝑥) ∈ 𝑢})
255, 24mto 198 . . 3 ¬ ∅ ∈ (UnifOn‘𝑥)
2625nex 1780 . 2 ¬ ∃𝑥∅ ∈ (UnifOn‘𝑥)
2718funmpt2 6256 . . . 4 Fun UnifOn
28 elunirn 6866 . . . 4 (Fun UnifOn → (∅ ∈ ran UnifOn ↔ ∃𝑥 ∈ dom UnifOn∅ ∈ (UnifOn‘𝑥)))
2927, 28ax-mp 5 . . 3 (∅ ∈ ran UnifOn ↔ ∃𝑥 ∈ dom UnifOn∅ ∈ (UnifOn‘𝑥))
30 ustfn 22481 . . . . 5 UnifOn Fn V
31 fndm 6317 . . . . 5 (UnifOn Fn V → dom UnifOn = V)
3230, 31ax-mp 5 . . . 4 dom UnifOn = V
3332rexeqi 3371 . . 3 (∃𝑥 ∈ dom UnifOn∅ ∈ (UnifOn‘𝑥) ↔ ∃𝑥 ∈ V ∅ ∈ (UnifOn‘𝑥))
34 rexv 3458 . . 3 (∃𝑥 ∈ V ∅ ∈ (UnifOn‘𝑥) ↔ ∃𝑥∅ ∈ (UnifOn‘𝑥))
3529, 33, 343bitri 298 . 2 (∅ ∈ ran UnifOn ↔ ∃𝑥∅ ∈ (UnifOn‘𝑥))
3626, 35mtbir 324 1 ¬ ∅ ∈ ran UnifOn
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  w3a 1078   = wceq 1520  wex 1759  wcel 2079  {cab 2773  wral 3103  wrex 3104  Vcvv 3432  cin 3853  wss 3854  c0 4206  𝒫 cpw 4447   cuni 4739   I cid 5339   × cxp 5433  ccnv 5434  dom cdm 5435  ran crn 5436  cres 5437  ccom 5439  Fun wfun 6211   Fn wfn 6212  cfv 6217  UnifOncust 22479
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214  ax-un 7310
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3434  df-sbc 3702  df-csb 3807  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-pw 4449  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-br 4957  df-opab 5019  df-mpt 5036  df-id 5340  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-rn 5446  df-res 5447  df-ima 5448  df-iota 6181  df-fun 6219  df-fn 6220  df-fv 6225  df-ust 22480
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator