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 } , 𝑟 ) ) ∈ ( 𝒫 3om 𝒫 3o ) ↔ ( 𝑟 ∈ 𝒫 3o ↦ if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) ) : 𝒫 3o ⟶ 𝒫 3o )
30 27 29 mpbir ( 𝑟 ∈ 𝒫 3o ↦ if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) ) ∈ ( 𝒫 3om 𝒫 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 syl5bb ( 𝑘 = ( 𝑟 ∈ 𝒫 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 } , 𝑟 ) ) ∈ ( 𝒫 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 ( 𝑠𝑡 → ( 𝑘𝑠 ) ⊆ ( 𝑘𝑡 ) ) ) )
67 30 39 66 mp2an 𝑘 ∈ ( 𝒫 3om 𝒫 3o ) ( ( ( ( 𝑘 ‘ ∅ ) = ∅ ∧ ∀ 𝑠 ∈ 𝒫 3o 𝑠 ⊆ ( 𝑘𝑠 ) ) ∧ ( ∀ 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o ( 𝑘 ‘ ( 𝑠𝑡 ) ) ⊆ ( ( 𝑘𝑠 ) ∪ ( 𝑘𝑡 ) ) ∧ ∀ 𝑠 ∈ 𝒫 3o ( 𝑘 ‘ ( 𝑘𝑠 ) ) = ( 𝑘𝑠 ) ) ) ∧ ¬ ∀ 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o ( 𝑠𝑡 → ( 𝑘𝑠 ) ⊆ ( 𝑘𝑡 ) ) )
68 pweq ( 𝑏 = 3o → 𝒫 𝑏 = 𝒫 3o )
69 68 68 oveq12d ( 𝑏 = 3o → ( 𝒫 𝑏m 𝒫 𝑏 ) = ( 𝒫 3om 𝒫 3o ) )
70 pm4.61 ( ¬ ( ( ( 𝜑𝜒 ) ∧ ( 𝜃𝜏 ) ) → 𝜓 ) ↔ ( ( ( 𝜑𝜒 ) ∧ ( 𝜃𝜏 ) ) ∧ ¬ 𝜓 ) )
71 1 a1i ( 𝑏 = 3o → ( 𝜑 ↔ ( 𝑘 ‘ ∅ ) = ∅ ) )
72 68 raleqdv ( 𝑏 = 3o → ( ∀ 𝑠 ∈ 𝒫 𝑏 𝑠 ⊆ ( 𝑘𝑠 ) ↔ ∀ 𝑠 ∈ 𝒫 3o 𝑠 ⊆ ( 𝑘𝑠 ) ) )
73 3 72 syl5bb ( 𝑏 = 3o → ( 𝜒 ↔ ∀ 𝑠 ∈ 𝒫 3o 𝑠 ⊆ ( 𝑘𝑠 ) ) )
74 71 73 anbi12d ( 𝑏 = 3o → ( ( 𝜑𝜒 ) ↔ ( ( 𝑘 ‘ ∅ ) = ∅ ∧ ∀ 𝑠 ∈ 𝒫 3o 𝑠 ⊆ ( 𝑘𝑠 ) ) ) )
75 68 raleqdv ( 𝑏 = 3o → ( ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠𝑡 ) ) ⊆ ( ( 𝑘𝑠 ) ∪ ( 𝑘𝑡 ) ) ↔ ∀ 𝑡 ∈ 𝒫 3o ( 𝑘 ‘ ( 𝑠𝑡 ) ) ⊆ ( ( 𝑘𝑠 ) ∪ ( 𝑘𝑡 ) ) ) )
76 68 75 raleqbidv ( 𝑏 = 3o → ( ∀ 𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠𝑡 ) ) ⊆ ( ( 𝑘𝑠 ) ∪ ( 𝑘𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o ( 𝑘 ‘ ( 𝑠𝑡 ) ) ⊆ ( ( 𝑘𝑠 ) ∪ ( 𝑘𝑡 ) ) ) )
77 4 76 syl5bb ( 𝑏 = 3o → ( 𝜃 ↔ ∀ 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o ( 𝑘 ‘ ( 𝑠𝑡 ) ) ⊆ ( ( 𝑘𝑠 ) ∪ ( 𝑘𝑡 ) ) ) )
78 68 raleqdv ( 𝑏 = 3o → ( ∀ 𝑠 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑘𝑠 ) ) = ( 𝑘𝑠 ) ↔ ∀ 𝑠 ∈ 𝒫 3o ( 𝑘 ‘ ( 𝑘𝑠 ) ) = ( 𝑘𝑠 ) ) )
79 5 78 syl5bb ( 𝑏 = 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 syl5bb ( 𝑏 = 3o → ( 𝜓 ↔ ∀ 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o ( 𝑠𝑡 → ( 𝑘𝑠 ) ⊆ ( 𝑘𝑡 ) ) ) )
85 84 notbid ( 𝑏 = 3o → ( ¬ 𝜓 ↔ ¬ ∀ 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o ( 𝑠𝑡 → ( 𝑘𝑠 ) ⊆ ( 𝑘𝑡 ) ) ) )
86 81 85 anbi12d ( 𝑏 = 3o → ( ( ( ( 𝜑𝜒 ) ∧ ( 𝜃𝜏 ) ) ∧ ¬ 𝜓 ) ↔ ( ( ( ( 𝑘 ‘ ∅ ) = ∅ ∧ ∀ 𝑠 ∈ 𝒫 3o 𝑠 ⊆ ( 𝑘𝑠 ) ) ∧ ( ∀ 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o ( 𝑘 ‘ ( 𝑠𝑡 ) ) ⊆ ( ( 𝑘𝑠 ) ∪ ( 𝑘𝑡 ) ) ∧ ∀ 𝑠 ∈ 𝒫 3o ( 𝑘 ‘ ( 𝑘𝑠 ) ) = ( 𝑘𝑠 ) ) ) ∧ ¬ ∀ 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o ( 𝑠𝑡 → ( 𝑘𝑠 ) ⊆ ( 𝑘𝑡 ) ) ) ) )
87 70 86 syl5bb ( 𝑏 = 3o → ( ¬ ( ( ( 𝜑𝜒 ) ∧ ( 𝜃𝜏 ) ) → 𝜓 ) ↔ ( ( ( ( 𝑘 ‘ ∅ ) = ∅ ∧ ∀ 𝑠 ∈ 𝒫 3o 𝑠 ⊆ ( 𝑘𝑠 ) ) ∧ ( ∀ 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o ( 𝑘 ‘ ( 𝑠𝑡 ) ) ⊆ ( ( 𝑘𝑠 ) ∪ ( 𝑘𝑡 ) ) ∧ ∀ 𝑠 ∈ 𝒫 3o ( 𝑘 ‘ ( 𝑘𝑠 ) ) = ( 𝑘𝑠 ) ) ) ∧ ¬ ∀ 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o ( 𝑠𝑡 → ( 𝑘𝑠 ) ⊆ ( 𝑘𝑡 ) ) ) ) )
88 69 87 rexeqbidv ( 𝑏 = 3o → ( ∃ 𝑘 ∈ ( 𝒫 𝑏m 𝒫 𝑏 ) ¬ ( ( ( 𝜑𝜒 ) ∧ ( 𝜃𝜏 ) ) → 𝜓 ) ↔ ∃ 𝑘 ∈ ( 𝒫 3om 𝒫 3o ) ( ( ( ( 𝑘 ‘ ∅ ) = ∅ ∧ ∀ 𝑠 ∈ 𝒫 3o 𝑠 ⊆ ( 𝑘𝑠 ) ) ∧ ( ∀ 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o ( 𝑘 ‘ ( 𝑠𝑡 ) ) ⊆ ( ( 𝑘𝑠 ) ∪ ( 𝑘𝑡 ) ) ∧ ∀ 𝑠 ∈ 𝒫 3o ( 𝑘 ‘ ( 𝑘𝑠 ) ) = ( 𝑘𝑠 ) ) ) ∧ ¬ ∀ 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o ( 𝑠𝑡 → ( 𝑘𝑠 ) ⊆ ( 𝑘𝑡 ) ) ) ) )
89 88 rspcev ( ( 3o ∈ V ∧ ∃ 𝑘 ∈ ( 𝒫 3om 𝒫 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 ∧ ∃ 𝑘 ∈ ( 𝒫 3om 𝒫 3o ) ( ( ( ( 𝑘 ‘ ∅ ) = ∅ ∧ ∀ 𝑠 ∈ 𝒫 3o 𝑠 ⊆ ( 𝑘𝑠 ) ) ∧ ( ∀ 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o ( 𝑘 ‘ ( 𝑠𝑡 ) ) ⊆ ( ( 𝑘𝑠 ) ∪ ( 𝑘𝑡 ) ) ∧ ∀ 𝑠 ∈ 𝒫 3o ( 𝑘 ‘ ( 𝑘𝑠 ) ) = ( 𝑘𝑠 ) ) ) ∧ ¬ ∀ 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o ( 𝑠𝑡 → ( 𝑘𝑠 ) ⊆ ( 𝑘𝑡 ) ) ) ) → ¬ ∀ 𝑏𝑘 ∈ ( 𝒫 𝑏m 𝒫 𝑏 ) ( ( ( 𝜑𝜒 ) ∧ ( 𝜃𝜏 ) ) → 𝜓 ) )
94 7 67 93 mp2an ¬ ∀ 𝑏𝑘 ∈ ( 𝒫 𝑏m 𝒫 𝑏 ) ( ( ( 𝜑𝜒 ) ∧ ( 𝜃𝜏 ) ) → 𝜓 )