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 ⊢ ( 𝜑 ↔ ( 𝑘 ‘ ∅ ) = ∅ )
clsnim.k1 ⊢ ( 𝜓 ↔ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑠 ⊆ 𝑡 → ( 𝑘 ‘ 𝑠 ) ⊆ ( 𝑘 ‘ 𝑡 ) ) )
clsnim.k2 ⊢ ( 𝜒 ↔ ∀ 𝑠 ∈ 𝒫 𝑏 𝑠 ⊆ ( 𝑘 ‘ 𝑠 ) )
clsnim.k3 ⊢ ( 𝜃 ↔ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) )
clsnim.k4 ⊢ ( 𝜏 ↔ ∀ 𝑠 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑘 ‘ 𝑠 ) ) = ( 𝑘 ‘ 𝑠 ) )
Assertion clsk1independent ¬ ∀ 𝑏 ∀ 𝑘 ∈ ( 𝒫 𝑏 ↑m 𝒫 𝑏 ) ( ( ( 𝜑 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜏 ) ) → 𝜓 )

Proof

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