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 38863
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 7723 . . 3 3𝑜 ∈ On
21elexi 3362 . 2 3𝑜 ∈ V
3 eqid 2770 . . . . 5 (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))
4 notnotr 128 . . . . . . . . . . 11 (¬ ¬ 𝑟 = {∅} → 𝑟 = {∅})
54a1i 11 . . . . . . . . . 10 (𝑟 ∈ 𝒫 3𝑜 → (¬ ¬ 𝑟 = {∅} → 𝑟 = {∅}))
6 sssucid 5945 . . . . . . . . . . . . 13 2𝑜 ⊆ suc 2𝑜
7 2on 7721 . . . . . . . . . . . . . . 15 2𝑜 ∈ On
87elexi 3362 . . . . . . . . . . . . . 14 2𝑜 ∈ V
98elpw 4301 . . . . . . . . . . . . 13 (2𝑜 ∈ 𝒫 suc 2𝑜 ↔ 2𝑜 ⊆ suc 2𝑜)
106, 9mpbir 221 . . . . . . . . . . . 12 2𝑜 ∈ 𝒫 suc 2𝑜
11 df2o3 7726 . . . . . . . . . . . 12 2𝑜 = {∅, 1𝑜}
12 df-3o 7714 . . . . . . . . . . . . . 14 3𝑜 = suc 2𝑜
1312eqcomi 2779 . . . . . . . . . . . . 13 suc 2𝑜 = 3𝑜
1413pweqi 4299 . . . . . . . . . . . 12 𝒫 suc 2𝑜 = 𝒫 3𝑜
1510, 11, 143eltr3i 2861 . . . . . . . . . . 11 {∅, 1𝑜} ∈ 𝒫 3𝑜
16152a1i 12 . . . . . . . . . 10 (𝑟 ∈ 𝒫 3𝑜 → (¬ ¬ 𝑟 = {∅} → {∅, 1𝑜} ∈ 𝒫 3𝑜))
175, 16jcad 496 . . . . . . . . 9 (𝑟 ∈ 𝒫 3𝑜 → (¬ ¬ 𝑟 = {∅} → (𝑟 = {∅} ∧ {∅, 1𝑜} ∈ 𝒫 3𝑜)))
1817con1d 141 . . . . . . . 8 (𝑟 ∈ 𝒫 3𝑜 → (¬ (𝑟 = {∅} ∧ {∅, 1𝑜} ∈ 𝒫 3𝑜) → ¬ 𝑟 = {∅}))
1918anc2ri 538 . . . . . . 7 (𝑟 ∈ 𝒫 3𝑜 → (¬ (𝑟 = {∅} ∧ {∅, 1𝑜} ∈ 𝒫 3𝑜) → (¬ 𝑟 = {∅} ∧ 𝑟 ∈ 𝒫 3𝑜)))
2019orrd 843 . . . . . 6 (𝑟 ∈ 𝒫 3𝑜 → ((𝑟 = {∅} ∧ {∅, 1𝑜} ∈ 𝒫 3𝑜) ∨ (¬ 𝑟 = {∅} ∧ 𝑟 ∈ 𝒫 3𝑜)))
21 ifel 4266 . . . . . 6 (if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟) ∈ 𝒫 3𝑜 ↔ ((𝑟 = {∅} ∧ {∅, 1𝑜} ∈ 𝒫 3𝑜) ∨ (¬ 𝑟 = {∅} ∧ 𝑟 ∈ 𝒫 3𝑜)))
2220, 21sylibr 224 . . . . 5 (𝑟 ∈ 𝒫 3𝑜 → if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟) ∈ 𝒫 3𝑜)
233, 22fmpti 6525 . . . 4 (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)):𝒫 3𝑜⟶𝒫 3𝑜
242pwex 4976 . . . . 5 𝒫 3𝑜 ∈ V
2524, 24elmap 8037 . . . 4 ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) ∈ (𝒫 3𝑜𝑚 𝒫 3𝑜) ↔ (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)):𝒫 3𝑜⟶𝒫 3𝑜)
2623, 25mpbir 221 . . 3 (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) ∈ (𝒫 3𝑜𝑚 𝒫 3𝑜)
273clsk1indlem0 38858 . . . . . 6 ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘∅) = ∅
283clsk1indlem2 38859 . . . . . 6 𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)
2927, 28pm3.2i 447 . . . . 5 (((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠))
303clsk1indlem3 38860 . . . . . 6 𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘(𝑠𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡))
313clsk1indlem4 38861 . . . . . 6 𝑠 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)
3230, 31pm3.2i 447 . . . . 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 447 . . . 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 38862 . . . 4 𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡))
3533, 34pm3.2i 447 . . 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 6331 . . . . . . . 8 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (𝑘‘∅) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘∅))
3736eqeq1d 2772 . . . . . . 7 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → ((𝑘‘∅) = ∅ ↔ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘∅) = ∅))
38 fveq1 6331 . . . . . . . . 9 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (𝑘𝑠) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠))
3938sseq2d 3780 . . . . . . . 8 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (𝑠 ⊆ (𝑘𝑠) ↔ 𝑠 ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)))
4039ralbidv 3134 . . . . . . 7 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠) ↔ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)))
4137, 40anbi12d 608 . . . . . 6 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)) ↔ (((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠))))
42 fveq1 6331 . . . . . . . . 9 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (𝑘‘(𝑠𝑡)) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘(𝑠𝑡)))
43 fveq1 6331 . . . . . . . . . 10 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (𝑘𝑡) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡))
4438, 43uneq12d 3917 . . . . . . . . 9 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → ((𝑘𝑠) ∪ (𝑘𝑡)) = (((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡)))
4542, 44sseq12d 3781 . . . . . . . 8 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → ((𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘(𝑠𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡))))
46452ralbidv 3137 . . . . . . 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 6338 . . . . . . . . 9 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (𝑘‘(𝑘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)))
4948, 38eqeq12d 2785 . . . . . . . 8 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → ((𝑘‘(𝑘𝑠)) = (𝑘𝑠) ↔ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)))
5049ralbidv 3134 . . . . . . 7 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠) ↔ ∀𝑠 ∈ 𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠)))
5146, 50anbi12d 608 . . . . . 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 608 . . . . 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 3190 . . . . . 6 (∃𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜 ¬ (𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ ¬ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))
54 pm4.61 391 . . . . . . . 8 (¬ (𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ (𝑠𝑡 ∧ ¬ (𝑘𝑠) ⊆ (𝑘𝑡)))
5538, 43sseq12d 3781 . . . . . . . . . 10 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → ((𝑘𝑠) ⊆ (𝑘𝑡) ↔ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡)))
5655notbid 307 . . . . . . . . 9 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (¬ (𝑘𝑠) ⊆ (𝑘𝑡) ↔ ¬ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡)))
5756anbi2d 606 . . . . . . . 8 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → ((𝑠𝑡 ∧ ¬ (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ (𝑠𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡))))
5854, 57syl5bb 272 . . . . . . 7 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (¬ (𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ (𝑠𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡))))
59582rexbidv 3204 . . . . . 6 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (∃𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜 ¬ (𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ ∃𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡))))
6053, 59syl5bbr 274 . . . . 5 (𝑘 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟)) → (¬ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ ∃𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))‘𝑡))))
6152, 60anbi12d 608 . . . 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 3458 . . 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 664 . 2 𝑘 ∈ (𝒫 3𝑜𝑚 𝒫 3𝑜)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))
64 pweq 4298 . . . . . 6 (𝑏 = 3𝑜 → 𝒫 𝑏 = 𝒫 3𝑜)
6564, 64oveq12d 6810 . . . . 5 (𝑏 = 3𝑜 → (𝒫 𝑏𝑚 𝒫 𝑏) = (𝒫 3𝑜𝑚 𝒫 3𝑜))
66 pm4.61 391 . . . . . 6 (¬ (((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓) ↔ (((𝜑𝜒) ∧ (𝜃𝜏)) ∧ ¬ 𝜓))
67 clsnim.k0 . . . . . . . . . 10 (𝜑 ↔ (𝑘‘∅) = ∅)
6867a1i 11 . . . . . . . . 9 (𝑏 = 3𝑜 → (𝜑 ↔ (𝑘‘∅) = ∅))
69 clsnim.k2 . . . . . . . . . 10 (𝜒 ↔ ∀𝑠 ∈ 𝒫 𝑏𝑠 ⊆ (𝑘𝑠))
7064raleqdv 3292 . . . . . . . . . 10 (𝑏 = 3𝑜 → (∀𝑠 ∈ 𝒫 𝑏𝑠 ⊆ (𝑘𝑠) ↔ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)))
7169, 70syl5bb 272 . . . . . . . . 9 (𝑏 = 3𝑜 → (𝜒 ↔ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)))
7268, 71anbi12d 608 . . . . . . . 8 (𝑏 = 3𝑜 → ((𝜑𝜒) ↔ ((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠))))
73 clsnim.k3 . . . . . . . . . 10 (𝜃 ↔ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)))
7464raleqdv 3292 . . . . . . . . . . 11 (𝑏 = 3𝑜 → (∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ ∀𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡))))
7564, 74raleqbidv 3300 . . . . . . . . . 10 (𝑏 = 3𝑜 → (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡))))
7673, 75syl5bb 272 . . . . . . . . 9 (𝑏 = 3𝑜 → (𝜃 ↔ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡))))
77 clsnim.k4 . . . . . . . . . 10 (𝜏 ↔ ∀𝑠 ∈ 𝒫 𝑏(𝑘‘(𝑘𝑠)) = (𝑘𝑠))
7864raleqdv 3292 . . . . . . . . . 10 (𝑏 = 3𝑜 → (∀𝑠 ∈ 𝒫 𝑏(𝑘‘(𝑘𝑠)) = (𝑘𝑠) ↔ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠)))
7977, 78syl5bb 272 . . . . . . . . 9 (𝑏 = 3𝑜 → (𝜏 ↔ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠)))
8076, 79anbi12d 608 . . . . . . . 8 (𝑏 = 3𝑜 → ((𝜃𝜏) ↔ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠))))
8172, 80anbi12d 608 . . . . . . 7 (𝑏 = 3𝑜 → (((𝜑𝜒) ∧ (𝜃𝜏)) ↔ (((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠)))))
82 clsnim.k1 . . . . . . . . 9 (𝜓 ↔ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))
8364raleqdv 3292 . . . . . . . . . 10 (𝑏 = 3𝑜 → (∀𝑡 ∈ 𝒫 𝑏(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ ∀𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡))))
8464, 83raleqbidv 3300 . . . . . . . . 9 (𝑏 = 3𝑜 → (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡))))
8582, 84syl5bb 272 . . . . . . . 8 (𝑏 = 3𝑜 → (𝜓 ↔ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡))))
8685notbid 307 . . . . . . 7 (𝑏 = 3𝑜 → (¬ 𝜓 ↔ ¬ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡))))
8781, 86anbi12d 608 . . . . . 6 (𝑏 = 3𝑜 → ((((𝜑𝜒) ∧ (𝜃𝜏)) ∧ ¬ 𝜓) ↔ ((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))))
8866, 87syl5bb 272 . . . . 5 (𝑏 = 3𝑜 → (¬ (((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓) ↔ ((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))))
8965, 88rexeqbidv 3301 . . . 4 (𝑏 = 3𝑜 → (∃𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ¬ (((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓) ↔ ∃𝑘 ∈ (𝒫 3𝑜𝑚 𝒫 3𝑜)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))))
9089rspcev 3458 . . 3 ((3𝑜 ∈ V ∧ ∃𝑘 ∈ (𝒫 3𝑜𝑚 𝒫 3𝑜)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))) → ∃𝑏 ∈ V ∃𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ¬ (((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓))
91 rexnal2 3190 . . . 4 (∃𝑏 ∈ V ∃𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ¬ (((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓) ↔ ¬ ∀𝑏 ∈ V ∀𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓))
92 ralv 3368 . . . 4 (∀𝑏 ∈ V ∀𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓) ↔ ∀𝑏𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓))
9391, 92xchbinx 323 . . 3 (∃𝑏 ∈ V ∃𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ¬ (((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓) ↔ ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓))
9490, 93sylib 208 . 2 ((3𝑜 ∈ V ∧ ∃𝑘 ∈ (𝒫 3𝑜𝑚 𝒫 3𝑜)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))) → ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓))
952, 63, 94mp2an 664 1 ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wo 826  wal 1628   = wceq 1630  wcel 2144  wral 3060  wrex 3061  Vcvv 3349  cun 3719  wss 3721  c0 4061  ifcif 4223  𝒫 cpw 4295  {csn 4314  {cpr 4316  cmpt 4861  Oncon0 5866  suc csuc 5868  wf 6027  cfv 6031  (class class class)co 6792  1𝑜c1o 7705  2𝑜c2o 7706  3𝑜c3o 7707  𝑚 cmap 8008
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095  ax-reg 8652
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1071  df-3an 1072  df-xor 1612  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-sbc 3586  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-pss 3737  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-tp 4319  df-op 4321  df-uni 4573  df-br 4785  df-opab 4845  df-mpt 4862  df-tr 4885  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-ord 5869  df-on 5870  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-fv 6039  df-ov 6795  df-oprab 6796  df-mpt2 6797  df-1o 7712  df-2o 7713  df-3o 7714  df-map 8010
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator