Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  clsk1indlem3 Structured version   Visualization version   GIF version

Theorem clsk1indlem3 41635
Description: The ansatz closure function (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) has the K3 property of being sub-linear. (Contributed by RP, 6-Jul-2021.)
Hypothesis
Ref Expression
clsk1indlem.k 𝐾 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))
Assertion
Ref Expression
clsk1indlem3 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝐾‘(𝑠𝑡)) ⊆ ((𝐾𝑠) ∪ (𝐾𝑡))
Distinct variable group:   𝑠,𝑟,𝑡
Allowed substitution hints:   𝐾(𝑡,𝑠,𝑟)

Proof of Theorem clsk1indlem3
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elif 4508 . . . . . 6 (𝑥 ∈ if((𝑠𝑡) = {∅}, {∅, 1o}, (𝑠𝑡)) ↔ (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))))
2 uneq12 4097 . . . . . . . . . . 11 ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑠𝑡) = ({∅} ∪ {∅}))
3 unidm 4091 . . . . . . . . . . 11 ({∅} ∪ {∅}) = {∅}
42, 3eqtrdi 2796 . . . . . . . . . 10 ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑠𝑡) = {∅})
5 an3 656 . . . . . . . . . . . . . 14 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o})) → (𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}))
65orcd 870 . . . . . . . . . . . . 13 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o})) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)))
76orcd 870 . . . . . . . . . . . 12 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o})) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
87ex 413 . . . . . . . . . . 11 ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
9 pm2.24 124 . . . . . . . . . . . 12 ((𝑠𝑡) = {∅} → (¬ (𝑠𝑡) = {∅} → (𝑥 ∈ (𝑠𝑡) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
109impd 411 . . . . . . . . . . 11 ((𝑠𝑡) = {∅} → ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
118, 10jaao 952 . . . . . . . . . 10 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ (𝑠𝑡) = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
124, 11mpdan 684 . . . . . . . . 9 ((𝑠 = {∅} ∧ 𝑡 = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
1312a1i 11 . . . . . . . 8 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → ((𝑠 = {∅} ∧ 𝑡 = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
14 uneqsn 41615 . . . . . . . . . . . . 13 ((𝑠𝑡) = {∅} ↔ ((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})))
15 df-3or 1087 . . . . . . . . . . . . 13 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})) ↔ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})))
1614, 15bitri 274 . . . . . . . . . . . 12 ((𝑠𝑡) = {∅} ↔ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})))
17 pm2.21 123 . . . . . . . . . . . . . . . 16 𝑠 = {∅} → (𝑠 = {∅} → (𝑥 ∈ {∅, 1o} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
1817adantrd 492 . . . . . . . . . . . . . . 15 𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑥 ∈ {∅, 1o} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
1917adantrd 492 . . . . . . . . . . . . . . 15 𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑡 = ∅) → (𝑥 ∈ {∅, 1o} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2018, 19jaod 856 . . . . . . . . . . . . . 14 𝑠 = {∅} → (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) → (𝑥 ∈ {∅, 1o} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2120adantr 481 . . . . . . . . . . . . 13 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) → (𝑥 ∈ {∅, 1o} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
22 pm2.21 123 . . . . . . . . . . . . . . 15 𝑡 = {∅} → (𝑡 = {∅} → (𝑥 ∈ {∅, 1o} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2322adantl 482 . . . . . . . . . . . . . 14 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → (𝑡 = {∅} → (𝑥 ∈ {∅, 1o} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2423adantld 491 . . . . . . . . . . . . 13 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = ∅ ∧ 𝑡 = {∅}) → (𝑥 ∈ {∅, 1o} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2521, 24jaod 856 . . . . . . . . . . . 12 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})) → (𝑥 ∈ {∅, 1o} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2616, 25syl5bi 241 . . . . . . . . . . 11 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠𝑡) = {∅} → (𝑥 ∈ {∅, 1o} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2726impd 411 . . . . . . . . . 10 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
28 elun 4088 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑠𝑡) ↔ (𝑥𝑠𝑥𝑡))
2928biimpi 215 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑠𝑡) → (𝑥𝑠𝑥𝑡))
3029adantl 482 . . . . . . . . . . . . . 14 ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → (𝑥𝑠𝑥𝑡))
31 andi 1005 . . . . . . . . . . . . . . 15 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (𝑥𝑠𝑥𝑡)) ↔ (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑠) ∨ ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑡)))
32 simpl 483 . . . . . . . . . . . . . . . . 17 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ¬ 𝑠 = {∅})
3332anim1i 615 . . . . . . . . . . . . . . . 16 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑠) → (¬ 𝑠 = {∅} ∧ 𝑥𝑠))
34 simpr 485 . . . . . . . . . . . . . . . . 17 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ¬ 𝑡 = {∅})
3534anim1i 615 . . . . . . . . . . . . . . . 16 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑡) → (¬ 𝑡 = {∅} ∧ 𝑥𝑡))
3633, 35orim12i 906 . . . . . . . . . . . . . . 15 ((((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑠) ∨ ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑡)) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
3731, 36sylbi 216 . . . . . . . . . . . . . 14 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (𝑥𝑠𝑥𝑡)) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
3830, 37sylan2 593 . . . . . . . . . . . . 13 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
3938olcd 871 . . . . . . . . . . . 12 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o})) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
40 or4 924 . . . . . . . . . . . 12 ((((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o})) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))) ↔ (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
4139, 40sylib 217 . . . . . . . . . . 11 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
4241ex 413 . . . . . . . . . 10 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
4327, 42jaod 856 . . . . . . . . 9 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
4443a1i 11 . . . . . . . 8 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
4513, 44jaod 856 . . . . . . 7 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅})) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
46 orc 864 . . . . . . . . . . . . . . 15 ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
4746expcom 414 . . . . . . . . . . . . . 14 (𝑥 ∈ {∅, 1o} → (𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
4847adantrd 492 . . . . . . . . . . . . 13 (𝑥 ∈ {∅, 1o} → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
4948adantl 482 . . . . . . . . . . . 12 (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
50 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑠𝑠 = {∅}) → 𝑠 = {∅})
51 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = {∅} → 𝑠 = {∅})
52 snsspr1 4753 . . . . . . . . . . . . . . . . . . . . 21 {∅} ⊆ {∅, 1o}
5351, 52eqsstrdi 3980 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = {∅} → 𝑠 ⊆ {∅, 1o})
5453sseld 3925 . . . . . . . . . . . . . . . . . . 19 (𝑠 = {∅} → (𝑥𝑠𝑥 ∈ {∅, 1o}))
5554impcom 408 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑠𝑠 = {∅}) → 𝑥 ∈ {∅, 1o})
5650, 55jca 512 . . . . . . . . . . . . . . . . 17 ((𝑥𝑠𝑠 = {∅}) → (𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}))
5756orcd 870 . . . . . . . . . . . . . . . 16 ((𝑥𝑠𝑠 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
5857ex 413 . . . . . . . . . . . . . . 15 (𝑥𝑠 → (𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
59 olc 865 . . . . . . . . . . . . . . . 16 ((¬ 𝑡 = {∅} ∧ 𝑥𝑡) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
6059expcom 414 . . . . . . . . . . . . . . 15 (𝑥𝑡 → (¬ 𝑡 = {∅} → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
6158, 60jaoa 953 . . . . . . . . . . . . . 14 ((𝑥𝑠𝑥𝑡) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
6228, 61sylbi 216 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑠𝑡) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
6362adantl 482 . . . . . . . . . . . 12 ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
6449, 63jaoi 854 . . . . . . . . . . 11 ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
65 olc 865 . . . . . . . . . . . . . . 15 ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o})))
6665expcom 414 . . . . . . . . . . . . . 14 (𝑥 ∈ {∅, 1o} → (𝑡 = {∅} → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}))))
6766adantl 482 . . . . . . . . . . . . 13 (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) → (𝑡 = {∅} → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}))))
6867adantrd 492 . . . . . . . . . . . 12 (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}))))
69 id 22 . . . . . . . . . . . . . . . . . 18 ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) → (¬ 𝑠 = {∅} ∧ 𝑥𝑠))
7069ex 413 . . . . . . . . . . . . . . . . 17 𝑠 = {∅} → (𝑥𝑠 → (¬ 𝑠 = {∅} ∧ 𝑥𝑠)))
7170adantl 482 . . . . . . . . . . . . . . . 16 ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → (𝑥𝑠 → (¬ 𝑠 = {∅} ∧ 𝑥𝑠)))
72 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = {∅} → 𝑡 = {∅})
7372, 52eqsstrdi 3980 . . . . . . . . . . . . . . . . . . 19 (𝑡 = {∅} → 𝑡 ⊆ {∅, 1o})
7473sseld 3925 . . . . . . . . . . . . . . . . . 18 (𝑡 = {∅} → (𝑥𝑡𝑥 ∈ {∅, 1o}))
7574anc2li 556 . . . . . . . . . . . . . . . . 17 (𝑡 = {∅} → (𝑥𝑡 → (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o})))
7675adantr 481 . . . . . . . . . . . . . . . 16 ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → (𝑥𝑡 → (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o})))
7771, 76orim12d 962 . . . . . . . . . . . . . . 15 ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((𝑥𝑠𝑥𝑡) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}))))
7877com12 32 . . . . . . . . . . . . . 14 ((𝑥𝑠𝑥𝑡) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}))))
7928, 78sylbi 216 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑠𝑡) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}))))
8079adantl 482 . . . . . . . . . . . 12 ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}))))
8168, 80jaoi 854 . . . . . . . . . . 11 ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}))))
8264, 81orim12d 962 . . . . . . . . . 10 ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o})))))
8382com12 32 . . . . . . . . 9 (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o})))))
84 or42 925 . . . . . . . . 9 ((((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}))) ↔ (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
8583, 84syl6ib 250 . . . . . . . 8 (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
8685a1i 11 . . . . . . 7 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
87 4exmid 1049 . . . . . . . 8 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅})) ∨ ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})))
8887a1i 11 . . . . . . 7 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅})) ∨ ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅}))))
8945, 86, 88mpjaod 857 . . . . . 6 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
901, 89syl5bi 241 . . . . 5 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → (𝑥 ∈ if((𝑠𝑡) = {∅}, {∅, 1o}, (𝑠𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
91 elun 4088 . . . . . 6 (𝑥 ∈ (if(𝑠 = {∅}, {∅, 1o}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1o}, 𝑡)) ↔ (𝑥 ∈ if(𝑠 = {∅}, {∅, 1o}, 𝑠) ∨ 𝑥 ∈ if(𝑡 = {∅}, {∅, 1o}, 𝑡)))
92 elif 4508 . . . . . . 7 (𝑥 ∈ if(𝑠 = {∅}, {∅, 1o}, 𝑠) ↔ ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)))
93 elif 4508 . . . . . . 7 (𝑥 ∈ if(𝑡 = {∅}, {∅, 1o}, 𝑡) ↔ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
9492, 93orbi12i 912 . . . . . 6 ((𝑥 ∈ if(𝑠 = {∅}, {∅, 1o}, 𝑠) ∨ 𝑥 ∈ if(𝑡 = {∅}, {∅, 1o}, 𝑡)) ↔ (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
9591, 94sylbbr 235 . . . . 5 ((((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))) → 𝑥 ∈ (if(𝑠 = {∅}, {∅, 1o}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1o}, 𝑡)))
9690, 95syl6 35 . . . 4 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → (𝑥 ∈ if((𝑠𝑡) = {∅}, {∅, 1o}, (𝑠𝑡)) → 𝑥 ∈ (if(𝑠 = {∅}, {∅, 1o}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1o}, 𝑡))))
9796ssrdv 3932 . . 3 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → if((𝑠𝑡) = {∅}, {∅, 1o}, (𝑠𝑡)) ⊆ (if(𝑠 = {∅}, {∅, 1o}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1o}, 𝑡)))
98 pwuncl 7615 . . . 4 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → (𝑠𝑡) ∈ 𝒫 3o)
99 eqeq1 2744 . . . . . 6 (𝑟 = (𝑠𝑡) → (𝑟 = {∅} ↔ (𝑠𝑡) = {∅}))
100 id 22 . . . . . 6 (𝑟 = (𝑠𝑡) → 𝑟 = (𝑠𝑡))
10199, 100ifbieq2d 4491 . . . . 5 (𝑟 = (𝑠𝑡) → if(𝑟 = {∅}, {∅, 1o}, 𝑟) = if((𝑠𝑡) = {∅}, {∅, 1o}, (𝑠𝑡)))
102 clsk1indlem.k . . . . 5 𝐾 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))
103 prex 5359 . . . . . 6 {∅, 1o} ∈ V
104 vex 3435 . . . . . . 7 𝑠 ∈ V
105 vex 3435 . . . . . . 7 𝑡 ∈ V
106104, 105unex 7591 . . . . . 6 (𝑠𝑡) ∈ V
107103, 106ifex 4515 . . . . 5 if((𝑠𝑡) = {∅}, {∅, 1o}, (𝑠𝑡)) ∈ V
108101, 102, 107fvmpt 6872 . . . 4 ((𝑠𝑡) ∈ 𝒫 3o → (𝐾‘(𝑠𝑡)) = if((𝑠𝑡) = {∅}, {∅, 1o}, (𝑠𝑡)))
10998, 108syl 17 . . 3 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → (𝐾‘(𝑠𝑡)) = if((𝑠𝑡) = {∅}, {∅, 1o}, (𝑠𝑡)))
110 eqeq1 2744 . . . . . . 7 (𝑟 = 𝑠 → (𝑟 = {∅} ↔ 𝑠 = {∅}))
111 id 22 . . . . . . 7 (𝑟 = 𝑠𝑟 = 𝑠)
112110, 111ifbieq2d 4491 . . . . . 6 (𝑟 = 𝑠 → if(𝑟 = {∅}, {∅, 1o}, 𝑟) = if(𝑠 = {∅}, {∅, 1o}, 𝑠))
113103, 104ifex 4515 . . . . . 6 if(𝑠 = {∅}, {∅, 1o}, 𝑠) ∈ V
114112, 102, 113fvmpt 6872 . . . . 5 (𝑠 ∈ 𝒫 3o → (𝐾𝑠) = if(𝑠 = {∅}, {∅, 1o}, 𝑠))
115114adantr 481 . . . 4 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → (𝐾𝑠) = if(𝑠 = {∅}, {∅, 1o}, 𝑠))
116 eqeq1 2744 . . . . . . 7 (𝑟 = 𝑡 → (𝑟 = {∅} ↔ 𝑡 = {∅}))
117 id 22 . . . . . . 7 (𝑟 = 𝑡𝑟 = 𝑡)
118116, 117ifbieq2d 4491 . . . . . 6 (𝑟 = 𝑡 → if(𝑟 = {∅}, {∅, 1o}, 𝑟) = if(𝑡 = {∅}, {∅, 1o}, 𝑡))
119103, 105ifex 4515 . . . . . 6 if(𝑡 = {∅}, {∅, 1o}, 𝑡) ∈ V
120118, 102, 119fvmpt 6872 . . . . 5 (𝑡 ∈ 𝒫 3o → (𝐾𝑡) = if(𝑡 = {∅}, {∅, 1o}, 𝑡))
121120adantl 482 . . . 4 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → (𝐾𝑡) = if(𝑡 = {∅}, {∅, 1o}, 𝑡))
122115, 121uneq12d 4103 . . 3 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → ((𝐾𝑠) ∪ (𝐾𝑡)) = (if(𝑠 = {∅}, {∅, 1o}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1o}, 𝑡)))
12397, 109, 1223sstr4d 3973 . 2 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → (𝐾‘(𝑠𝑡)) ⊆ ((𝐾𝑠) ∪ (𝐾𝑡)))
124123rgen2 3129 1 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝐾‘(𝑠𝑡)) ⊆ ((𝐾𝑠) ∪ (𝐾𝑡))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 844  w3o 1085   = wceq 1542  wcel 2110  wral 3066  cun 3890  wss 3892  c0 4262  ifcif 4465  𝒫 cpw 4539  {csn 4567  {cpr 4569  cmpt 5162  cfv 6432  1oc1o 8282  3oc3o 8284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356  ax-un 7583
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-xor 1507  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-iota 6390  df-fun 6434  df-fv 6440
This theorem is referenced by:  clsk1independent  41638
  Copyright terms: Public domain W3C validator