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 40531
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 8092 . . 3 3o ∈ On
21elexi 3492 . 2 3o ∈ V
3 eqid 2820 . . . . 5 (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))
4 notnotr 132 . . . . . . . . . . 11 (¬ ¬ 𝑟 = {∅} → 𝑟 = {∅})
54a1i 11 . . . . . . . . . 10 (𝑟 ∈ 𝒫 3o → (¬ ¬ 𝑟 = {∅} → 𝑟 = {∅}))
6 sssucid 6244 . . . . . . . . . . . . 13 2o ⊆ suc 2o
7 2oex 8090 . . . . . . . . . . . . . 14 2o ∈ V
87elpw 4519 . . . . . . . . . . . . 13 (2o ∈ 𝒫 suc 2o ↔ 2o ⊆ suc 2o)
96, 8mpbir 233 . . . . . . . . . . . 12 2o ∈ 𝒫 suc 2o
10 df2o3 8095 . . . . . . . . . . . 12 2o = {∅, 1o}
11 df-3o 8082 . . . . . . . . . . . . . 14 3o = suc 2o
1211eqcomi 2829 . . . . . . . . . . . . 13 suc 2o = 3o
1312pweqi 4533 . . . . . . . . . . . 12 𝒫 suc 2o = 𝒫 3o
149, 10, 133eltr3i 2923 . . . . . . . . . . 11 {∅, 1o} ∈ 𝒫 3o
15142a1i 12 . . . . . . . . . 10 (𝑟 ∈ 𝒫 3o → (¬ ¬ 𝑟 = {∅} → {∅, 1o} ∈ 𝒫 3o))
165, 15jcad 515 . . . . . . . . 9 (𝑟 ∈ 𝒫 3o → (¬ ¬ 𝑟 = {∅} → (𝑟 = {∅} ∧ {∅, 1o} ∈ 𝒫 3o)))
1716con1d 147 . . . . . . . 8 (𝑟 ∈ 𝒫 3o → (¬ (𝑟 = {∅} ∧ {∅, 1o} ∈ 𝒫 3o) → ¬ 𝑟 = {∅}))
1817anc2ri 559 . . . . . . 7 (𝑟 ∈ 𝒫 3o → (¬ (𝑟 = {∅} ∧ {∅, 1o} ∈ 𝒫 3o) → (¬ 𝑟 = {∅} ∧ 𝑟 ∈ 𝒫 3o)))
1918orrd 859 . . . . . 6 (𝑟 ∈ 𝒫 3o → ((𝑟 = {∅} ∧ {∅, 1o} ∈ 𝒫 3o) ∨ (¬ 𝑟 = {∅} ∧ 𝑟 ∈ 𝒫 3o)))
20 ifel 4486 . . . . . 6 (if(𝑟 = {∅}, {∅, 1o}, 𝑟) ∈ 𝒫 3o ↔ ((𝑟 = {∅} ∧ {∅, 1o} ∈ 𝒫 3o) ∨ (¬ 𝑟 = {∅} ∧ 𝑟 ∈ 𝒫 3o)))
2119, 20sylibr 236 . . . . 5 (𝑟 ∈ 𝒫 3o → if(𝑟 = {∅}, {∅, 1o}, 𝑟) ∈ 𝒫 3o)
223, 21fmpti 6852 . . . 4 (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)):𝒫 3o⟶𝒫 3o
232pwex 5257 . . . . 5 𝒫 3o ∈ V
2423, 23elmap 8413 . . . 4 ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) ∈ (𝒫 3om 𝒫 3o) ↔ (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)):𝒫 3o⟶𝒫 3o)
2522, 24mpbir 233 . . 3 (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) ∈ (𝒫 3om 𝒫 3o)
263clsk1indlem0 40526 . . . . . 6 ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘∅) = ∅
273clsk1indlem2 40527 . . . . . 6 𝑠 ∈ 𝒫 3o𝑠 ⊆ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠)
2826, 27pm3.2i 473 . . . . 5 (((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠))
293clsk1indlem3 40528 . . . . . 6 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘(𝑠𝑡)) ⊆ (((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑡))
303clsk1indlem4 40529 . . . . . 6 𝑠 ∈ 𝒫 3o((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠)
3129, 30pm3.2i 473 . . . . 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 473 . . . 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 40530 . . . 4 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑠𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑡))
3432, 33pm3.2i 473 . . 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 6645 . . . . . . . 8 (𝑘 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) → (𝑘‘∅) = ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘∅))
3635eqeq1d 2822 . . . . . . 7 (𝑘 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) → ((𝑘‘∅) = ∅ ↔ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘∅) = ∅))
37 fveq1 6645 . . . . . . . . 9 (𝑘 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) → (𝑘𝑠) = ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠))
3837sseq2d 3978 . . . . . . . 8 (𝑘 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) → (𝑠 ⊆ (𝑘𝑠) ↔ 𝑠 ⊆ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠)))
3938ralbidv 3184 . . . . . . 7 (𝑘 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) → (∀𝑠 ∈ 𝒫 3o𝑠 ⊆ (𝑘𝑠) ↔ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠)))
4036, 39anbi12d 632 . . . . . 6 (𝑘 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) → (((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ (𝑘𝑠)) ↔ (((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠))))
41 fveq1 6645 . . . . . . . . 9 (𝑘 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) → (𝑘‘(𝑠𝑡)) = ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘(𝑠𝑡)))
42 fveq1 6645 . . . . . . . . . 10 (𝑘 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) → (𝑘𝑡) = ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑡))
4337, 42uneq12d 4119 . . . . . . . . 9 (𝑘 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) → ((𝑘𝑠) ∪ (𝑘𝑡)) = (((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑡)))
4441, 43sseq12d 3979 . . . . . . . 8 (𝑘 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) → ((𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘(𝑠𝑡)) ⊆ (((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑡))))
45442ralbidv 3186 . . . . . . 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 6653 . . . . . . . . 9 (𝑘 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) → (𝑘‘(𝑘𝑠)) = ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠)))
4847, 37eqeq12d 2836 . . . . . . . 8 (𝑘 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) → ((𝑘‘(𝑘𝑠)) = (𝑘𝑠) ↔ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠)))
4948ralbidv 3184 . . . . . . 7 (𝑘 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) → (∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘𝑠)) = (𝑘𝑠) ↔ ∀𝑠 ∈ 𝒫 3o((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠)))
5045, 49anbi12d 632 . . . . . 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 632 . . . . 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 3245 . . . . . 6 (∃𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o ¬ (𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ ¬ ∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))
53 pm4.61 407 . . . . . . . 8 (¬ (𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ (𝑠𝑡 ∧ ¬ (𝑘𝑠) ⊆ (𝑘𝑡)))
5437, 42sseq12d 3979 . . . . . . . . . 10 (𝑘 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) → ((𝑘𝑠) ⊆ (𝑘𝑡) ↔ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑡)))
5554notbid 320 . . . . . . . . 9 (𝑘 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) → (¬ (𝑘𝑠) ⊆ (𝑘𝑡) ↔ ¬ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑡)))
5655anbi2d 630 . . . . . . . 8 (𝑘 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) → ((𝑠𝑡 ∧ ¬ (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ (𝑠𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑡))))
5753, 56syl5bb 285 . . . . . . 7 (𝑘 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) → (¬ (𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ (𝑠𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑡))))
58572rexbidv 3287 . . . . . 6 (𝑘 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) → (∃𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o ¬ (𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ ∃𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑠𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑡))))
5952, 58syl5bbr 287 . . . . 5 (𝑘 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) → (¬ ∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ ∃𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑠𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑡))))
6051, 59anbi12d 632 . . . 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 3602 . . 3 (((𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) ∈ (𝒫 3om 𝒫 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}, 𝑟))‘𝑡)))) → ∃𝑘 ∈ (𝒫 3om 𝒫 3o)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡))))
6225, 34, 61mp2an 690 . 2 𝑘 ∈ (𝒫 3om 𝒫 3o)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))
63 pweq 4531 . . . . . 6 (𝑏 = 3o → 𝒫 𝑏 = 𝒫 3o)
6463, 63oveq12d 7151 . . . . 5 (𝑏 = 3o → (𝒫 𝑏m 𝒫 𝑏) = (𝒫 3om 𝒫 3o))
65 pm4.61 407 . . . . . 6 (¬ (((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓) ↔ (((𝜑𝜒) ∧ (𝜃𝜏)) ∧ ¬ 𝜓))
66 clsnim.k0 . . . . . . . . . 10 (𝜑 ↔ (𝑘‘∅) = ∅)
6766a1i 11 . . . . . . . . 9 (𝑏 = 3o → (𝜑 ↔ (𝑘‘∅) = ∅))
68 clsnim.k2 . . . . . . . . . 10 (𝜒 ↔ ∀𝑠 ∈ 𝒫 𝑏𝑠 ⊆ (𝑘𝑠))
6963raleqdv 3398 . . . . . . . . . 10 (𝑏 = 3o → (∀𝑠 ∈ 𝒫 𝑏𝑠 ⊆ (𝑘𝑠) ↔ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ (𝑘𝑠)))
7068, 69syl5bb 285 . . . . . . . . 9 (𝑏 = 3o → (𝜒 ↔ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ (𝑘𝑠)))
7167, 70anbi12d 632 . . . . . . . 8 (𝑏 = 3o → ((𝜑𝜒) ↔ ((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ (𝑘𝑠))))
72 clsnim.k3 . . . . . . . . . 10 (𝜃 ↔ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)))
7363raleqdv 3398 . . . . . . . . . . 11 (𝑏 = 3o → (∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ ∀𝑡 ∈ 𝒫 3o(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡))))
7463, 73raleqbidv 3388 . . . . . . . . . 10 (𝑏 = 3o → (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ ∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡))))
7572, 74syl5bb 285 . . . . . . . . 9 (𝑏 = 3o → (𝜃 ↔ ∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡))))
76 clsnim.k4 . . . . . . . . . 10 (𝜏 ↔ ∀𝑠 ∈ 𝒫 𝑏(𝑘‘(𝑘𝑠)) = (𝑘𝑠))
7763raleqdv 3398 . . . . . . . . . 10 (𝑏 = 3o → (∀𝑠 ∈ 𝒫 𝑏(𝑘‘(𝑘𝑠)) = (𝑘𝑠) ↔ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘𝑠)) = (𝑘𝑠)))
7876, 77syl5bb 285 . . . . . . . . 9 (𝑏 = 3o → (𝜏 ↔ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘𝑠)) = (𝑘𝑠)))
7975, 78anbi12d 632 . . . . . . . 8 (𝑏 = 3o → ((𝜃𝜏) ↔ (∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘𝑠)) = (𝑘𝑠))))
8071, 79anbi12d 632 . . . . . . 7 (𝑏 = 3o → (((𝜑𝜒) ∧ (𝜃𝜏)) ↔ (((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘𝑠)) = (𝑘𝑠)))))
81 clsnim.k1 . . . . . . . . 9 (𝜓 ↔ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))
8263raleqdv 3398 . . . . . . . . . 10 (𝑏 = 3o → (∀𝑡 ∈ 𝒫 𝑏(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ ∀𝑡 ∈ 𝒫 3o(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡))))
8363, 82raleqbidv 3388 . . . . . . . . 9 (𝑏 = 3o → (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)) ↔ ∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡))))
8481, 83syl5bb 285 . . . . . . . 8 (𝑏 = 3o → (𝜓 ↔ ∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡))))
8584notbid 320 . . . . . . 7 (𝑏 = 3o → (¬ 𝜓 ↔ ¬ ∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡))))
8680, 85anbi12d 632 . . . . . 6 (𝑏 = 3o → ((((𝜑𝜒) ∧ (𝜃𝜏)) ∧ ¬ 𝜓) ↔ ((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))))
8765, 86syl5bb 285 . . . . 5 (𝑏 = 3o → (¬ (((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓) ↔ ((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))))
8864, 87rexeqbidv 3389 . . . 4 (𝑏 = 3o → (∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏) ¬ (((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓) ↔ ∃𝑘 ∈ (𝒫 3om 𝒫 3o)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))))
8988rspcev 3602 . . 3 ((3o ∈ V ∧ ∃𝑘 ∈ (𝒫 3om 𝒫 3o)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))) → ∃𝑏 ∈ V ∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏) ¬ (((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓))
90 rexnal2 3245 . . . 4 (∃𝑏 ∈ V ∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏) ¬ (((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓) ↔ ¬ ∀𝑏 ∈ V ∀𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓))
91 ralv 3498 . . . 4 (∀𝑏 ∈ V ∀𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓) ↔ ∀𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓))
9290, 91xchbinx 336 . . 3 (∃𝑏 ∈ V ∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏) ¬ (((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓) ↔ ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓))
9389, 92sylib 220 . 2 ((3o ∈ V ∧ ∃𝑘 ∈ (𝒫 3om 𝒫 3o)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ (𝑘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘𝑠)) = (𝑘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝑠𝑡 → (𝑘𝑠) ⊆ (𝑘𝑡)))) → ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓))
942, 62, 93mp2an 690 1 ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(((𝜑𝜒) ∧ (𝜃𝜏)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wo 843  wal 1535   = wceq 1537  wcel 2114  wral 3125  wrex 3126  Vcvv 3473  cun 3911  wss 3913  c0 4269  ifcif 4443  𝒫 cpw 4515  {csn 4543  {cpr 4545  cmpt 5122  Oncon0 6167  suc csuc 6169  wf 6327  cfv 6331  (class class class)co 7133  1oc1o 8073  2oc2o 8074  3oc3o 8075  m cmap 8384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439  ax-reg 9034
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-xor 1502  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3475  df-sbc 3753  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-uni 4815  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5436  df-eprel 5441  df-po 5450  df-so 5451  df-fr 5490  df-we 5492  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-ord 6170  df-on 6171  df-suc 6173  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-fv 6339  df-ov 7136  df-oprab 7137  df-mpo 7138  df-1o 8080  df-2o 8081  df-3o 8082  df-map 8386
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator