Metamath Proof Explorer

Theorem clsk1independent

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)

Ref Expression
Hypotheses clsnim.k0 ⊢ φ ↔ k ⁡ ∅ = ∅
clsnim.k1 ⊢ ψ ↔ ∀ s ∈ 𝒫 b ∀ t ∈ 𝒫 b s ⊆ t → k ⁡ s ⊆ k ⁡ t
clsnim.k2 ⊢ χ ↔ ∀ s ∈ 𝒫 b s ⊆ k ⁡ s
clsnim.k3 ⊢ θ ↔ ∀ s ∈ 𝒫 b ∀ t ∈ 𝒫 b k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t
clsnim.k4 ⊢ τ ↔ ∀ s ∈ 𝒫 b k ⁡ k ⁡ s = k ⁡ s
Assertion clsk1independent ⊢ ¬ ∀ b ∀ k ∈ 𝒫 b 𝒫 b φ ∧ χ ∧ θ ∧ τ → ψ

Proof

Step Hyp Ref Expression
1 clsnim.k0 ⊢ φ ↔ k ⁡ ∅ = ∅
2 clsnim.k1 ⊢ ψ ↔ ∀ s ∈ 𝒫 b ∀ t ∈ 𝒫 b s ⊆ t → k ⁡ s ⊆ k ⁡ t
3 clsnim.k2 ⊢ χ ↔ ∀ s ∈ 𝒫 b s ⊆ k ⁡ s
4 clsnim.k3 ⊢ θ ↔ ∀ s ∈ 𝒫 b ∀ t ∈ 𝒫 b k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t
5 clsnim.k4 ⊢ τ ↔ ∀ s ∈ 𝒫 b k ⁡ k ⁡ s = k ⁡ s
6 3on ⊢ 3 𝑜 ∈ On
7 6 elexi ⊢ 3 𝑜 ∈ V
8 eqid ⊢ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r
9 notnotr ⊢ ¬ ¬ r = ∅ → r = ∅
10 9 a1i ⊢ r ∈ 𝒫 3 𝑜 → ¬ ¬ r = ∅ → r = ∅
11 sssucid ⊢ 2 𝑜 ⊆ suc ⁡ 2 𝑜
12 2oex ⊢ 2 𝑜 ∈ V
13 12 elpw ⊢ 2 𝑜 ∈ 𝒫 suc ⁡ 2 𝑜 ↔ 2 𝑜 ⊆ suc ⁡ 2 𝑜
14 11 13 mpbir ⊢ 2 𝑜 ∈ 𝒫 suc ⁡ 2 𝑜
15 df2o3 ⊢ 2 𝑜 = ∅ 1 𝑜
16 df-3o ⊢ 3 𝑜 = suc ⁡ 2 𝑜
17 16 eqcomi ⊢ suc ⁡ 2 𝑜 = 3 𝑜
18 17 pweqi ⊢ 𝒫 suc ⁡ 2 𝑜 = 𝒫 3 𝑜
19 14 15 18 3eltr3i ⊢ ∅ 1 𝑜 ∈ 𝒫 3 𝑜
20 19 2a1i ⊢ r ∈ 𝒫 3 𝑜 → ¬ ¬ r = ∅ → ∅ 1 𝑜 ∈ 𝒫 3 𝑜
21 10 20 jcad ⊢ r ∈ 𝒫 3 𝑜 → ¬ ¬ r = ∅ → r = ∅ ∧ ∅ 1 𝑜 ∈ 𝒫 3 𝑜
22 21 con1d ⊢ r ∈ 𝒫 3 𝑜 → ¬ r = ∅ ∧ ∅ 1 𝑜 ∈ 𝒫 3 𝑜 → ¬ r = ∅
23 22 anc2ri ⊢ r ∈ 𝒫 3 𝑜 → ¬ r = ∅ ∧ ∅ 1 𝑜 ∈ 𝒫 3 𝑜 → ¬ r = ∅ ∧ r ∈ 𝒫 3 𝑜
24 23 orrd ⊢ r ∈ 𝒫 3 𝑜 → r = ∅ ∧ ∅ 1 𝑜 ∈ 𝒫 3 𝑜 ∨ ¬ r = ∅ ∧ r ∈ 𝒫 3 𝑜
25 ifel ⊢ if r = ∅ ∅ 1 𝑜 r ∈ 𝒫 3 𝑜 ↔ r = ∅ ∧ ∅ 1 𝑜 ∈ 𝒫 3 𝑜 ∨ ¬ r = ∅ ∧ r ∈ 𝒫 3 𝑜
26 24 25 sylibr ⊢ r ∈ 𝒫 3 𝑜 → if r = ∅ ∅ 1 𝑜 r ∈ 𝒫 3 𝑜
27 8 26 fmpti ⊢ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r : 𝒫 3 𝑜 ⟶ 𝒫 3 𝑜
28 7 pwex ⊢ 𝒫 3 𝑜 ∈ V
29 28 28 elmap ⊢ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ∈ 𝒫 3 𝑜 𝒫 3 𝑜 ↔ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r : 𝒫 3 𝑜 ⟶ 𝒫 3 𝑜
30 27 29 mpbir ⊢ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ∈ 𝒫 3 𝑜 𝒫 3 𝑜
31 8 clsk1indlem0 ⊢ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ ∅ = ∅
32 8 clsk1indlem2 ⊢ ∀ s ∈ 𝒫 3 𝑜 s ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s
33 31 32 pm3.2i ⊢ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ ∅ = ∅ ∧ ∀ s ∈ 𝒫 3 𝑜 s ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s
34 8 clsk1indlem3 ⊢ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ t ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t
35 8 clsk1indlem4 ⊢ ∀ s ∈ 𝒫 3 𝑜 r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s
36 34 35 pm3.2i ⊢ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ t ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t ∧ ∀ s ∈ 𝒫 3 𝑜 r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s
37 33 36 pm3.2i ⊢ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ ∅ = ∅ ∧ ∀ s ∈ 𝒫 3 𝑜 s ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∧ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ t ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t ∧ ∀ s ∈ 𝒫 3 𝑜 r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s
38 8 clsk1indlem1 ⊢ ∃ s ∈ 𝒫 3 𝑜 ∃ t ∈ 𝒫 3 𝑜 s ⊆ t ∧ ¬ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t
39 37 38 pm3.2i ⊢ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ ∅ = ∅ ∧ ∀ s ∈ 𝒫 3 𝑜 s ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∧ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ t ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t ∧ ∀ s ∈ 𝒫 3 𝑜 r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∧ ∃ s ∈ 𝒫 3 𝑜 ∃ t ∈ 𝒫 3 𝑜 s ⊆ t ∧ ¬ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t
40 fveq1 ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → k ⁡ ∅ = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ ∅
41 40 eqeq1d ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → k ⁡ ∅ = ∅ ↔ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ ∅ = ∅
42 fveq1 ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → k ⁡ s = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s
43 42 sseq2d ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → s ⊆ k ⁡ s ↔ s ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s
44 43 ralbidv ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → ∀ s ∈ 𝒫 3 𝑜 s ⊆ k ⁡ s ↔ ∀ s ∈ 𝒫 3 𝑜 s ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s
45 41 44 anbi12d ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → k ⁡ ∅ = ∅ ∧ ∀ s ∈ 𝒫 3 𝑜 s ⊆ k ⁡ s ↔ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ ∅ = ∅ ∧ ∀ s ∈ 𝒫 3 𝑜 s ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s
46 fveq1 ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → k ⁡ s ∪ t = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ t
47 fveq1 ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → k ⁡ t = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t
48 42 47 uneq12d ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → k ⁡ s ∪ k ⁡ t = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t
49 46 48 sseq12d ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t ↔ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ t ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t
50 49 2ralbidv ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t ↔ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ t ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t
51 id ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r
52 51 42 fveq12d ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → k ⁡ k ⁡ s = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s
53 52 42 eqeq12d ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → k ⁡ k ⁡ s = k ⁡ s ↔ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s
54 53 ralbidv ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → ∀ s ∈ 𝒫 3 𝑜 k ⁡ k ⁡ s = k ⁡ s ↔ ∀ s ∈ 𝒫 3 𝑜 r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s
55 50 54 anbi12d ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t ∧ ∀ s ∈ 𝒫 3 𝑜 k ⁡ k ⁡ s = k ⁡ s ↔ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ t ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t ∧ ∀ s ∈ 𝒫 3 𝑜 r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s
56 45 55 anbi12d ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → k ⁡ ∅ = ∅ ∧ ∀ s ∈ 𝒫 3 𝑜 s ⊆ k ⁡ s ∧ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t ∧ ∀ s ∈ 𝒫 3 𝑜 k ⁡ k ⁡ s = k ⁡ s ↔ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ ∅ = ∅ ∧ ∀ s ∈ 𝒫 3 𝑜 s ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∧ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ t ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t ∧ ∀ s ∈ 𝒫 3 𝑜 r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s
57 rexnal2 ⊢ ∃ s ∈ 𝒫 3 𝑜 ∃ t ∈ 𝒫 3 𝑜 ¬ s ⊆ t → k ⁡ s ⊆ k ⁡ t ↔ ¬ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 s ⊆ t → k ⁡ s ⊆ k ⁡ t
58 pm4.61 ⊢ ¬ s ⊆ t → k ⁡ s ⊆ k ⁡ t ↔ s ⊆ t ∧ ¬ k ⁡ s ⊆ k ⁡ t
59 42 47 sseq12d ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → k ⁡ s ⊆ k ⁡ t ↔ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t
60 59 notbid ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → ¬ k ⁡ s ⊆ k ⁡ t ↔ ¬ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t
61 60 anbi2d ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → s ⊆ t ∧ ¬ k ⁡ s ⊆ k ⁡ t ↔ s ⊆ t ∧ ¬ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t
62 58 61 bitrid ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → ¬ s ⊆ t → k ⁡ s ⊆ k ⁡ t ↔ s ⊆ t ∧ ¬ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t
63 62 2rexbidv ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → ∃ s ∈ 𝒫 3 𝑜 ∃ t ∈ 𝒫 3 𝑜 ¬ s ⊆ t → k ⁡ s ⊆ k ⁡ t ↔ ∃ s ∈ 𝒫 3 𝑜 ∃ t ∈ 𝒫 3 𝑜 s ⊆ t ∧ ¬ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t
64 57 63 bitr3id ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → ¬ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 s ⊆ t → k ⁡ s ⊆ k ⁡ t ↔ ∃ s ∈ 𝒫 3 𝑜 ∃ t ∈ 𝒫 3 𝑜 s ⊆ t ∧ ¬ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t
65 56 64 anbi12d ⊢ k = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r → k ⁡ ∅ = ∅ ∧ ∀ s ∈ 𝒫 3 𝑜 s ⊆ k ⁡ s ∧ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t ∧ ∀ s ∈ 𝒫 3 𝑜 k ⁡ k ⁡ s = k ⁡ s ∧ ¬ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 s ⊆ t → k ⁡ s ⊆ k ⁡ t ↔ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ ∅ = ∅ ∧ ∀ s ∈ 𝒫 3 𝑜 s ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∧ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ t ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t ∧ ∀ s ∈ 𝒫 3 𝑜 r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∧ ∃ s ∈ 𝒫 3 𝑜 ∃ t ∈ 𝒫 3 𝑜 s ⊆ t ∧ ¬ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t
66 65 rspcev ⊢ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ∈ 𝒫 3 𝑜 𝒫 3 𝑜 ∧ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ ∅ = ∅ ∧ ∀ s ∈ 𝒫 3 𝑜 s ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∧ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ t ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∪ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t ∧ ∀ s ∈ 𝒫 3 𝑜 r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s = r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ∧ ∃ s ∈ 𝒫 3 𝑜 ∃ t ∈ 𝒫 3 𝑜 s ⊆ t ∧ ¬ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ s ⊆ r ∈ 𝒫 3 𝑜 ⟼ if r = ∅ ∅ 1 𝑜 r ⁡ t → ∃ k ∈ 𝒫 3 𝑜 𝒫 3 𝑜 k ⁡ ∅ = ∅ ∧ ∀ s ∈ 𝒫 3 𝑜 s ⊆ k ⁡ s ∧ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t ∧ ∀ s ∈ 𝒫 3 𝑜 k ⁡ k ⁡ s = k ⁡ s ∧ ¬ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 s ⊆ t → k ⁡ s ⊆ k ⁡ t
67 30 39 66 mp2an ⊢ ∃ k ∈ 𝒫 3 𝑜 𝒫 3 𝑜 k ⁡ ∅ = ∅ ∧ ∀ s ∈ 𝒫 3 𝑜 s ⊆ k ⁡ s ∧ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t ∧ ∀ s ∈ 𝒫 3 𝑜 k ⁡ k ⁡ s = k ⁡ s ∧ ¬ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 s ⊆ t → k ⁡ s ⊆ k ⁡ t
68 pweq ⊢ b = 3 𝑜 → 𝒫 b = 𝒫 3 𝑜
69 68 68 oveq12d ⊢ b = 3 𝑜 → 𝒫 b 𝒫 b = 𝒫 3 𝑜 𝒫 3 𝑜
70 pm4.61 ⊢ ¬ φ ∧ χ ∧ θ ∧ τ → ψ ↔ φ ∧ χ ∧ θ ∧ τ ∧ ¬ ψ
71 1 a1i ⊢ b = 3 𝑜 → φ ↔ k ⁡ ∅ = ∅
72 68 raleqdv ⊢ b = 3 𝑜 → ∀ s ∈ 𝒫 b s ⊆ k ⁡ s ↔ ∀ s ∈ 𝒫 3 𝑜 s ⊆ k ⁡ s
73 3 72 bitrid ⊢ b = 3 𝑜 → χ ↔ ∀ s ∈ 𝒫 3 𝑜 s ⊆ k ⁡ s
74 71 73 anbi12d ⊢ b = 3 𝑜 → φ ∧ χ ↔ k ⁡ ∅ = ∅ ∧ ∀ s ∈ 𝒫 3 𝑜 s ⊆ k ⁡ s
75 68 raleqdv ⊢ b = 3 𝑜 → ∀ t ∈ 𝒫 b k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t ↔ ∀ t ∈ 𝒫 3 𝑜 k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t
76 68 75 raleqbidv ⊢ b = 3 𝑜 → ∀ s ∈ 𝒫 b ∀ t ∈ 𝒫 b k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t ↔ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t
77 4 76 bitrid ⊢ b = 3 𝑜 → θ ↔ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t
78 68 raleqdv ⊢ b = 3 𝑜 → ∀ s ∈ 𝒫 b k ⁡ k ⁡ s = k ⁡ s ↔ ∀ s ∈ 𝒫 3 𝑜 k ⁡ k ⁡ s = k ⁡ s
79 5 78 bitrid ⊢ b = 3 𝑜 → τ ↔ ∀ s ∈ 𝒫 3 𝑜 k ⁡ k ⁡ s = k ⁡ s
80 77 79 anbi12d ⊢ b = 3 𝑜 → θ ∧ τ ↔ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t ∧ ∀ s ∈ 𝒫 3 𝑜 k ⁡ k ⁡ s = k ⁡ s
81 74 80 anbi12d ⊢ b = 3 𝑜 → φ ∧ χ ∧ θ ∧ τ ↔ k ⁡ ∅ = ∅ ∧ ∀ s ∈ 𝒫 3 𝑜 s ⊆ k ⁡ s ∧ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t ∧ ∀ s ∈ 𝒫 3 𝑜 k ⁡ k ⁡ s = k ⁡ s
82 68 raleqdv ⊢ b = 3 𝑜 → ∀ t ∈ 𝒫 b s ⊆ t → k ⁡ s ⊆ k ⁡ t ↔ ∀ t ∈ 𝒫 3 𝑜 s ⊆ t → k ⁡ s ⊆ k ⁡ t
83 68 82 raleqbidv ⊢ b = 3 𝑜 → ∀ s ∈ 𝒫 b ∀ t ∈ 𝒫 b s ⊆ t → k ⁡ s ⊆ k ⁡ t ↔ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 s ⊆ t → k ⁡ s ⊆ k ⁡ t
84 2 83 bitrid ⊢ b = 3 𝑜 → ψ ↔ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 s ⊆ t → k ⁡ s ⊆ k ⁡ t
85 84 notbid ⊢ b = 3 𝑜 → ¬ ψ ↔ ¬ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 s ⊆ t → k ⁡ s ⊆ k ⁡ t
86 81 85 anbi12d ⊢ b = 3 𝑜 → φ ∧ χ ∧ θ ∧ τ ∧ ¬ ψ ↔ k ⁡ ∅ = ∅ ∧ ∀ s ∈ 𝒫 3 𝑜 s ⊆ k ⁡ s ∧ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t ∧ ∀ s ∈ 𝒫 3 𝑜 k ⁡ k ⁡ s = k ⁡ s ∧ ¬ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 s ⊆ t → k ⁡ s ⊆ k ⁡ t
87 70 86 bitrid ⊢ b = 3 𝑜 → ¬ φ ∧ χ ∧ θ ∧ τ → ψ ↔ k ⁡ ∅ = ∅ ∧ ∀ s ∈ 𝒫 3 𝑜 s ⊆ k ⁡ s ∧ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t ∧ ∀ s ∈ 𝒫 3 𝑜 k ⁡ k ⁡ s = k ⁡ s ∧ ¬ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 s ⊆ t → k ⁡ s ⊆ k ⁡ t
88 69 87 rexeqbidv ⊢ b = 3 𝑜 → ∃ k ∈ 𝒫 b 𝒫 b ¬ φ ∧ χ ∧ θ ∧ τ → ψ ↔ ∃ k ∈ 𝒫 3 𝑜 𝒫 3 𝑜 k ⁡ ∅ = ∅ ∧ ∀ s ∈ 𝒫 3 𝑜 s ⊆ k ⁡ s ∧ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t ∧ ∀ s ∈ 𝒫 3 𝑜 k ⁡ k ⁡ s = k ⁡ s ∧ ¬ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 s ⊆ t → k ⁡ s ⊆ k ⁡ t
89 88 rspcev ⊢ 3 𝑜 ∈ V ∧ ∃ k ∈ 𝒫 3 𝑜 𝒫 3 𝑜 k ⁡ ∅ = ∅ ∧ ∀ s ∈ 𝒫 3 𝑜 s ⊆ k ⁡ s ∧ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t ∧ ∀ s ∈ 𝒫 3 𝑜 k ⁡ k ⁡ s = k ⁡ s ∧ ¬ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 s ⊆ t → k ⁡ s ⊆ k ⁡ t → ∃ b ∈ V ∃ k ∈ 𝒫 b 𝒫 b ¬ φ ∧ χ ∧ θ ∧ τ → ψ
90 rexnal2 ⊢ ∃ b ∈ V ∃ k ∈ 𝒫 b 𝒫 b ¬ φ ∧ χ ∧ θ ∧ τ → ψ ↔ ¬ ∀ b ∈ V ∀ k ∈ 𝒫 b 𝒫 b φ ∧ χ ∧ θ ∧ τ → ψ
91 ralv ⊢ ∀ b ∈ V ∀ k ∈ 𝒫 b 𝒫 b φ ∧ χ ∧ θ ∧ τ → ψ ↔ ∀ b ∀ k ∈ 𝒫 b 𝒫 b φ ∧ χ ∧ θ ∧ τ → ψ
92 90 91 xchbinx ⊢ ∃ b ∈ V ∃ k ∈ 𝒫 b 𝒫 b ¬ φ ∧ χ ∧ θ ∧ τ → ψ ↔ ¬ ∀ b ∀ k ∈ 𝒫 b 𝒫 b φ ∧ χ ∧ θ ∧ τ → ψ
93 89 92 sylib ⊢ 3 𝑜 ∈ V ∧ ∃ k ∈ 𝒫 3 𝑜 𝒫 3 𝑜 k ⁡ ∅ = ∅ ∧ ∀ s ∈ 𝒫 3 𝑜 s ⊆ k ⁡ s ∧ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 k ⁡ s ∪ t ⊆ k ⁡ s ∪ k ⁡ t ∧ ∀ s ∈ 𝒫 3 𝑜 k ⁡ k ⁡ s = k ⁡ s ∧ ¬ ∀ s ∈ 𝒫 3 𝑜 ∀ t ∈ 𝒫 3 𝑜 s ⊆ t → k ⁡ s ⊆ k ⁡ t → ¬ ∀ b ∀ k ∈ 𝒫 b 𝒫 b φ ∧ χ ∧ θ ∧ τ → ψ
94 7 67 93 mp2an ⊢ ¬ ∀ b ∀ k ∈ 𝒫 b 𝒫 b φ ∧ χ ∧ θ ∧ τ → ψ