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 43386
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 4567 . . . . . 6 (𝑥 ∈ if((𝑠𝑡) = {∅}, {∅, 1o}, (𝑠𝑡)) ↔ (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))))
2 uneq12 4154 . . . . . . . . . . 11 ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑠𝑡) = ({∅} ∪ {∅}))
3 unidm 4148 . . . . . . . . . . 11 ({∅} ∪ {∅}) = {∅}
42, 3eqtrdi 2783 . . . . . . . . . 10 ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑠𝑡) = {∅})
5 an3 658 . . . . . . . . . . . . . 14 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o})) → (𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}))
65orcd 872 . . . . . . . . . . . . 13 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o})) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)))
76orcd 872 . . . . . . . . . . . 12 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o})) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
87ex 412 . . . . . . . . . . 11 ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
9 pm2.24 124 . . . . . . . . . . . 12 ((𝑠𝑡) = {∅} → (¬ (𝑠𝑡) = {∅} → (𝑥 ∈ (𝑠𝑡) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
109impd 410 . . . . . . . . . . 11 ((𝑠𝑡) = {∅} → ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
118, 10jaao 953 . . . . . . . . . 10 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ (𝑠𝑡) = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
124, 11mpdan 686 . . . . . . . . 9 ((𝑠 = {∅} ∧ 𝑡 = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
1312a1i 11 . . . . . . . 8 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → ((𝑠 = {∅} ∧ 𝑡 = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
14 uneqsn 43368 . . . . . . . . . . . . 13 ((𝑠𝑡) = {∅} ↔ ((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})))
15 df-3or 1086 . . . . . . . . . . . . 13 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})) ↔ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})))
1614, 15bitri 275 . . . . . . . . . . . 12 ((𝑠𝑡) = {∅} ↔ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})))
17 pm2.21 123 . . . . . . . . . . . . . . . 16 𝑠 = {∅} → (𝑠 = {∅} → (𝑥 ∈ {∅, 1o} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
1817adantrd 491 . . . . . . . . . . . . . . 15 𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑥 ∈ {∅, 1o} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
1917adantrd 491 . . . . . . . . . . . . . . 15 𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑡 = ∅) → (𝑥 ∈ {∅, 1o} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2018, 19jaod 858 . . . . . . . . . . . . . 14 𝑠 = {∅} → (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) → (𝑥 ∈ {∅, 1o} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2120adantr 480 . . . . . . . . . . . . 13 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) → (𝑥 ∈ {∅, 1o} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
22 pm2.21 123 . . . . . . . . . . . . . . 15 𝑡 = {∅} → (𝑡 = {∅} → (𝑥 ∈ {∅, 1o} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2322adantl 481 . . . . . . . . . . . . . 14 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → (𝑡 = {∅} → (𝑥 ∈ {∅, 1o} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2423adantld 490 . . . . . . . . . . . . 13 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = ∅ ∧ 𝑡 = {∅}) → (𝑥 ∈ {∅, 1o} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2521, 24jaod 858 . . . . . . . . . . . 12 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})) → (𝑥 ∈ {∅, 1o} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2616, 25biimtrid 241 . . . . . . . . . . 11 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠𝑡) = {∅} → (𝑥 ∈ {∅, 1o} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2726impd 410 . . . . . . . . . 10 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
28 elun 4144 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑠𝑡) ↔ (𝑥𝑠𝑥𝑡))
2928biimpi 215 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑠𝑡) → (𝑥𝑠𝑥𝑡))
3029adantl 481 . . . . . . . . . . . . . 14 ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → (𝑥𝑠𝑥𝑡))
31 andi 1006 . . . . . . . . . . . . . . 15 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (𝑥𝑠𝑥𝑡)) ↔ (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑠) ∨ ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑡)))
32 simpl 482 . . . . . . . . . . . . . . . . 17 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ¬ 𝑠 = {∅})
3332anim1i 614 . . . . . . . . . . . . . . . 16 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑠) → (¬ 𝑠 = {∅} ∧ 𝑥𝑠))
34 simpr 484 . . . . . . . . . . . . . . . . 17 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ¬ 𝑡 = {∅})
3534anim1i 614 . . . . . . . . . . . . . . . 16 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑡) → (¬ 𝑡 = {∅} ∧ 𝑥𝑡))
3633, 35orim12i 907 . . . . . . . . . . . . . . 15 ((((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑠) ∨ ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑡)) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
3731, 36sylbi 216 . . . . . . . . . . . . . 14 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (𝑥𝑠𝑥𝑡)) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
3830, 37sylan2 592 . . . . . . . . . . . . 13 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
3938olcd 873 . . . . . . . . . . . 12 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o})) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
40 or4 925 . . . . . . . . . . . 12 ((((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o})) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))) ↔ (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
4139, 40sylib 217 . . . . . . . . . . 11 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
4241ex 412 . . . . . . . . . 10 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
4327, 42jaod 858 . . . . . . . . 9 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
4443a1i 11 . . . . . . . 8 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
4513, 44jaod 858 . . . . . . 7 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅})) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
46 orc 866 . . . . . . . . . . . . . . 15 ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
4746expcom 413 . . . . . . . . . . . . . 14 (𝑥 ∈ {∅, 1o} → (𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
4847adantrd 491 . . . . . . . . . . . . 13 (𝑥 ∈ {∅, 1o} → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
4948adantl 481 . . . . . . . . . . . 12 (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
50 simpr 484 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑠𝑠 = {∅}) → 𝑠 = {∅})
51 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = {∅} → 𝑠 = {∅})
52 snsspr1 4813 . . . . . . . . . . . . . . . . . . . . 21 {∅} ⊆ {∅, 1o}
5351, 52eqsstrdi 4032 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = {∅} → 𝑠 ⊆ {∅, 1o})
5453sseld 3977 . . . . . . . . . . . . . . . . . . 19 (𝑠 = {∅} → (𝑥𝑠𝑥 ∈ {∅, 1o}))
5554impcom 407 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑠𝑠 = {∅}) → 𝑥 ∈ {∅, 1o})
5650, 55jca 511 . . . . . . . . . . . . . . . . 17 ((𝑥𝑠𝑠 = {∅}) → (𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}))
5756orcd 872 . . . . . . . . . . . . . . . 16 ((𝑥𝑠𝑠 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
5857ex 412 . . . . . . . . . . . . . . 15 (𝑥𝑠 → (𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
59 olc 867 . . . . . . . . . . . . . . . 16 ((¬ 𝑡 = {∅} ∧ 𝑥𝑡) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
6059expcom 413 . . . . . . . . . . . . . . 15 (𝑥𝑡 → (¬ 𝑡 = {∅} → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
6158, 60jaoa 954 . . . . . . . . . . . . . 14 ((𝑥𝑠𝑥𝑡) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
6228, 61sylbi 216 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑠𝑡) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
6362adantl 481 . . . . . . . . . . . 12 ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
6449, 63jaoi 856 . . . . . . . . . . 11 ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
65 olc 867 . . . . . . . . . . . . . . 15 ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o})))
6665expcom 413 . . . . . . . . . . . . . 14 (𝑥 ∈ {∅, 1o} → (𝑡 = {∅} → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}))))
6766adantl 481 . . . . . . . . . . . . 13 (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) → (𝑡 = {∅} → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}))))
6867adantrd 491 . . . . . . . . . . . 12 (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}))))
69 id 22 . . . . . . . . . . . . . . . . . 18 ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) → (¬ 𝑠 = {∅} ∧ 𝑥𝑠))
7069ex 412 . . . . . . . . . . . . . . . . 17 𝑠 = {∅} → (𝑥𝑠 → (¬ 𝑠 = {∅} ∧ 𝑥𝑠)))
7170adantl 481 . . . . . . . . . . . . . . . 16 ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → (𝑥𝑠 → (¬ 𝑠 = {∅} ∧ 𝑥𝑠)))
72 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = {∅} → 𝑡 = {∅})
7372, 52eqsstrdi 4032 . . . . . . . . . . . . . . . . . . 19 (𝑡 = {∅} → 𝑡 ⊆ {∅, 1o})
7473sseld 3977 . . . . . . . . . . . . . . . . . 18 (𝑡 = {∅} → (𝑥𝑡𝑥 ∈ {∅, 1o}))
7574anc2li 555 . . . . . . . . . . . . . . . . 17 (𝑡 = {∅} → (𝑥𝑡 → (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o})))
7675adantr 480 . . . . . . . . . . . . . . . 16 ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → (𝑥𝑡 → (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o})))
7771, 76orim12d 963 . . . . . . . . . . . . . . 15 ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((𝑥𝑠𝑥𝑡) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}))))
7877com12 32 . . . . . . . . . . . . . 14 ((𝑥𝑠𝑥𝑡) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}))))
7928, 78sylbi 216 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑠𝑡) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}))))
8079adantl 481 . . . . . . . . . . . 12 ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}))))
8168, 80jaoi 856 . . . . . . . . . . 11 ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}))))
8264, 81orim12d 963 . . . . . . . . . 10 ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o})))))
8382com12 32 . . . . . . . . 9 (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o})))))
84 or42 926 . . . . . . . . 9 ((((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}))) ↔ (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
8583, 84imbitrdi 250 . . . . . . . 8 (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
8685a1i 11 . . . . . . 7 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
87 4exmid 1050 . . . . . . . 8 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅})) ∨ ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})))
8887a1i 11 . . . . . . 7 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅})) ∨ ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅}))))
8945, 86, 88mpjaod 859 . . . . . 6 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
901, 89biimtrid 241 . . . . 5 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → (𝑥 ∈ if((𝑠𝑡) = {∅}, {∅, 1o}, (𝑠𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
91 elun 4144 . . . . . 6 (𝑥 ∈ (if(𝑠 = {∅}, {∅, 1o}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1o}, 𝑡)) ↔ (𝑥 ∈ if(𝑠 = {∅}, {∅, 1o}, 𝑠) ∨ 𝑥 ∈ if(𝑡 = {∅}, {∅, 1o}, 𝑡)))
92 elif 4567 . . . . . . 7 (𝑥 ∈ if(𝑠 = {∅}, {∅, 1o}, 𝑠) ↔ ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)))
93 elif 4567 . . . . . . 7 (𝑥 ∈ if(𝑡 = {∅}, {∅, 1o}, 𝑡) ↔ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
9492, 93orbi12i 913 . . . . . 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 3984 . . 3 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → if((𝑠𝑡) = {∅}, {∅, 1o}, (𝑠𝑡)) ⊆ (if(𝑠 = {∅}, {∅, 1o}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1o}, 𝑡)))
98 pwuncl 7764 . . . 4 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → (𝑠𝑡) ∈ 𝒫 3o)
99 eqeq1 2731 . . . . . 6 (𝑟 = (𝑠𝑡) → (𝑟 = {∅} ↔ (𝑠𝑡) = {∅}))
100 id 22 . . . . . 6 (𝑟 = (𝑠𝑡) → 𝑟 = (𝑠𝑡))
10199, 100ifbieq2d 4550 . . . . 5 (𝑟 = (𝑠𝑡) → if(𝑟 = {∅}, {∅, 1o}, 𝑟) = if((𝑠𝑡) = {∅}, {∅, 1o}, (𝑠𝑡)))
102 clsk1indlem.k . . . . 5 𝐾 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))
103 prex 5428 . . . . . 6 {∅, 1o} ∈ V
104 vex 3473 . . . . . . 7 𝑠 ∈ V
105 vex 3473 . . . . . . 7 𝑡 ∈ V
106104, 105unex 7740 . . . . . 6 (𝑠𝑡) ∈ V
107103, 106ifex 4574 . . . . 5 if((𝑠𝑡) = {∅}, {∅, 1o}, (𝑠𝑡)) ∈ V
108101, 102, 107fvmpt 6999 . . . 4 ((𝑠𝑡) ∈ 𝒫 3o → (𝐾‘(𝑠𝑡)) = if((𝑠𝑡) = {∅}, {∅, 1o}, (𝑠𝑡)))
10998, 108syl 17 . . 3 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → (𝐾‘(𝑠𝑡)) = if((𝑠𝑡) = {∅}, {∅, 1o}, (𝑠𝑡)))
110 eqeq1 2731 . . . . . . 7 (𝑟 = 𝑠 → (𝑟 = {∅} ↔ 𝑠 = {∅}))
111 id 22 . . . . . . 7 (𝑟 = 𝑠𝑟 = 𝑠)
112110, 111ifbieq2d 4550 . . . . . 6 (𝑟 = 𝑠 → if(𝑟 = {∅}, {∅, 1o}, 𝑟) = if(𝑠 = {∅}, {∅, 1o}, 𝑠))
113103, 104ifex 4574 . . . . . 6 if(𝑠 = {∅}, {∅, 1o}, 𝑠) ∈ V
114112, 102, 113fvmpt 6999 . . . . 5 (𝑠 ∈ 𝒫 3o → (𝐾𝑠) = if(𝑠 = {∅}, {∅, 1o}, 𝑠))
115114adantr 480 . . . 4 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → (𝐾𝑠) = if(𝑠 = {∅}, {∅, 1o}, 𝑠))
116 eqeq1 2731 . . . . . . 7 (𝑟 = 𝑡 → (𝑟 = {∅} ↔ 𝑡 = {∅}))
117 id 22 . . . . . . 7 (𝑟 = 𝑡𝑟 = 𝑡)
118116, 117ifbieq2d 4550 . . . . . 6 (𝑟 = 𝑡 → if(𝑟 = {∅}, {∅, 1o}, 𝑟) = if(𝑡 = {∅}, {∅, 1o}, 𝑡))
119103, 105ifex 4574 . . . . . 6 if(𝑡 = {∅}, {∅, 1o}, 𝑡) ∈ V
120118, 102, 119fvmpt 6999 . . . . 5 (𝑡 ∈ 𝒫 3o → (𝐾𝑡) = if(𝑡 = {∅}, {∅, 1o}, 𝑡))
121120adantl 481 . . . 4 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → (𝐾𝑡) = if(𝑡 = {∅}, {∅, 1o}, 𝑡))
122115, 121uneq12d 4160 . . 3 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → ((𝐾𝑠) ∪ (𝐾𝑡)) = (if(𝑠 = {∅}, {∅, 1o}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1o}, 𝑡)))
12397, 109, 1223sstr4d 4025 . 2 ((𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o) → (𝐾‘(𝑠𝑡)) ⊆ ((𝐾𝑠) ∪ (𝐾𝑡)))
124123rgen2 3192 1 𝑠 ∈ 𝒫 3o𝑡 ∈ 𝒫 3o(𝐾‘(𝑠𝑡)) ⊆ ((𝐾𝑠) ∪ (𝐾𝑡))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 846  w3o 1084   = wceq 1534  wcel 2099  wral 3056  cun 3942  wss 3944  c0 4318  ifcif 4524  𝒫 cpw 4598  {csn 4624  {cpr 4626  cmpt 5225  cfv 6542  1oc1o 8471  3oc3o 8473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7732
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-xor 1506  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-iota 6494  df-fun 6544  df-fv 6550
This theorem is referenced by:  clsk1independent  43389
  Copyright terms: Public domain W3C validator