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

Theorem clsk1independent 43399
Description: For generalized closure functions, property K1 (isotony) is independent of the properties K0, K2, K3, K4. This contradicts a claim which appears in preprints of Table 2 in BΓ€rbel M. R. Stadler and Peter F. Stadler. "Generalized Topological Spaces in Evolutionary Theory and Combinatorial Chemistry." J. Chem. Inf. Comput. Sci., 42:577-585, 2002. Proceedings MCC 2001, Dubrovnik. The same table row implying K1 follows from the other four appears in the supplemental materials BΓ€rbel M. R. Stadler and Peter F. Stadler. "Basic Properties of Closure Spaces" 2001 on page 12. (Contributed by RP, 5-Jul-2021.)
Hypotheses
Ref Expression
clsnim.k0 (πœ‘ ↔ (π‘˜β€˜βˆ…) = βˆ…)
clsnim.k1 (πœ“ ↔ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘)))
clsnim.k2 (πœ’ ↔ βˆ€π‘  ∈ 𝒫 𝑏𝑠 βŠ† (π‘˜β€˜π‘ ))
clsnim.k3 (πœƒ ↔ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)))
clsnim.k4 (𝜏 ↔ βˆ€π‘  ∈ 𝒫 𝑏(π‘˜β€˜(π‘˜β€˜π‘ )) = (π‘˜β€˜π‘ ))
Assertion
Ref Expression
clsk1independent Β¬ βˆ€π‘βˆ€π‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(((πœ‘ ∧ πœ’) ∧ (πœƒ ∧ 𝜏)) β†’ πœ“)
Distinct variable group:   π‘˜,𝑏,𝑠,𝑑
Allowed substitution hints:   πœ‘(𝑑,π‘˜,𝑠,𝑏)   πœ“(𝑑,π‘˜,𝑠,𝑏)   πœ’(𝑑,π‘˜,𝑠,𝑏)   πœƒ(𝑑,π‘˜,𝑠,𝑏)   𝜏(𝑑,π‘˜,𝑠,𝑏)

