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

Proof of Theorem clsk1indlem3
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elif 4077 . . . . . 6 (𝑥 ∈ if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)) ↔ (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))))
2 uneq12 3723 . . . . . . . . . . 11 ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑠𝑡) = ({∅} ∪ {∅}))
3 unidm 3717 . . . . . . . . . . 11 ({∅} ∪ {∅}) = {∅}
42, 3syl6eq 2659 . . . . . . . . . 10 ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑠𝑡) = {∅})
5 an3 863 . . . . . . . . . . . . . 14 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})) → (𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))
65orcd 405 . . . . . . . . . . . . 13 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)))
76orcd 405 . . . . . . . . . . . 12 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
87ex 448 . . . . . . . . . . 11 ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
9 pm2.24 119 . . . . . . . . . . . 12 ((𝑠𝑡) = {∅} → (¬ (𝑠𝑡) = {∅} → (𝑥 ∈ (𝑠𝑡) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
109impd 445 . . . . . . . . . . 11 ((𝑠𝑡) = {∅} → ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
118, 10jaao 529 . . . . . . . . . 10 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ (𝑠𝑡) = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
124, 11mpdan 698 . . . . . . . . 9 ((𝑠 = {∅} ∧ 𝑡 = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
1312a1i 11 . . . . . . . 8 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → ((𝑠 = {∅} ∧ 𝑡 = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
14 uneqsn 37137 . . . . . . . . . . . . 13 ((𝑠𝑡) = {∅} ↔ ((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})))
15 df-3or 1031 . . . . . . . . . . . . 13 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})) ↔ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})))
1614, 15bitri 262 . . . . . . . . . . . 12 ((𝑠𝑡) = {∅} ↔ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})))
17 pm2.21 118 . . . . . . . . . . . . . . . 16 𝑠 = {∅} → (𝑠 = {∅} → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
1817adantrd 482 . . . . . . . . . . . . . . 15 𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
1917adantrd 482 . . . . . . . . . . . . . . 15 𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑡 = ∅) → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2018, 19jaod 393 . . . . . . . . . . . . . 14 𝑠 = {∅} → (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2120adantr 479 . . . . . . . . . . . . 13 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
22 pm2.21 118 . . . . . . . . . . . . . . 15 𝑡 = {∅} → (𝑡 = {∅} → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2322adantl 480 . . . . . . . . . . . . . 14 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → (𝑡 = {∅} → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2423adantld 481 . . . . . . . . . . . . 13 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = ∅ ∧ 𝑡 = {∅}) → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2521, 24jaod 393 . . . . . . . . . . . 12 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})) → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2616, 25syl5bi 230 . . . . . . . . . . 11 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠𝑡) = {∅} → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2726impd 445 . . . . . . . . . 10 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
28 elun 3714 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑠𝑡) ↔ (𝑥𝑠𝑥𝑡))
2928biimpi 204 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑠𝑡) → (𝑥𝑠𝑥𝑡))
3029adantl 480 . . . . . . . . . . . . . 14 ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → (𝑥𝑠𝑥𝑡))
31 andi 906 . . . . . . . . . . . . . . 15 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (𝑥𝑠𝑥𝑡)) ↔ (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑠) ∨ ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑡)))
32 simpl 471 . . . . . . . . . . . . . . . . 17 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ¬ 𝑠 = {∅})
3332anim1i 589 . . . . . . . . . . . . . . . 16 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑠) → (¬ 𝑠 = {∅} ∧ 𝑥𝑠))
34 simpr 475 . . . . . . . . . . . . . . . . 17 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ¬ 𝑡 = {∅})
3534anim1i 589 . . . . . . . . . . . . . . . 16 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑡) → (¬ 𝑡 = {∅} ∧ 𝑥𝑡))
3633, 35orim12i 536 . . . . . . . . . . . . . . 15 ((((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑠) ∨ ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑡)) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
3731, 36sylbi 205 . . . . . . . . . . . . . 14 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (𝑥𝑠𝑥𝑡)) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
3830, 37sylan2 489 . . . . . . . . . . . . 13 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
3938olcd 406 . . . . . . . . . . . 12 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
40 or4 548 . . . . . . . . . . . 12 ((((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))) ↔ (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
4139, 40sylib 206 . . . . . . . . . . 11 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
4241ex 448 . . . . . . . . . 10 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
4327, 42jaod 393 . . . . . . . . 9 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
4443a1i 11 . . . . . . . 8 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
4513, 44jaod 393 . . . . . . 7 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅})) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
46 orc 398 . . . . . . . . . . . . . . 15 ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
4746expcom 449 . . . . . . . . . . . . . 14 (𝑥 ∈ {∅, 1𝑜} → (𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
4847adantrd 482 . . . . . . . . . . . . 13 (𝑥 ∈ {∅, 1𝑜} → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
4948adantl 480 . . . . . . . . . . . 12 (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
50 simpr 475 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑠𝑠 = {∅}) → 𝑠 = {∅})
51 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = {∅} → 𝑠 = {∅})
52 snsspr1 4284 . . . . . . . . . . . . . . . . . . . . 21 {∅} ⊆ {∅, 1𝑜}
5351, 52syl6eqss 3617 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = {∅} → 𝑠 ⊆ {∅, 1𝑜})
5453sseld 3566 . . . . . . . . . . . . . . . . . . 19 (𝑠 = {∅} → (𝑥𝑠𝑥 ∈ {∅, 1𝑜}))
5554impcom 444 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑠𝑠 = {∅}) → 𝑥 ∈ {∅, 1𝑜})
5650, 55jca 552 . . . . . . . . . . . . . . . . 17 ((𝑥𝑠𝑠 = {∅}) → (𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))
5756orcd 405 . . . . . . . . . . . . . . . 16 ((𝑥𝑠𝑠 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
5857ex 448 . . . . . . . . . . . . . . 15 (𝑥𝑠 → (𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
59 olc 397 . . . . . . . . . . . . . . . 16 ((¬ 𝑡 = {∅} ∧ 𝑥𝑡) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
6059expcom 449 . . . . . . . . . . . . . . 15 (𝑥𝑡 → (¬ 𝑡 = {∅} → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
6158, 60jaoa 530 . . . . . . . . . . . . . 14 ((𝑥𝑠𝑥𝑡) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
6228, 61sylbi 205 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑠𝑡) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
6362adantl 480 . . . . . . . . . . . 12 ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
6449, 63jaoi 392 . . . . . . . . . . 11 ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
65 olc 397 . . . . . . . . . . . . . . 15 ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})))
6665expcom 449 . . . . . . . . . . . . . 14 (𝑥 ∈ {∅, 1𝑜} → (𝑡 = {∅} → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
6766adantl 480 . . . . . . . . . . . . 13 (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → (𝑡 = {∅} → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
6867adantrd 482 . . . . . . . . . . . 12 (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
69 id 22 . . . . . . . . . . . . . . . . . 18 ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) → (¬ 𝑠 = {∅} ∧ 𝑥𝑠))
7069ex 448 . . . . . . . . . . . . . . . . 17 𝑠 = {∅} → (𝑥𝑠 → (¬ 𝑠 = {∅} ∧ 𝑥𝑠)))
7170adantl 480 . . . . . . . . . . . . . . . 16 ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → (𝑥𝑠 → (¬ 𝑠 = {∅} ∧ 𝑥𝑠)))
72 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = {∅} → 𝑡 = {∅})
7372, 52syl6eqss 3617 . . . . . . . . . . . . . . . . . . 19 (𝑡 = {∅} → 𝑡 ⊆ {∅, 1𝑜})
7473sseld 3566 . . . . . . . . . . . . . . . . . 18 (𝑡 = {∅} → (𝑥𝑡𝑥 ∈ {∅, 1𝑜}))
7574anc2li 577 . . . . . . . . . . . . . . . . 17 (𝑡 = {∅} → (𝑥𝑡 → (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})))
7675adantr 479 . . . . . . . . . . . . . . . 16 ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → (𝑥𝑡 → (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})))
7771, 76orim12d 878 . . . . . . . . . . . . . . 15 ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((𝑥𝑠𝑥𝑡) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
7877com12 32 . . . . . . . . . . . . . 14 ((𝑥𝑠𝑥𝑡) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
7928, 78sylbi 205 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑠𝑡) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
8079adantl 480 . . . . . . . . . . . 12 ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
8168, 80jaoi 392 . . . . . . . . . . 11 ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
8264, 81orim12d 878 . . . . . . . . . 10 ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})))))
8382com12 32 . . . . . . . . 9 (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})))))
84 or42 549 . . . . . . . . 9 ((((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))) ↔ (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
8583, 84syl6ib 239 . . . . . . . 8 (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
8685a1i 11 . . . . . . 7 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
87 4exmid 976 . . . . . . . 8 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅})) ∨ ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})))
8887a1i 11 . . . . . . 7 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅})) ∨ ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅}))))
8945, 86, 88mpjaod 394 . . . . . 6 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
901, 89syl5bi 230 . . . . 5 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝑥 ∈ if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
91 elun 3714 . . . . . 6 (𝑥 ∈ (if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡)) ↔ (𝑥 ∈ if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∨ 𝑥 ∈ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡)))
92 elif 4077 . . . . . . 7 (𝑥 ∈ if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ↔ ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)))
93 elif 4077 . . . . . . 7 (𝑥 ∈ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡) ↔ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
9492, 93orbi12i 541 . . . . . 6 ((𝑥 ∈ if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∨ 𝑥 ∈ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡)) ↔ (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
9591, 94sylbbr 224 . . . . 5 ((((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))) → 𝑥 ∈ (if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡)))
9690, 95syl6 34 . . . 4 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝑥 ∈ if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)) → 𝑥 ∈ (if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡))))
9796ssrdv 3573 . . 3 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)) ⊆ (if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡)))
98 3on 7434 . . . . . 6 3𝑜 ∈ On
9998a1i 11 . . . . 5 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → 3𝑜 ∈ On)
100 elpwi 4116 . . . . . 6 (𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ 3𝑜)
101 elpwi 4116 . . . . . 6 (𝑡 ∈ 𝒫 3𝑜𝑡 ⊆ 3𝑜)
102 unss 3748 . . . . . . 7 ((𝑠 ⊆ 3𝑜𝑡 ⊆ 3𝑜) ↔ (𝑠𝑡) ⊆ 3𝑜)
103102biimpi 204 . . . . . 6 ((𝑠 ⊆ 3𝑜𝑡 ⊆ 3𝑜) → (𝑠𝑡) ⊆ 3𝑜)
104100, 101, 103syl2an 492 . . . . 5 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝑠𝑡) ⊆ 3𝑜)
10599, 104sselpwd 4729 . . . 4 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝑠𝑡) ∈ 𝒫 3𝑜)
106 eqeq1 2613 . . . . . 6 (𝑟 = (𝑠𝑡) → (𝑟 = {∅} ↔ (𝑠𝑡) = {∅}))
107 id 22 . . . . . 6 (𝑟 = (𝑠𝑡) → 𝑟 = (𝑠𝑡))
108106, 107ifbieq2d 4060 . . . . 5 (𝑟 = (𝑠𝑡) → if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟) = if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)))
109 clsk1indlem.k . . . . 5 𝐾 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))
110 prex 4831 . . . . . 6 {∅, 1𝑜} ∈ V
111 vex 3175 . . . . . . 7 𝑠 ∈ V
112 vex 3175 . . . . . . 7 𝑡 ∈ V
113111, 112unex 6831 . . . . . 6 (𝑠𝑡) ∈ V
114110, 113ifex 4105 . . . . 5 if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)) ∈ V
115108, 109, 114fvmpt 6176 . . . 4 ((𝑠𝑡) ∈ 𝒫 3𝑜 → (𝐾‘(𝑠𝑡)) = if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)))
116105, 115syl 17 . . 3 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝐾‘(𝑠𝑡)) = if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)))
117 eqeq1 2613 . . . . . . 7 (𝑟 = 𝑠 → (𝑟 = {∅} ↔ 𝑠 = {∅}))
118 id 22 . . . . . . 7 (𝑟 = 𝑠𝑟 = 𝑠)
119117, 118ifbieq2d 4060 . . . . . 6 (𝑟 = 𝑠 → if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟) = if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠))
120110, 111ifex 4105 . . . . . 6 if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∈ V
121119, 109, 120fvmpt 6176 . . . . 5 (𝑠 ∈ 𝒫 3𝑜 → (𝐾𝑠) = if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠))
122121adantr 479 . . . 4 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝐾𝑠) = if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠))
123 eqeq1 2613 . . . . . . 7 (𝑟 = 𝑡 → (𝑟 = {∅} ↔ 𝑡 = {∅}))
124 id 22 . . . . . . 7 (𝑟 = 𝑡𝑟 = 𝑡)
125123, 124ifbieq2d 4060 . . . . . 6 (𝑟 = 𝑡 → if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟) = if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡))
126110, 112ifex 4105 . . . . . 6 if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡) ∈ V
127125, 109, 126fvmpt 6176 . . . . 5 (𝑡 ∈ 𝒫 3𝑜 → (𝐾𝑡) = if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡))
128127adantl 480 . . . 4 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝐾𝑡) = if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡))
129122, 128uneq12d 3729 . . 3 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → ((𝐾𝑠) ∪ (𝐾𝑡)) = (if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡)))
13097, 116, 1293sstr4d 3610 . 2 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝐾‘(𝑠𝑡)) ⊆ ((𝐾𝑠) ∪ (𝐾𝑡)))
131130rgen2a 2959 1 𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝐾‘(𝑠𝑡)) ⊆ ((𝐾𝑠) ∪ (𝐾𝑡))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 381  wa 382  w3o 1029   = wceq 1474  wcel 1976  wral 2895  cun 3537  wss 3539  c0 3873  ifcif 4035  𝒫 cpw 4107  {csn 4124  {cpr 4126  cmpt 4637  Oncon0 5626  cfv 5790  1𝑜c1o 7417  3𝑜c3o 7419
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pr 4828  ax-un 6824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-xor 1456  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-ord 5629  df-on 5630  df-suc 5632  df-iota 5754  df-fun 5792  df-fv 5798  df-1o 7424  df-2o 7425  df-3o 7426
This theorem is referenced by:  clsk1independent  37160
  Copyright terms: Public domain W3C validator