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

Theorem clsk1indlem1 41149
 Description: The ansatz closure function (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) does not have the K1 property of isotony. (Contributed by RP, 6-Jul-2021.)
Hypothesis
Ref Expression
clsk1indlem.k 𝐾 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))
Assertion
Ref Expression
clsk1indlem1 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑠𝑡 ∧ ¬ (𝐾𝑠) ⊆ (𝐾𝑡))
Distinct variable groups:   𝐾,𝑠,𝑡   𝑠,𝑟,𝑡
Allowed substitution hint:   𝐾(𝑟)

Proof of Theorem clsk1indlem1
StepHypRef Expression
1 tpex 7473 . . . 4 {∅, 1o, 2o} ∈ V
2 snsstp1 4709 . . . 4 {∅} ⊆ {∅, 1o, 2o}
31, 2elpwi2 5219 . . 3 {∅} ∈ 𝒫 {∅, 1o, 2o}
4 df3o2 41128 . . . 4 3o = {∅, 1o, 2o}
54pweqi 4515 . . 3 𝒫 3o = 𝒫 {∅, 1o, 2o}
63, 5eleqtrri 2851 . 2 {∅} ∈ 𝒫 3o
71a1i 11 . . . . 5 (⊤ → {∅, 1o, 2o} ∈ V)
82a1i 11 . . . . . . 7 (⊤ → {∅} ⊆ {∅, 1o, 2o})
9 0ex 5180 . . . . . . . 8 ∅ ∈ V
109snss 4679 . . . . . . 7 (∅ ∈ {∅, 1o, 2o} ↔ {∅} ⊆ {∅, 1o, 2o})
118, 10sylibr 237 . . . . . 6 (⊤ → ∅ ∈ {∅, 1o, 2o})
12 snsstp3 4711 . . . . . . . 8 {2o} ⊆ {∅, 1o, 2o}
1312a1i 11 . . . . . . 7 (⊤ → {2o} ⊆ {∅, 1o, 2o})
14 2oex 8127 . . . . . . . 8 2o ∈ V
1514snss 4679 . . . . . . 7 (2o ∈ {∅, 1o, 2o} ↔ {2o} ⊆ {∅, 1o, 2o})
1613, 15sylibr 237 . . . . . 6 (⊤ → 2o ∈ {∅, 1o, 2o})
1711, 16prssd 4715 . . . . 5 (⊤ → {∅, 2o} ⊆ {∅, 1o, 2o})
187, 17sselpwd 5199 . . . 4 (⊤ → {∅, 2o} ∈ 𝒫 {∅, 1o, 2o})
1918mptru 1545 . . 3 {∅, 2o} ∈ 𝒫 {∅, 1o, 2o}
2019, 5eleqtrri 2851 . 2 {∅, 2o} ∈ 𝒫 3o
21 simpl 486 . . 3 (({∅} ∈ 𝒫 3o ∧ {∅, 2o} ∈ 𝒫 3o) → {∅} ∈ 𝒫 3o)
22 sseq1 3919 . . . . . 6 (𝑠 = {∅} → (𝑠𝑡 ↔ {∅} ⊆ 𝑡))
23 fveq2 6662 . . . . . . . 8 (𝑠 = {∅} → (𝐾𝑠) = (𝐾‘{∅}))
2423sseq1d 3925 . . . . . . 7 (𝑠 = {∅} → ((𝐾𝑠) ⊆ (𝐾𝑡) ↔ (𝐾‘{∅}) ⊆ (𝐾𝑡)))
2524notbid 321 . . . . . 6 (𝑠 = {∅} → (¬ (𝐾𝑠) ⊆ (𝐾𝑡) ↔ ¬ (𝐾‘{∅}) ⊆ (𝐾𝑡)))
2622, 25anbi12d 633 . . . . 5 (𝑠 = {∅} → ((𝑠𝑡 ∧ ¬ (𝐾𝑠) ⊆ (𝐾𝑡)) ↔ ({∅} ⊆ 𝑡 ∧ ¬ (𝐾‘{∅}) ⊆ (𝐾𝑡))))
2726rexbidv 3221 . . . 4 (𝑠 = {∅} → (∃𝑡 ∈ 𝒫 3o(𝑠𝑡 ∧ ¬ (𝐾𝑠) ⊆ (𝐾𝑡)) ↔ ∃𝑡 ∈ 𝒫 3o({∅} ⊆ 𝑡 ∧ ¬ (𝐾‘{∅}) ⊆ (𝐾𝑡))))
2827adantl 485 . . 3 ((({∅} ∈ 𝒫 3o ∧ {∅, 2o} ∈ 𝒫 3o) ∧ 𝑠 = {∅}) → (∃𝑡 ∈ 𝒫 3o(𝑠𝑡 ∧ ¬ (𝐾𝑠) ⊆ (𝐾𝑡)) ↔ ∃𝑡 ∈ 𝒫 3o({∅} ⊆ 𝑡 ∧ ¬ (𝐾‘{∅}) ⊆ (𝐾𝑡))))
29 simpr 488 . . . 4 (({∅} ∈ 𝒫 3o ∧ {∅, 2o} ∈ 𝒫 3o) → {∅, 2o} ∈ 𝒫 3o)
30 fveq2 6662 . . . . . . . 8 (𝑡 = {∅, 2o} → (𝐾𝑡) = (𝐾‘{∅, 2o}))
3130sseq2d 3926 . . . . . . 7 (𝑡 = {∅, 2o} → ((𝐾‘{∅}) ⊆ (𝐾𝑡) ↔ (𝐾‘{∅}) ⊆ (𝐾‘{∅, 2o})))
3231notbid 321 . . . . . 6 (𝑡 = {∅, 2o} → (¬ (𝐾‘{∅}) ⊆ (𝐾𝑡) ↔ ¬ (𝐾‘{∅}) ⊆ (𝐾‘{∅, 2o})))
3332cleq2lem 40709 . . . . 5 (𝑡 = {∅, 2o} → (({∅} ⊆ 𝑡 ∧ ¬ (𝐾‘{∅}) ⊆ (𝐾𝑡)) ↔ ({∅} ⊆ {∅, 2o} ∧ ¬ (𝐾‘{∅}) ⊆ (𝐾‘{∅, 2o}))))
3433adantl 485 . . . 4 ((({∅} ∈ 𝒫 3o ∧ {∅, 2o} ∈ 𝒫 3o) ∧ 𝑡 = {∅, 2o}) → (({∅} ⊆ 𝑡 ∧ ¬ (𝐾‘{∅}) ⊆ (𝐾𝑡)) ↔ ({∅} ⊆ {∅, 2o} ∧ ¬ (𝐾‘{∅}) ⊆ (𝐾‘{∅, 2o}))))
35 1oex 8125 . . . . . . . 8 1o ∈ V
3635prid2 4659 . . . . . . 7 1o ∈ {∅, 1o}
37 iftrue 4429 . . . . . . . . 9 (𝑟 = {∅} → if(𝑟 = {∅}, {∅, 1o}, 𝑟) = {∅, 1o})
38 clsk1indlem.k . . . . . . . . 9 𝐾 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))
39 prex 5304 . . . . . . . . 9 {∅, 1o} ∈ V
4037, 38, 39fvmpt 6763 . . . . . . . 8 ({∅} ∈ 𝒫 3o → (𝐾‘{∅}) = {∅, 1o})
4140adantr 484 . . . . . . 7 (({∅} ∈ 𝒫 3o ∧ {∅, 2o} ∈ 𝒫 3o) → (𝐾‘{∅}) = {∅, 1o})
4236, 41eleqtrrid 2859 . . . . . 6 (({∅} ∈ 𝒫 3o ∧ {∅, 2o} ∈ 𝒫 3o) → 1o ∈ (𝐾‘{∅}))
43 1n0 8134 . . . . . . . . . . 11 1o ≠ ∅
4443neii 2953 . . . . . . . . . 10 ¬ 1o = ∅
45 eqcom 2765 . . . . . . . . . . . 12 (1o = 2o ↔ 2o = 1o)
46 df-2o 8118 . . . . . . . . . . . . 13 2o = suc 1o
47 df-1o 8117 . . . . . . . . . . . . 13 1o = suc ∅
4846, 47eqeq12i 2773 . . . . . . . . . . . 12 (2o = 1o ↔ suc 1o = suc ∅)
49 suc11reg 9120 . . . . . . . . . . . 12 (suc 1o = suc ∅ ↔ 1o = ∅)
5045, 48, 493bitri 300 . . . . . . . . . . 11 (1o = 2o ↔ 1o = ∅)
5143, 50nemtbir 3046 . . . . . . . . . 10 ¬ 1o = 2o
5244, 51pm3.2ni 878 . . . . . . . . 9 ¬ (1o = ∅ ∨ 1o = 2o)
53 elpri 4547 . . . . . . . . 9 (1o ∈ {∅, 2o} → (1o = ∅ ∨ 1o = 2o))
5452, 53mto 200 . . . . . . . 8 ¬ 1o ∈ {∅, 2o}
5554a1i 11 . . . . . . 7 (({∅} ∈ 𝒫 3o ∧ {∅, 2o} ∈ 𝒫 3o) → ¬ 1o ∈ {∅, 2o})
56 eqeq1 2762 . . . . . . . . . . 11 (𝑟 = {∅, 2o} → (𝑟 = {∅} ↔ {∅, 2o} = {∅}))
57 id 22 . . . . . . . . . . 11 (𝑟 = {∅, 2o} → 𝑟 = {∅, 2o})
5856, 57ifbieq2d 4449 . . . . . . . . . 10 (𝑟 = {∅, 2o} → if(𝑟 = {∅}, {∅, 1o}, 𝑟) = if({∅, 2o} = {∅}, {∅, 1o}, {∅, 2o}))
5914prid2 4659 . . . . . . . . . . . 12 2o ∈ {∅, 2o}
60 2on0 8128 . . . . . . . . . . . . 13 2o ≠ ∅
61 nelsn 4565 . . . . . . . . . . . . 13 (2o ≠ ∅ → ¬ 2o ∈ {∅})
6260, 61ax-mp 5 . . . . . . . . . . . 12 ¬ 2o ∈ {∅}
63 nelneq2 2877 . . . . . . . . . . . 12 ((2o ∈ {∅, 2o} ∧ ¬ 2o ∈ {∅}) → ¬ {∅, 2o} = {∅})
6459, 62, 63mp2an 691 . . . . . . . . . . 11 ¬ {∅, 2o} = {∅}
6564iffalsei 4433 . . . . . . . . . 10 if({∅, 2o} = {∅}, {∅, 1o}, {∅, 2o}) = {∅, 2o}
6658, 65eqtrdi 2809 . . . . . . . . 9 (𝑟 = {∅, 2o} → if(𝑟 = {∅}, {∅, 1o}, 𝑟) = {∅, 2o})
67 prex 5304 . . . . . . . . 9 {∅, 2o} ∈ V
6866, 38, 67fvmpt 6763 . . . . . . . 8 ({∅, 2o} ∈ 𝒫 3o → (𝐾‘{∅, 2o}) = {∅, 2o})
6968adantl 485 . . . . . . 7 (({∅} ∈ 𝒫 3o ∧ {∅, 2o} ∈ 𝒫 3o) → (𝐾‘{∅, 2o}) = {∅, 2o})
7055, 69neleqtrrd 2874 . . . . . 6 (({∅} ∈ 𝒫 3o ∧ {∅, 2o} ∈ 𝒫 3o) → ¬ 1o ∈ (𝐾‘{∅, 2o}))
71 nelss 3957 . . . . . 6 ((1o ∈ (𝐾‘{∅}) ∧ ¬ 1o ∈ (𝐾‘{∅, 2o})) → ¬ (𝐾‘{∅}) ⊆ (𝐾‘{∅, 2o}))
7242, 70, 71syl2anc 587 . . . . 5 (({∅} ∈ 𝒫 3o ∧ {∅, 2o} ∈ 𝒫 3o) → ¬ (𝐾‘{∅}) ⊆ (𝐾‘{∅, 2o}))
73 snsspr1 4707 . . . . 5 {∅} ⊆ {∅, 2o}
7472, 73jctil 523 . . . 4 (({∅} ∈ 𝒫 3o ∧ {∅, 2o} ∈ 𝒫 3o) → ({∅} ⊆ {∅, 2o} ∧ ¬ (𝐾‘{∅}) ⊆ (𝐾‘{∅, 2o})))
7529, 34, 74rspcedvd 3546 . . 3 (({∅} ∈ 𝒫 3o ∧ {∅, 2o} ∈ 𝒫 3o) → ∃𝑡 ∈ 𝒫 3o({∅} ⊆ 𝑡 ∧ ¬ (𝐾‘{∅}) ⊆ (𝐾𝑡)))
7621, 28, 75rspcedvd 3546 . 2 (({∅} ∈ 𝒫 3o ∧ {∅, 2o} ∈ 𝒫 3o) → ∃𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑠𝑡 ∧ ¬ (𝐾𝑠) ⊆ (𝐾𝑡)))
776, 20, 76mp2an 691 1 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑠𝑡 ∧ ¬ (𝐾𝑠) ⊆ (𝐾𝑡))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538  ⊤wtru 1539   ∈ wcel 2111   ≠ wne 2951  ∃wrex 3071  Vcvv 3409   ⊆ wss 3860  ∅c0 4227  ifcif 4423  𝒫 cpw 4497  {csn 4525  {cpr 4527  {ctp 4529   ↦ cmpt 5115  suc csuc 6175  ‘cfv 6339  1oc1o 8110  2oc2o 8111  3oc3o 8112 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 5172  ax-nul 5179  ax-pr 5301  ax-un 7464  ax-reg 9094 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  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 3699  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-br 5036  df-opab 5098  df-mpt 5116  df-tr 5142  df-id 5433  df-eprel 5438  df-po 5446  df-so 5447  df-fr 5486  df-we 5488  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-ord 6176  df-on 6177  df-suc 6179  df-iota 6298  df-fun 6341  df-fv 6347  df-1o 8117  df-2o 8118  df-3o 8119 This theorem is referenced by:  clsk1independent  41150
 Copyright terms: Public domain W3C validator