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 38845
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 ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓)
Distinct variable group:   𝑘,𝑏,𝑠,𝑡
Allowed substitution hints:   𝜑(𝑡,𝑘,𝑠,𝑏)   𝜓(𝑡,𝑘,𝑠,𝑏)   𝜒(𝑡,𝑘,𝑠,𝑏)   𝜃(𝑡,𝑘,𝑠,𝑏)   𝜏(𝑡,𝑘,𝑠,𝑏)

Proof of Theorem clsk1independent
Dummy variable 𝑟 is distinct from all other variables.
StepHypRef Expression
1 3on 7810 . . 3 3𝑜 ∈ On
21elexi 3414 . 2 3𝑜 ∈ V
3 eqid 2813 . . . . 5 (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))
4 notnotr 128 . . . . . . . . . . 11 (¬ ¬ 𝑟 = {∅} → 𝑟 = {∅})
54a1i 11 . . . . . . . . . 10 (𝑟 ∈ 𝒫 3𝑜 → (¬ ¬ 𝑟 = {∅} → 𝑟 = {∅}))
6 sssucid 6021 . . . . . . . . . . . . 13 2𝑜 ⊆ suc 2𝑜
7 2on 7808 . . . . . . . . . . . . . . 15 2𝑜 ∈ On
87elexi 3414 . . . . . . . . . . . . . 14 2𝑜 ∈ V
98elpw 4364 . . . . . . . . . . . . 13 (2𝑜 ∈ 𝒫 suc 2𝑜 ↔ 2𝑜 ⊆ suc 2𝑜)
106, 9mpbir 222 . . . . . . . . . . . 12 2𝑜 ∈ 𝒫 suc 2𝑜
11 df2o3 7813 . . . . . . . . . . . 12 2𝑜 = {∅, 1𝑜}
12 df-3o 7801 . . . . . . . . . . . . . 14 3𝑜 = suc 2𝑜
1312eqcomi 2822 . . . . . . . . . . . . 13 suc 2𝑜 = 3𝑜
1413pweqi 4362 . . . . . . . . . . . 12 𝒫 suc 2𝑜 = 𝒫 3𝑜
1510, 11, 143eltr3i 2904 . . . . . . . . . . 11 {∅, 1𝑜} ∈ 𝒫 3𝑜
16152a1i 12 . . . . . . . . . 10 (𝑟 ∈ 𝒫 3𝑜 → (¬ ¬ 𝑟 = {∅} → {∅, 1𝑜} ∈ 𝒫 3𝑜))
175, 16jcad 504 . . . . . . . . 9 (𝑟 ∈ 𝒫 3𝑜 → (¬ ¬ 𝑟 = {∅} → (𝑟 = {∅} ∧ {∅, 1𝑜} ∈ 𝒫 3𝑜)))
1817con1d 141 . . . . . . . 8 (𝑟 ∈ 𝒫 3𝑜 → (¬ (𝑟 = {∅} ∧ {∅, 1𝑜} ∈ 𝒫 3𝑜) → ¬ 𝑟 = {∅}))
1918anc2ri 548 . . . . . . 7 (𝑟 ∈ 𝒫 3𝑜 → (¬ (𝑟 = {∅} ∧ {∅, 1𝑜} ∈ 𝒫 3𝑜) → (¬ 𝑟 = {∅} ∧ 𝑟 ∈ 𝒫 3𝑜)))
2019orrd 881 . . . . . 6 (𝑟 ∈ 𝒫 3𝑜 → ((𝑟 = {∅} ∧ {∅, 1𝑜} ∈ 𝒫 3𝑜) ∨ (¬ 𝑟 = {∅} ∧ 𝑟 ∈ 𝒫 3𝑜)))
21 ifel 4329 . . . . . 6 (if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟) ∈ 𝒫 3𝑜 ↔ ((𝑟 = {∅} ∧ {∅, 1𝑜} ∈ 𝒫 3𝑜) ∨ (¬ 𝑟 = {∅} ∧ 𝑟 ∈ 𝒫 3𝑜)))
2220, 21sylibr 225 . . . . 5 (𝑟 ∈ 𝒫 3𝑜 → if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟) ∈ 𝒫 3𝑜)
233, 22fmpti 6607 . . . 4 (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)):𝒫 3𝑜⟶𝒫 3𝑜
242pwex 5057 . . . . 5 𝒫 3𝑜 ∈ V
2524, 24elmap 8124 . . . 4 ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) ∈ (𝒫 3𝑜𝑚 𝒫 3𝑜) ↔ (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)):𝒫 3𝑜⟶𝒫 3𝑜)
2623, 25mpbir 222 . . 3 (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) ∈ (𝒫 3𝑜𝑚 𝒫 3𝑜)
273clsk1indlem0 38840 . . . . . 6 ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘∅) = ∅
283clsk1indlem2 38841 . . . . . 6 𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)
2927, 28pm3.2i 458 . . . . 5 (((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠))
303clsk1indlem3 38842 . . . . . 6 𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘(𝑠𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡))
313clsk1indlem4 38843 . . . . . 6 𝑠 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)
3230, 31pm3.2i 458 . . . . 5 (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘(𝑠𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠))
3329, 32pm3.2i 458 . . . 4 ((((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘(𝑠𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)))
343clsk1indlem1 38844 . . . 4 𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡))
3533, 34pm3.2i 458 . . 3 (((((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘(𝑠𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠))) ∧ ∃𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡)))
36 fveq1 6410 . . . . . . . 8 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (𝑘‘∅) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘∅))
3736eqeq1d 2815 . . . . . . 7 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → ((𝑘‘∅) = ∅ ↔ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘∅) = ∅))
38 fveq1 6410 . . . . . . . . 9 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (𝑘𝑠) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠))
3938sseq2d 3837 . . . . . . . 8 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (𝑠 ⊆ (𝑘𝑠) ↔ 𝑠 ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)))
4039ralbidv 3181 . . . . . . 7 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠) ↔ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)))
4137, 40anbi12d 618 . . . . . 6 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)) ↔ (((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠))))
42 fveq1 6410 . . . . . . . . 9 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (𝑘‘(𝑠𝑡)) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘(𝑠𝑡)))
43 fveq1 6410 . . . . . . . . . 10 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (𝑘𝑡) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡))
4438, 43uneq12d 3974 . . . . . . . . 9 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → ((𝑘𝑠) ∪ (𝑘𝑡)) = (((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡)))
4542, 44sseq12d 3838 . . . . . . . 8 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → ((𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘(𝑠𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡))))
46452ralbidv 3184 . . . . . . 7 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘(𝑠𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡))))
47 id 22 . . . . . . . . . 10 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → 𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)))
4847, 38fveq12d 6418 . . . . . . . . 9 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (𝑘‘(𝑘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)))
4948, 38eqeq12d 2828 . . . . . . . 8 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → ((𝑘‘(𝑘𝑠)) = (𝑘𝑠) ↔ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)))
5049ralbidv 3181 . . . . . . 7 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠) ↔ ∀𝑠 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)))
5146, 50anbi12d 618 . . . . . 6 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → ((∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠)) ↔ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘(𝑠𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠))))
5241, 51anbi12d 618 . . . . 5 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → ((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ↔ ((((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘(𝑠𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)))))
53 rexnal2 3238 . . . . . 6 (∃𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜 ¬ (𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ ¬ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))
54 pm4.61 393 . . . . . . . 8 (¬ (𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ (𝑠𝑡 ∧ ¬ (𝑘𝑠) ⊆ (𝑘𝑡)))
5538, 43sseq12d 3838 . . . . . . . . . 10 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → ((𝑘𝑠) ⊆ (𝑘𝑡) ↔ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡)))
5655notbid 309 . . . . . . . . 9 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (¬ (𝑘𝑠) ⊆ (𝑘𝑡) ↔ ¬ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡)))
5756anbi2d 616 . . . . . . . 8 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → ((𝑠𝑡 ∧ ¬ (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ (𝑠𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡))))
5854, 57syl5bb 274 . . . . . . 7 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (¬ (𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ (𝑠𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡))))
59582rexbidv 3252 . . . . . 6 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (∃𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜 ¬ (𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ ∃𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡))))
6053, 59syl5bbr 276 . . . . 5 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (¬ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ ∃𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡))))
6152, 60anbi12d 618 . . . 4 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡))) ↔ (((((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘(𝑠𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠))) ∧ ∃𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡)))))
6261rspcev 3509 . . 3 (((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) ∈ (𝒫 3𝑜𝑚 𝒫 3𝑜) ∧ (((((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘(𝑠𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠))) ∧ ∃𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡)))) → ∃𝑘 ∈ (𝒫 3𝑜𝑚 𝒫 3𝑜)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡))))
6326, 35, 62mp2an 675 . 2 𝑘 ∈ (𝒫 3𝑜𝑚 𝒫 3𝑜)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))
64 pweq 4361 . . . . . 6 (𝑏 = 3𝑜 → 𝒫 𝑏 = 𝒫 3𝑜)
6564, 64oveq12d 6895 . . . . 5 (𝑏 = 3𝑜 → (𝒫 𝑏𝑚 𝒫 𝑏) = (𝒫 3𝑜𝑚 𝒫 3𝑜))
66 pm4.61 393 . . . . . 6 (¬ (((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓) ↔ (((𝜑𝜒) ∧ (𝜃𝜏)) ∧ ¬ 𝜓))
67 clsnim.k0 . . . . . . . . . 10 (𝜑 ↔ (𝑘‘∅) = ∅)
6867a1i 11 . . . . . . . . 9 (𝑏 = 3𝑜 → (𝜑 ↔ (𝑘‘∅) = ∅))
69 clsnim.k2 . . . . . . . . . 10 (𝜒 ↔ ∀𝑠 ∈ 𝒫 𝑏𝑠 ⊆ (𝑘𝑠))
7064raleqdv 3340 . . . . . . . . . 10 (𝑏 = 3𝑜 → (∀𝑠 ∈ 𝒫 𝑏𝑠 ⊆ (𝑘𝑠) ↔ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)))
7169, 70syl5bb 274 . . . . . . . . 9 (𝑏 = 3𝑜 → (𝜒 ↔ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)))
7268, 71anbi12d 618 . . . . . . . 8 (𝑏 = 3𝑜 → ((𝜑𝜒) ↔ ((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠))))
73 clsnim.k3 . . . . . . . . . 10 (𝜃 ↔ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)))
7464raleqdv 3340 . . . . . . . . . . 11 (𝑏 = 3𝑜 → (∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ ∀𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡))))
7564, 74raleqbidv 3348 . . . . . . . . . 10 (𝑏 = 3𝑜 → (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡))))
7673, 75syl5bb 274 . . . . . . . . 9 (𝑏 = 3𝑜 → (𝜃 ↔ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡))))
77 clsnim.k4 . . . . . . . . . 10 (𝜏 ↔ ∀𝑠 ∈ 𝒫 𝑏(𝑘‘(𝑘𝑠)) = (𝑘𝑠))
7864raleqdv 3340 . . . . . . . . . 10 (𝑏 = 3𝑜 → (∀𝑠 ∈ 𝒫 𝑏(𝑘‘(𝑘𝑠)) = (𝑘𝑠) ↔ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠)))
7977, 78syl5bb 274 . . . . . . . . 9 (𝑏 = 3𝑜 → (𝜏 ↔ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠)))
8076, 79anbi12d 618 . . . . . . . 8 (𝑏 = 3𝑜 → ((𝜃𝜏) ↔ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠))))
8172, 80anbi12d 618 . . . . . . 7 (𝑏 = 3𝑜 → (((𝜑𝜒) ∧ (𝜃𝜏)) ↔ (((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠)))))
82 clsnim.k1 . . . . . . . . 9 (𝜓 ↔ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))
8364raleqdv 3340 . . . . . . . . . 10 (𝑏 = 3𝑜 → (∀𝑡 ∈ 𝒫 𝑏(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ ∀𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡))))
8464, 83raleqbidv 3348 . . . . . . . . 9 (𝑏 = 3𝑜 → (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡))))
8582, 84syl5bb 274 . . . . . . . 8 (𝑏 = 3𝑜 → (𝜓 ↔ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡))))
8685notbid 309 . . . . . . 7 (𝑏 = 3𝑜 → (¬ 𝜓 ↔ ¬ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡))))
8781, 86anbi12d 618 . . . . . 6 (𝑏 = 3𝑜 → ((((𝜑𝜒) ∧ (𝜃𝜏)) ∧ ¬ 𝜓) ↔ ((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))))
8866, 87syl5bb 274 . . . . 5 (𝑏 = 3𝑜 → (¬ (((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓) ↔ ((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))))
8965, 88rexeqbidv 3349 . . . 4 (𝑏 = 3𝑜 → (∃𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ¬ (((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓) ↔ ∃𝑘 ∈ (𝒫 3𝑜𝑚 𝒫 3𝑜)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))))
9089rspcev 3509 . . 3 ((3𝑜 ∈ V ∧ ∃𝑘 ∈ (𝒫 3𝑜𝑚 𝒫 3𝑜)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))) → ∃𝑏 ∈ V ∃𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ¬ (((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓))
91 rexnal2 3238 . . . 4 (∃𝑏 ∈ V ∃𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ¬ (((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓) ↔ ¬ ∀𝑏 ∈ V ∀𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓))
92 ralv 3420 . . . 4 (∀𝑏 ∈ V ∀𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓) ↔ ∀𝑏𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓))
9391, 92xchbinx 325 . . 3 (∃𝑏 ∈ V ∃𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ¬ (((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓) ↔ ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓))
9490, 93sylib 209 . 2 ((3𝑜 ∈ V ∧ ∃𝑘 ∈ (𝒫 3𝑜𝑚 𝒫 3𝑜)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))) → ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓))
952, 63, 94mp2an 675 1 ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  wal 1635   = wceq 1637  wcel 2157  wral 3103  wrex 3104  Vcvv 3398  cun 3774  wss 3776  c0 4123  ifcif 4286  𝒫 cpw 4358  {csn 4377  {cpr 4379  cmpt 4930  Oncon0 5943  suc csuc 5945  wf 6100  cfv 6104  (class class class)co 6877  1𝑜c1o 7792  2𝑜c2o 7793  3𝑜c3o 7794  𝑚 cmap 8095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-reg 8739
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-xor 1619  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3400  df-sbc 3641  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-ord 5946  df-on 5947  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-fv 6112  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-1o 7799  df-2o 7800  df-3o 7801  df-map 8097
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator