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

Theorem clsk1indlem3 38658
 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 4161 . . . . . 6 (𝑥 ∈ if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)) ↔ (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))))
2 uneq12 3795 . . . . . . . . . . 11 ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑠𝑡) = ({∅} ∪ {∅}))
3 unidm 3789 . . . . . . . . . . 11 ({∅} ∪ {∅}) = {∅}
42, 3syl6eq 2701 . . . . . . . . . 10 ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑠𝑡) = {∅})
5 an3 885 . . . . . . . . . . . . . 14 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})) → (𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))
65orcd 406 . . . . . . . . . . . . 13 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)))
76orcd 406 . . . . . . . . . . . 12 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
87ex 449 . . . . . . . . . . 11 ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
9 pm2.24 121 . . . . . . . . . . . 12 ((𝑠𝑡) = {∅} → (¬ (𝑠𝑡) = {∅} → (𝑥 ∈ (𝑠𝑡) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
109impd 446 . . . . . . . . . . 11 ((𝑠𝑡) = {∅} → ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
118, 10jaao 530 . . . . . . . . . 10 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ (𝑠𝑡) = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
124, 11mpdan 703 . . . . . . . . 9 ((𝑠 = {∅} ∧ 𝑡 = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
1312a1i 11 . . . . . . . 8 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → ((𝑠 = {∅} ∧ 𝑡 = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
14 uneqsn 38638 . . . . . . . . . . . . 13 ((𝑠𝑡) = {∅} ↔ ((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})))
15 df-3or 1055 . . . . . . . . . . . . 13 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})) ↔ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})))
1614, 15bitri 264 . . . . . . . . . . . 12 ((𝑠𝑡) = {∅} ↔ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})))
17 pm2.21 120 . . . . . . . . . . . . . . . 16 𝑠 = {∅} → (𝑠 = {∅} → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
1817adantrd 483 . . . . . . . . . . . . . . 15 𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
1917adantrd 483 . . . . . . . . . . . . . . 15 𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑡 = ∅) → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2018, 19jaod 394 . . . . . . . . . . . . . 14 𝑠 = {∅} → (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2120adantr 480 . . . . . . . . . . . . 13 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
22 pm2.21 120 . . . . . . . . . . . . . . 15 𝑡 = {∅} → (𝑡 = {∅} → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2322adantl 481 . . . . . . . . . . . . . 14 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → (𝑡 = {∅} → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2423adantld 482 . . . . . . . . . . . . 13 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = ∅ ∧ 𝑡 = {∅}) → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2521, 24jaod 394 . . . . . . . . . . . 12 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})) → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2616, 25syl5bi 232 . . . . . . . . . . 11 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠𝑡) = {∅} → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2726impd 446 . . . . . . . . . 10 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
28 elun 3786 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑠𝑡) ↔ (𝑥𝑠𝑥𝑡))
2928biimpi 206 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑠𝑡) → (𝑥𝑠𝑥𝑡))
3029adantl 481 . . . . . . . . . . . . . 14 ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → (𝑥𝑠𝑥𝑡))
31 andi 929 . . . . . . . . . . . . . . 15 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (𝑥𝑠𝑥𝑡)) ↔ (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑠) ∨ ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑡)))
32 simpl 472 . . . . . . . . . . . . . . . . 17 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ¬ 𝑠 = {∅})
3332anim1i 591 . . . . . . . . . . . . . . . 16 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑠) → (¬ 𝑠 = {∅} ∧ 𝑥𝑠))
34 simpr 476 . . . . . . . . . . . . . . . . 17 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ¬ 𝑡 = {∅})
3534anim1i 591 . . . . . . . . . . . . . . . 16 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑡) → (¬ 𝑡 = {∅} ∧ 𝑥𝑡))
3633, 35orim12i 537 . . . . . . . . . . . . . . 15 ((((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑠) ∨ ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑡)) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
3731, 36sylbi 207 . . . . . . . . . . . . . 14 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (𝑥𝑠𝑥𝑡)) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
3830, 37sylan2 490 . . . . . . . . . . . . 13 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
3938olcd 407 . . . . . . . . . . . 12 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
40 or4 549 . . . . . . . . . . . 12 ((((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))) ↔ (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
4139, 40sylib 208 . . . . . . . . . . 11 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
4241ex 449 . . . . . . . . . 10 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
4327, 42jaod 394 . . . . . . . . 9 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
4443a1i 11 . . . . . . . 8 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
4513, 44jaod 394 . . . . . . 7 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅})) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
46 orc 399 . . . . . . . . . . . . . . 15 ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
4746expcom 450 . . . . . . . . . . . . . 14 (𝑥 ∈ {∅, 1𝑜} → (𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
4847adantrd 483 . . . . . . . . . . . . 13 (𝑥 ∈ {∅, 1𝑜} → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
4948adantl 481 . . . . . . . . . . . 12 (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
50 simpr 476 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑠𝑠 = {∅}) → 𝑠 = {∅})
51 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = {∅} → 𝑠 = {∅})
52 snsspr1 4377 . . . . . . . . . . . . . . . . . . . . 21 {∅} ⊆ {∅, 1𝑜}
5351, 52syl6eqss 3688 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = {∅} → 𝑠 ⊆ {∅, 1𝑜})
5453sseld 3635 . . . . . . . . . . . . . . . . . . 19 (𝑠 = {∅} → (𝑥𝑠𝑥 ∈ {∅, 1𝑜}))
5554impcom 445 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑠𝑠 = {∅}) → 𝑥 ∈ {∅, 1𝑜})
5650, 55jca 553 . . . . . . . . . . . . . . . . 17 ((𝑥𝑠𝑠 = {∅}) → (𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))
5756orcd 406 . . . . . . . . . . . . . . . 16 ((𝑥𝑠𝑠 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
5857ex 449 . . . . . . . . . . . . . . 15 (𝑥𝑠 → (𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
59 olc 398 . . . . . . . . . . . . . . . 16 ((¬ 𝑡 = {∅} ∧ 𝑥𝑡) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
6059expcom 450 . . . . . . . . . . . . . . 15 (𝑥𝑡 → (¬ 𝑡 = {∅} → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
6158, 60jaoa 531 . . . . . . . . . . . . . 14 ((𝑥𝑠𝑥𝑡) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
6228, 61sylbi 207 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑠𝑡) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
6362adantl 481 . . . . . . . . . . . 12 ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
6449, 63jaoi 393 . . . . . . . . . . 11 ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
65 olc 398 . . . . . . . . . . . . . . 15 ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})))
6665expcom 450 . . . . . . . . . . . . . 14 (𝑥 ∈ {∅, 1𝑜} → (𝑡 = {∅} → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
6766adantl 481 . . . . . . . . . . . . 13 (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → (𝑡 = {∅} → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
6867adantrd 483 . . . . . . . . . . . 12 (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
69 id 22 . . . . . . . . . . . . . . . . . 18 ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) → (¬ 𝑠 = {∅} ∧ 𝑥𝑠))
7069ex 449 . . . . . . . . . . . . . . . . 17 𝑠 = {∅} → (𝑥𝑠 → (¬ 𝑠 = {∅} ∧ 𝑥𝑠)))
7170adantl 481 . . . . . . . . . . . . . . . 16 ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → (𝑥𝑠 → (¬ 𝑠 = {∅} ∧ 𝑥𝑠)))
72 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = {∅} → 𝑡 = {∅})
7372, 52syl6eqss 3688 . . . . . . . . . . . . . . . . . . 19 (𝑡 = {∅} → 𝑡 ⊆ {∅, 1𝑜})
7473sseld 3635 . . . . . . . . . . . . . . . . . 18 (𝑡 = {∅} → (𝑥𝑡𝑥 ∈ {∅, 1𝑜}))
7574anc2li 579 . . . . . . . . . . . . . . . . 17 (𝑡 = {∅} → (𝑥𝑡 → (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})))
7675adantr 480 . . . . . . . . . . . . . . . 16 ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → (𝑥𝑡 → (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})))
7771, 76orim12d 901 . . . . . . . . . . . . . . 15 ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((𝑥𝑠𝑥𝑡) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
7877com12 32 . . . . . . . . . . . . . 14 ((𝑥𝑠𝑥𝑡) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
7928, 78sylbi 207 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑠𝑡) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
8079adantl 481 . . . . . . . . . . . 12 ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
8168, 80jaoi 393 . . . . . . . . . . 11 ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
8264, 81orim12d 901 . . . . . . . . . 10 ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})))))
8382com12 32 . . . . . . . . 9 (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})))))
84 or42 550 . . . . . . . . 9 ((((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))) ↔ (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
8583, 84syl6ib 241 . . . . . . . 8 (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
8685a1i 11 . . . . . . 7 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
87 4exmid 1021 . . . . . . . 8 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅})) ∨ ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})))
8887a1i 11 . . . . . . 7 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅})) ∨ ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅}))))
8945, 86, 88mpjaod 395 . . . . . 6 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
901, 89syl5bi 232 . . . . 5 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝑥 ∈ if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
91 elun 3786 . . . . . 6 (𝑥 ∈ (if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡)) ↔ (𝑥 ∈ if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∨ 𝑥 ∈ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡)))
92 elif 4161 . . . . . . 7 (𝑥 ∈ if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ↔ ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)))
93 elif 4161 . . . . . . 7 (𝑥 ∈ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡) ↔ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
9492, 93orbi12i 542 . . . . . 6 ((𝑥 ∈ if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∨ 𝑥 ∈ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡)) ↔ (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
9591, 94sylbbr 226 . . . . 5 ((((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))) → 𝑥 ∈ (if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡)))
9690, 95syl6 35 . . . 4 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝑥 ∈ if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)) → 𝑥 ∈ (if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡))))
9796ssrdv 3642 . . 3 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)) ⊆ (if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡)))
98 3on 7615 . . . . . 6 3𝑜 ∈ On
9998a1i 11 . . . . 5 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → 3𝑜 ∈ On)
100 elpwi 4201 . . . . . 6 (𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ 3𝑜)
101 elpwi 4201 . . . . . 6 (𝑡 ∈ 𝒫 3𝑜𝑡 ⊆ 3𝑜)
102 unss 3820 . . . . . . 7 ((𝑠 ⊆ 3𝑜𝑡 ⊆ 3𝑜) ↔ (𝑠𝑡) ⊆ 3𝑜)
103102biimpi 206 . . . . . 6 ((𝑠 ⊆ 3𝑜𝑡 ⊆ 3𝑜) → (𝑠𝑡) ⊆ 3𝑜)
104100, 101, 103syl2an 493 . . . . 5 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝑠𝑡) ⊆ 3𝑜)
10599, 104sselpwd 4840 . . . 4 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝑠𝑡) ∈ 𝒫 3𝑜)
106 eqeq1 2655 . . . . . 6 (𝑟 = (𝑠𝑡) → (𝑟 = {∅} ↔ (𝑠𝑡) = {∅}))
107 id 22 . . . . . 6 (𝑟 = (𝑠𝑡) → 𝑟 = (𝑠𝑡))
108106, 107ifbieq2d 4144 . . . . 5 (𝑟 = (𝑠𝑡) → if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟) = if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)))
109 clsk1indlem.k . . . . 5 𝐾 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))
110 prex 4939 . . . . . 6 {∅, 1𝑜} ∈ V
111 vex 3234 . . . . . . 7 𝑠 ∈ V
112 vex 3234 . . . . . . 7 𝑡 ∈ V
113111, 112unex 6998 . . . . . 6 (𝑠𝑡) ∈ V
114110, 113ifex 4189 . . . . 5 if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)) ∈ V
115108, 109, 114fvmpt 6321 . . . 4 ((𝑠𝑡) ∈ 𝒫 3𝑜 → (𝐾‘(𝑠𝑡)) = if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)))
116105, 115syl 17 . . 3 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝐾‘(𝑠𝑡)) = if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)))
117 eqeq1 2655 . . . . . . 7 (𝑟 = 𝑠 → (𝑟 = {∅} ↔ 𝑠 = {∅}))
118 id 22 . . . . . . 7 (𝑟 = 𝑠𝑟 = 𝑠)
119117, 118ifbieq2d 4144 . . . . . 6 (𝑟 = 𝑠 → if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟) = if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠))
120110, 111ifex 4189 . . . . . 6 if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∈ V
121119, 109, 120fvmpt 6321 . . . . 5 (𝑠 ∈ 𝒫 3𝑜 → (𝐾𝑠) = if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠))
122121adantr 480 . . . 4 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝐾𝑠) = if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠))
123 eqeq1 2655 . . . . . . 7 (𝑟 = 𝑡 → (𝑟 = {∅} ↔ 𝑡 = {∅}))
124 id 22 . . . . . . 7 (𝑟 = 𝑡𝑟 = 𝑡)
125123, 124ifbieq2d 4144 . . . . . 6 (𝑟 = 𝑡 → if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟) = if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡))
126110, 112ifex 4189 . . . . . 6 if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡) ∈ V
127125, 109, 126fvmpt 6321 . . . . 5 (𝑡 ∈ 𝒫 3𝑜 → (𝐾𝑡) = if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡))
128127adantl 481 . . . 4 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝐾𝑡) = if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡))
129122, 128uneq12d 3801 . . 3 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → ((𝐾𝑠) ∪ (𝐾𝑡)) = (if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡)))
13097, 116, 1293sstr4d 3681 . 2 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝐾‘(𝑠𝑡)) ⊆ ((𝐾𝑠) ∪ (𝐾𝑡)))
131130rgen2a 3006 1 𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝐾‘(𝑠𝑡)) ⊆ ((𝐾𝑠) ∪ (𝐾𝑡))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382   ∧ wa 383   ∨ w3o 1053   = wceq 1523   ∈ wcel 2030  ∀wral 2941   ∪ cun 3605   ⊆ wss 3607  ∅c0 3948  ifcif 4119  𝒫 cpw 4191  {csn 4210  {cpr 4212   ↦ cmpt 4762  Oncon0 5761  ‘cfv 5926  1𝑜c1o 7598  3𝑜c3o 7600 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936  ax-un 6991 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-xor 1505  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-ord 5764  df-on 5765  df-suc 5767  df-iota 5889  df-fun 5928  df-fv 5934  df-1o 7605  df-2o 7606  df-3o 7607 This theorem is referenced by:  clsk1independent  38661
 Copyright terms: Public domain W3C validator