Proof of Theorem clsk1independent
Dummy variable π‘Ÿ is distinct from all other variables.
StepHypRef Expression
1 3on 8498 . . 3 3o ∈ On
21elexi 3489 . 2 3o ∈ V
3 eqid 2727 . . . . 5 (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))
4 notnotr 130 . . . . . . . . . . 11 (Β¬ Β¬ π‘Ÿ = {βˆ…} β†’ π‘Ÿ = {βˆ…})
54a1i 11 . . . . . . . . . 10 (π‘Ÿ ∈ 𝒫 3o β†’ (Β¬ Β¬ π‘Ÿ = {βˆ…} β†’ π‘Ÿ = {βˆ…}))
6 sssucid 6443 . . . . . . . . . . . . 13 2o βŠ† suc 2o
7 2oex 8491 . . . . . . . . . . . . . 14 2o ∈ V
87elpw 4602 . . . . . . . . . . . . 13 (2o ∈ 𝒫 suc 2o ↔ 2o βŠ† suc 2o)
96, 8mpbir 230 . . . . . . . . . . . 12 2o ∈ 𝒫 suc 2o
10 df2o3 8488 . . . . . . . . . . . 12 2o = {βˆ…, 1o}
11 df-3o 8482 . . . . . . . . . . . . . 14 3o = suc 2o
1211eqcomi 2736 . . . . . . . . . . . . 13 suc 2o = 3o
1312pweqi 4614 . . . . . . . . . . . 12 𝒫 suc 2o = 𝒫 3o
149, 10, 133eltr3i 2840 . . . . . . . . . . 11 {βˆ…, 1o} ∈ 𝒫 3o
15142a1i 12 . . . . . . . . . 10 (π‘Ÿ ∈ 𝒫 3o β†’ (Β¬ Β¬ π‘Ÿ = {βˆ…} β†’ {βˆ…, 1o} ∈ 𝒫 3o))
165, 15jcad 512 . . . . . . . . 9 (π‘Ÿ ∈ 𝒫 3o β†’ (Β¬ Β¬ π‘Ÿ = {βˆ…} β†’ (π‘Ÿ = {βˆ…} ∧ {βˆ…, 1o} ∈ 𝒫 3o)))
1716con1d 145 . . . . . . . 8 (π‘Ÿ ∈ 𝒫 3o β†’ (Β¬ (π‘Ÿ = {βˆ…} ∧ {βˆ…, 1o} ∈ 𝒫 3o) β†’ Β¬ π‘Ÿ = {βˆ…}))
1817anc2ri 556 . . . . . . 7 (π‘Ÿ ∈ 𝒫 3o β†’ (Β¬ (π‘Ÿ = {βˆ…} ∧ {βˆ…, 1o} ∈ 𝒫 3o) β†’ (Β¬ π‘Ÿ = {βˆ…} ∧ π‘Ÿ ∈ 𝒫 3o)))
1918orrd 862 . . . . . 6 (π‘Ÿ ∈ 𝒫 3o β†’ ((π‘Ÿ = {βˆ…} ∧ {βˆ…, 1o} ∈ 𝒫 3o) ∨ (Β¬ π‘Ÿ = {βˆ…} ∧ π‘Ÿ ∈ 𝒫 3o)))
20 ifel 4568 . . . . . 6 (if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ) ∈ 𝒫 3o ↔ ((π‘Ÿ = {βˆ…} ∧ {βˆ…, 1o} ∈ 𝒫 3o) ∨ (Β¬ π‘Ÿ = {βˆ…} ∧ π‘Ÿ ∈ 𝒫 3o)))
2119, 20sylibr 233 . . . . 5 (π‘Ÿ ∈ 𝒫 3o β†’ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ) ∈ 𝒫 3o)
223, 21fmpti 7116 . . . 4 (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)):𝒫 3oβŸΆπ’« 3o
232pwex 5374 . . . . 5 𝒫 3o ∈ V
2423, 23elmap 8881 . . . 4 ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) ∈ (𝒫 3o ↑m 𝒫 3o) ↔ (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)):𝒫 3oβŸΆπ’« 3o)
2522, 24mpbir 230 . . 3 (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) ∈ (𝒫 3o ↑m 𝒫 3o)
263clsk1indlem0 43394 . . . . . 6 ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜βˆ…) = βˆ…
273clsk1indlem2 43395 . . . . . 6 βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )
2826, 27pm3.2i 470 . . . . 5 (((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜βˆ…) = βˆ… ∧ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ))
293clsk1indlem3 43396 . . . . . 6 βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜(𝑠 βˆͺ 𝑑)) βŠ† (((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βˆͺ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘))
303clsk1indlem4 43397 . . . . . 6 βˆ€π‘  ∈ 𝒫 3o((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )) = ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )
3129, 30pm3.2i 470 . . . . 5 (βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜(𝑠 βˆͺ 𝑑)) βŠ† (((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βˆͺ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘)) ∧ βˆ€π‘  ∈ 𝒫 3o((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )) = ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ))
3228, 31pm3.2i 470 . . . 4 ((((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜βˆ…) = βˆ… ∧ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )) ∧ (βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜(𝑠 βˆͺ 𝑑)) βŠ† (((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βˆͺ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘)) ∧ βˆ€π‘  ∈ 𝒫 3o((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )) = ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )))
333clsk1indlem1 43398 . . . 4 βˆƒπ‘  ∈ 𝒫 3oβˆƒπ‘‘ ∈ 𝒫 3o(𝑠 βŠ† 𝑑 ∧ Β¬ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βŠ† ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘))
3432, 33pm3.2i 470 . . 3 (((((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜βˆ…) = βˆ… ∧ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )) ∧ (βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜(𝑠 βˆͺ 𝑑)) βŠ† (((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βˆͺ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘)) ∧ βˆ€π‘  ∈ 𝒫 3o((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )) = ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ))) ∧ βˆƒπ‘  ∈ 𝒫 3oβˆƒπ‘‘ ∈ 𝒫 3o(𝑠 βŠ† 𝑑 ∧ Β¬ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βŠ† ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘)))
35 fveq1 6890 . . . . . . . 8 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ (π‘˜β€˜βˆ…) = ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜βˆ…))
3635eqeq1d 2729 . . . . . . 7 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ ((π‘˜β€˜βˆ…) = βˆ… ↔ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜βˆ…) = βˆ…))
37 fveq1 6890 . . . . . . . . 9 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ (π‘˜β€˜π‘ ) = ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ))
3837sseq2d 4010 . . . . . . . 8 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ (𝑠 βŠ† (π‘˜β€˜π‘ ) ↔ 𝑠 βŠ† ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )))
3938ralbidv 3172 . . . . . . 7 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ (βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† (π‘˜β€˜π‘ ) ↔ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )))
4036, 39anbi12d 630 . . . . . 6 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ (((π‘˜β€˜βˆ…) = βˆ… ∧ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† (π‘˜β€˜π‘ )) ↔ (((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜βˆ…) = βˆ… ∧ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ))))
41 fveq1 6890 . . . . . . . . 9 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ (π‘˜β€˜(𝑠 βˆͺ 𝑑)) = ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜(𝑠 βˆͺ 𝑑)))
42 fveq1 6890 . . . . . . . . . 10 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ (π‘˜β€˜π‘‘) = ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘))
4337, 42uneq12d 4160 . . . . . . . . 9 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = (((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βˆͺ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘)))
4441, 43sseq12d 4011 . . . . . . . 8 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ ((π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ↔ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜(𝑠 βˆͺ 𝑑)) βŠ† (((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βˆͺ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘))))
45442ralbidv 3213 . . . . . . 7 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ (βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ↔ βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜(𝑠 βˆͺ 𝑑)) βŠ† (((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βˆͺ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘))))
46 id 22 . . . . . . . . . 10 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)))
4746, 37fveq12d 6898 . . . . . . . . 9 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ (π‘˜β€˜(π‘˜β€˜π‘ )) = ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )))
4847, 37eqeq12d 2743 . . . . . . . 8 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ ((π‘˜β€˜(π‘˜β€˜π‘ )) = (π‘˜β€˜π‘ ) ↔ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )) = ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )))
4948ralbidv 3172 . . . . . . 7 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ (βˆ€π‘  ∈ 𝒫 3o(π‘˜β€˜(π‘˜β€˜π‘ )) = (π‘˜β€˜π‘ ) ↔ βˆ€π‘  ∈ 𝒫 3o((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )) = ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )))
5045, 49anbi12d 630 . . . . . 6 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ ((βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ βˆ€π‘  ∈ 𝒫 3o(π‘˜β€˜(π‘˜β€˜π‘ )) = (π‘˜β€˜π‘ )) ↔ (βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜(𝑠 βˆͺ 𝑑)) βŠ† (((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βˆͺ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘)) ∧ βˆ€π‘  ∈ 𝒫 3o((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )) = ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ))))
5140, 50anbi12d 630 . . . . 5 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ ((((π‘˜β€˜βˆ…) = βˆ… ∧ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† (π‘˜β€˜π‘ )) ∧ (βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ βˆ€π‘  ∈ 𝒫 3o(π‘˜β€˜(π‘˜β€˜π‘ )) = (π‘˜β€˜π‘ ))) ↔ ((((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜βˆ…) = βˆ… ∧ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )) ∧ (βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜(𝑠 βˆͺ 𝑑)) βŠ† (((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βˆͺ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘)) ∧ βˆ€π‘  ∈ 𝒫 3o((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )) = ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )))))
52 rexnal2 3130 . . . . . 6 (βˆƒπ‘  ∈ 𝒫 3oβˆƒπ‘‘ ∈ 𝒫 3o Β¬ (𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘)) ↔ Β¬ βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘)))
53 pm4.61 404 . . . . . . . 8 (Β¬ (𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘)) ↔ (𝑠 βŠ† 𝑑 ∧ Β¬ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘)))
5437, 42sseq12d 4011 . . . . . . . . . 10 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ ((π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘) ↔ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βŠ† ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘)))
5554notbid 318 . . . . . . . . 9 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ (Β¬ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘) ↔ Β¬ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βŠ† ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘)))
5655anbi2d 628 . . . . . . . 8 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ ((𝑠 βŠ† 𝑑 ∧ Β¬ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘)) ↔ (𝑠 βŠ† 𝑑 ∧ Β¬ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βŠ† ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘))))
5753, 56bitrid 283 . . . . . . 7 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ (Β¬ (𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘)) ↔ (𝑠 βŠ† 𝑑 ∧ Β¬ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βŠ† ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘))))
58572rexbidv 3214 . . . . . 6 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ (βˆƒπ‘  ∈ 𝒫 3oβˆƒπ‘‘ ∈ 𝒫 3o Β¬ (𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘)) ↔ βˆƒπ‘  ∈ 𝒫 3oβˆƒπ‘‘ ∈ 𝒫 3o(𝑠 βŠ† 𝑑 ∧ Β¬ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βŠ† ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘))))
5952, 58bitr3id 285 . . . . 5 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ (Β¬ βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘)) ↔ βˆƒπ‘  ∈ 𝒫 3oβˆƒπ‘‘ ∈ 𝒫 3o(𝑠 βŠ† 𝑑 ∧ Β¬ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βŠ† ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘))))
6051, 59anbi12d 630 . . . 4 (π‘˜ = (π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) β†’ (((((π‘˜β€˜βˆ…) = βˆ… ∧ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† (π‘˜β€˜π‘ )) ∧ (βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ βˆ€π‘  ∈ 𝒫 3o(π‘˜β€˜(π‘˜β€˜π‘ )) = (π‘˜β€˜π‘ ))) ∧ Β¬ βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘))) ↔ (((((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜βˆ…) = βˆ… ∧ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )) ∧ (βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜(𝑠 βˆͺ 𝑑)) βŠ† (((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βˆͺ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘)) ∧ βˆ€π‘  ∈ 𝒫 3o((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )) = ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ))) ∧ βˆƒπ‘  ∈ 𝒫 3oβˆƒπ‘‘ ∈ 𝒫 3o(𝑠 βŠ† 𝑑 ∧ Β¬ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βŠ† ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘)))))
6160rspcev 3607 . . 3 (((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ)) ∈ (𝒫 3o ↑m 𝒫 3o) ∧ (((((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜βˆ…) = βˆ… ∧ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )) ∧ (βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜(𝑠 βˆͺ 𝑑)) βŠ† (((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βˆͺ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘)) ∧ βˆ€π‘  ∈ 𝒫 3o((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ )) = ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ))) ∧ βˆƒπ‘  ∈ 𝒫 3oβˆƒπ‘‘ ∈ 𝒫 3o(𝑠 βŠ† 𝑑 ∧ Β¬ ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘ ) βŠ† ((π‘Ÿ ∈ 𝒫 3o ↦ if(π‘Ÿ = {βˆ…}, {βˆ…, 1o}, π‘Ÿ))β€˜π‘‘)))) β†’ βˆƒπ‘˜ ∈ (𝒫 3o ↑m 𝒫 3o)((((π‘˜β€˜βˆ…) = βˆ… ∧ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† (π‘˜β€˜π‘ )) ∧ (βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ βˆ€π‘  ∈ 𝒫 3o(π‘˜β€˜(π‘˜β€˜π‘ )) = (π‘˜β€˜π‘ ))) ∧ Β¬ βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘))))
6225, 34, 61mp2an 691 . 2 βˆƒπ‘˜ ∈ (𝒫 3o ↑m 𝒫 3o)((((π‘˜β€˜βˆ…) = βˆ… ∧ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† (π‘˜β€˜π‘ )) ∧ (βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ βˆ€π‘  ∈ 𝒫 3o(π‘˜β€˜(π‘˜β€˜π‘ )) = (π‘˜β€˜π‘ ))) ∧ Β¬ βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘)))
63 pweq 4612 . . . . . 6 (𝑏 = 3o β†’ 𝒫 𝑏 = 𝒫 3o)
6463, 63oveq12d 7432 . . . . 5 (𝑏 = 3o β†’ (𝒫 𝑏 ↑m 𝒫 𝑏) = (𝒫 3o ↑m 𝒫 3o))
65 pm4.61 404 . . . . . 6 (Β¬ (((πœ‘ ∧ πœ’) ∧ (πœƒ ∧ 𝜏)) β†’ πœ“) ↔ (((πœ‘ ∧ πœ’) ∧ (πœƒ ∧ 𝜏)) ∧ Β¬ πœ“))
66 clsnim.k0 . . . . . . . . . 10 (πœ‘ ↔ (π‘˜β€˜βˆ…) = βˆ…)
6766a1i 11 . . . . . . . . 9 (𝑏 = 3o β†’ (πœ‘ ↔ (π‘˜β€˜βˆ…) = βˆ…))
68 clsnim.k2 . . . . . . . . . 10 (πœ’ ↔ βˆ€π‘  ∈ 𝒫 𝑏𝑠 βŠ† (π‘˜β€˜π‘ ))
6963raleqdv 3320 . . . . . . . . . 10 (𝑏 = 3o β†’ (βˆ€π‘  ∈ 𝒫 𝑏𝑠 βŠ† (π‘˜β€˜π‘ ) ↔ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† (π‘˜β€˜π‘ )))
7068, 69bitrid 283 . . . . . . . . 9 (𝑏 = 3o β†’ (πœ’ ↔ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† (π‘˜β€˜π‘ )))
7167, 70anbi12d 630 . . . . . . . 8 (𝑏 = 3o β†’ ((πœ‘ ∧ πœ’) ↔ ((π‘˜β€˜βˆ…) = βˆ… ∧ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† (π‘˜β€˜π‘ ))))
72 clsnim.k3 . . . . . . . . . 10 (πœƒ ↔ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)))
7363raleqdv 3320 . . . . . . . . . . 11 (𝑏 = 3o β†’ (βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ↔ βˆ€π‘‘ ∈ 𝒫 3o(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘))))
7463, 73raleqbidv 3337 . . . . . . . . . 10 (𝑏 = 3o β†’ (βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ↔ βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘))))
7572, 74bitrid 283 . . . . . . . . 9 (𝑏 = 3o β†’ (πœƒ ↔ βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘))))
76 clsnim.k4 . . . . . . . . . 10 (𝜏 ↔ βˆ€π‘  ∈ 𝒫 𝑏(π‘˜β€˜(π‘˜β€˜π‘ )) = (π‘˜β€˜π‘ ))
7763raleqdv 3320 . . . . . . . . . 10 (𝑏 = 3o β†’ (βˆ€π‘  ∈ 𝒫 𝑏(π‘˜β€˜(π‘˜β€˜π‘ )) = (π‘˜β€˜π‘ ) ↔ βˆ€π‘  ∈ 𝒫 3o(π‘˜β€˜(π‘˜β€˜π‘ )) = (π‘˜β€˜π‘ )))
7876, 77bitrid 283 . . . . . . . . 9 (𝑏 = 3o β†’ (𝜏 ↔ βˆ€π‘  ∈ 𝒫 3o(π‘˜β€˜(π‘˜β€˜π‘ )) = (π‘˜β€˜π‘ )))
7975, 78anbi12d 630 . . . . . . . 8 (𝑏 = 3o β†’ ((πœƒ ∧ 𝜏) ↔ (βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ βˆ€π‘  ∈ 𝒫 3o(π‘˜β€˜(π‘˜β€˜π‘ )) = (π‘˜β€˜π‘ ))))
8071, 79anbi12d 630 . . . . . . 7 (𝑏 = 3o β†’ (((πœ‘ ∧ πœ’) ∧ (πœƒ ∧ 𝜏)) ↔ (((π‘˜β€˜βˆ…) = βˆ… ∧ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† (π‘˜β€˜π‘ )) ∧ (βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ βˆ€π‘  ∈ 𝒫 3o(π‘˜β€˜(π‘˜β€˜π‘ )) = (π‘˜β€˜π‘ )))))
81 clsnim.k1 . . . . . . . . 9 (πœ“ ↔ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘)))
8263raleqdv 3320 . . . . . . . . . 10 (𝑏 = 3o β†’ (βˆ€π‘‘ ∈ 𝒫 𝑏(𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘)) ↔ βˆ€π‘‘ ∈ 𝒫 3o(𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘))))
8363, 82raleqbidv 3337 . . . . . . . . 9 (𝑏 = 3o β†’ (βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘)) ↔ βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘))))
8481, 83bitrid 283 . . . . . . . 8 (𝑏 = 3o β†’ (πœ“ ↔ βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘))))
8584notbid 318 . . . . . . 7 (𝑏 = 3o β†’ (Β¬ πœ“ ↔ Β¬ βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘))))
8680, 85anbi12d 630 . . . . . 6 (𝑏 = 3o β†’ ((((πœ‘ ∧ πœ’) ∧ (πœƒ ∧ 𝜏)) ∧ Β¬ πœ“) ↔ ((((π‘˜β€˜βˆ…) = βˆ… ∧ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† (π‘˜β€˜π‘ )) ∧ (βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ βˆ€π‘  ∈ 𝒫 3o(π‘˜β€˜(π‘˜β€˜π‘ )) = (π‘˜β€˜π‘ ))) ∧ Β¬ βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘)))))
8765, 86bitrid 283 . . . . 5 (𝑏 = 3o β†’ (Β¬ (((πœ‘ ∧ πœ’) ∧ (πœƒ ∧ 𝜏)) β†’ πœ“) ↔ ((((π‘˜β€˜βˆ…) = βˆ… ∧ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† (π‘˜β€˜π‘ )) ∧ (βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ βˆ€π‘  ∈ 𝒫 3o(π‘˜β€˜(π‘˜β€˜π‘ )) = (π‘˜β€˜π‘ ))) ∧ Β¬ βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘)))))
8864, 87rexeqbidv 3338 . . . 4 (𝑏 = 3o β†’ (βˆƒπ‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) Β¬ (((πœ‘ ∧ πœ’) ∧ (πœƒ ∧ 𝜏)) β†’ πœ“) ↔ βˆƒπ‘˜ ∈ (𝒫 3o ↑m 𝒫 3o)((((π‘˜β€˜βˆ…) = βˆ… ∧ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† (π‘˜β€˜π‘ )) ∧ (βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ βˆ€π‘  ∈ 𝒫 3o(π‘˜β€˜(π‘˜β€˜π‘ )) = (π‘˜β€˜π‘ ))) ∧ Β¬ βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘)))))
8988rspcev 3607 . . 3 ((3o ∈ V ∧ βˆƒπ‘˜ ∈ (𝒫 3o ↑m 𝒫 3o)((((π‘˜β€˜βˆ…) = βˆ… ∧ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† (π‘˜β€˜π‘ )) ∧ (βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ βˆ€π‘  ∈ 𝒫 3o(π‘˜β€˜(π‘˜β€˜π‘ )) = (π‘˜β€˜π‘ ))) ∧ Β¬ βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘)))) β†’ βˆƒπ‘ ∈ V βˆƒπ‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) Β¬ (((πœ‘ ∧ πœ’) ∧ (πœƒ ∧ 𝜏)) β†’ πœ“))
90 rexnal2 3130 . . . 4 (βˆƒπ‘ ∈ V βˆƒπ‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) Β¬ (((πœ‘ ∧ πœ’) ∧ (πœƒ ∧ 𝜏)) β†’ πœ“) ↔ Β¬ βˆ€π‘ ∈ V βˆ€π‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(((πœ‘ ∧ πœ’) ∧ (πœƒ ∧ 𝜏)) β†’ πœ“))
91 ralv 3494 . . . 4 (βˆ€π‘ ∈ V βˆ€π‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(((πœ‘ ∧ πœ’) ∧ (πœƒ ∧ 𝜏)) β†’ πœ“) ↔ βˆ€π‘βˆ€π‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(((πœ‘ ∧ πœ’) ∧ (πœƒ ∧ 𝜏)) β†’ πœ“))
9290, 91xchbinx 334 . . 3 (βˆƒπ‘ ∈ V βˆƒπ‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) Β¬ (((πœ‘ ∧ πœ’) ∧ (πœƒ ∧ 𝜏)) β†’ πœ“) ↔ Β¬ βˆ€π‘βˆ€π‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(((πœ‘ ∧ πœ’) ∧ (πœƒ ∧ 𝜏)) β†’ πœ“))
9389, 92sylib 217 . 2 ((3o ∈ V ∧ βˆƒπ‘˜ ∈ (𝒫 3o ↑m 𝒫 3o)((((π‘˜β€˜βˆ…) = βˆ… ∧ βˆ€π‘  ∈ 𝒫 3o𝑠 βŠ† (π‘˜β€˜π‘ )) ∧ (βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ βˆ€π‘  ∈ 𝒫 3o(π‘˜β€˜(π‘˜β€˜π‘ )) = (π‘˜β€˜π‘ ))) ∧ Β¬ βˆ€π‘  ∈ 𝒫 3oβˆ€π‘‘ ∈ 𝒫 3o(𝑠 βŠ† 𝑑 β†’ (π‘˜β€˜π‘ ) βŠ† (π‘˜β€˜π‘‘)))) β†’ Β¬ βˆ€π‘βˆ€π‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(((πœ‘ ∧ πœ’) ∧ (πœƒ ∧ 𝜏)) β†’ πœ“))
942, 62, 93mp2an 691 1 Β¬ βˆ€π‘βˆ€π‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(((πœ‘ ∧ πœ’) ∧ (πœƒ ∧ 𝜏)) β†’ πœ“)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 846  βˆ€wal 1532   = wceq 1534   ∈ wcel 2099  βˆ€wral 3056  βˆƒwrex 3065  Vcvv 3469   βˆͺ cun 3942   βŠ† wss 3944  βˆ…c0 4318  ifcif 4524  π’« cpw 4598  {csn 4624  {cpr 4626   ↦ cmpt 5225  Oncon0 6363  suc csuc 6365  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7414  1oc1o 8473  2oc2o 8474  3oc3o 8475   ↑m cmap 8836
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-reg 9607
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-xor 1506  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-sbc 3775  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-ord 6366  df-on 6367  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550  df-ov 7417  df-oprab 7418  df-mpo 7419  df-1o 8480  df-2o 8481  df-3o 8482  df-map 8838
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator