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 38947
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 4285 . . . . . 6 (𝑥 ∈ if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)) ↔ (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))))
2 uneq12 3924 . . . . . . . . . . 11 ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑠𝑡) = ({∅} ∪ {∅}))
3 unidm 3918 . . . . . . . . . . 11 ({∅} ∪ {∅}) = {∅}
42, 3syl6eq 2815 . . . . . . . . . 10 ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑠𝑡) = {∅})
5 an3 649 . . . . . . . . . . . . . 14 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})) → (𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))
65orcd 899 . . . . . . . . . . . . 13 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)))
76orcd 899 . . . . . . . . . . . 12 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
87ex 401 . . . . . . . . . . 11 ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
9 pm2.24 122 . . . . . . . . . . . 12 ((𝑠𝑡) = {∅} → (¬ (𝑠𝑡) = {∅} → (𝑥 ∈ (𝑠𝑡) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
109impd 398 . . . . . . . . . . 11 ((𝑠𝑡) = {∅} → ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
118, 10jaao 977 . . . . . . . . . 10 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ (𝑠𝑡) = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
124, 11mpdan 678 . . . . . . . . 9 ((𝑠 = {∅} ∧ 𝑡 = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
1312a1i 11 . . . . . . . 8 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → ((𝑠 = {∅} ∧ 𝑡 = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
14 uneqsn 38927 . . . . . . . . . . . . 13 ((𝑠𝑡) = {∅} ↔ ((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})))
15 df-3or 1108 . . . . . . . . . . . . 13 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})) ↔ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})))
1614, 15bitri 266 . . . . . . . . . . . 12 ((𝑠𝑡) = {∅} ↔ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})))
17 pm2.21 121 . . . . . . . . . . . . . . . 16 𝑠 = {∅} → (𝑠 = {∅} → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
1817adantrd 485 . . . . . . . . . . . . . . 15 𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
1917adantrd 485 . . . . . . . . . . . . . . 15 𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑡 = ∅) → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2018, 19jaod 885 . . . . . . . . . . . . . 14 𝑠 = {∅} → (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2120adantr 472 . . . . . . . . . . . . 13 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
22 pm2.21 121 . . . . . . . . . . . . . . 15 𝑡 = {∅} → (𝑡 = {∅} → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2322adantl 473 . . . . . . . . . . . . . 14 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → (𝑡 = {∅} → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2423adantld 484 . . . . . . . . . . . . 13 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = ∅ ∧ 𝑡 = {∅}) → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2521, 24jaod 885 . . . . . . . . . . . 12 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})) → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2616, 25syl5bi 233 . . . . . . . . . . 11 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠𝑡) = {∅} → (𝑥 ∈ {∅, 1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
2726impd 398 . . . . . . . . . 10 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
28 elun 3915 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑠𝑡) ↔ (𝑥𝑠𝑥𝑡))
2928biimpi 207 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑠𝑡) → (𝑥𝑠𝑥𝑡))
3029adantl 473 . . . . . . . . . . . . . 14 ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → (𝑥𝑠𝑥𝑡))
31 andi 1030 . . . . . . . . . . . . . . 15 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (𝑥𝑠𝑥𝑡)) ↔ (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑠) ∨ ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑡)))
32 simpl 474 . . . . . . . . . . . . . . . . 17 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ¬ 𝑠 = {∅})
3332anim1i 608 . . . . . . . . . . . . . . . 16 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑠) → (¬ 𝑠 = {∅} ∧ 𝑥𝑠))
34 simpr 477 . . . . . . . . . . . . . . . . 17 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ¬ 𝑡 = {∅})
3534anim1i 608 . . . . . . . . . . . . . . . 16 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑡) → (¬ 𝑡 = {∅} ∧ 𝑥𝑡))
3633, 35orim12i 932 . . . . . . . . . . . . . . 15 ((((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑠) ∨ ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥𝑡)) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
3731, 36sylbi 208 . . . . . . . . . . . . . 14 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (𝑥𝑠𝑥𝑡)) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
3830, 37sylan2 586 . . . . . . . . . . . . 13 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
3938olcd 900 . . . . . . . . . . . 12 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
40 or4 950 . . . . . . . . . . . 12 ((((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))) ↔ (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
4139, 40sylib 209 . . . . . . . . . . 11 (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
4241ex 401 . . . . . . . . . 10 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
4327, 42jaod 885 . . . . . . . . 9 ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
4443a1i 11 . . . . . . . 8 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
4513, 44jaod 885 . . . . . . 7 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅})) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
46 orc 893 . . . . . . . . . . . . . . 15 ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
4746expcom 402 . . . . . . . . . . . . . 14 (𝑥 ∈ {∅, 1𝑜} → (𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
4847adantrd 485 . . . . . . . . . . . . 13 (𝑥 ∈ {∅, 1𝑜} → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
4948adantl 473 . . . . . . . . . . . 12 (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
50 simpr 477 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑠𝑠 = {∅}) → 𝑠 = {∅})
51 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = {∅} → 𝑠 = {∅})
52 snsspr1 4499 . . . . . . . . . . . . . . . . . . . . 21 {∅} ⊆ {∅, 1𝑜}
5351, 52syl6eqss 3815 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = {∅} → 𝑠 ⊆ {∅, 1𝑜})
5453sseld 3760 . . . . . . . . . . . . . . . . . . 19 (𝑠 = {∅} → (𝑥𝑠𝑥 ∈ {∅, 1𝑜}))
5554impcom 396 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑠𝑠 = {∅}) → 𝑥 ∈ {∅, 1𝑜})
5650, 55jca 507 . . . . . . . . . . . . . . . . 17 ((𝑥𝑠𝑠 = {∅}) → (𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))
5756orcd 899 . . . . . . . . . . . . . . . 16 ((𝑥𝑠𝑠 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
5857ex 401 . . . . . . . . . . . . . . 15 (𝑥𝑠 → (𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
59 olc 894 . . . . . . . . . . . . . . . 16 ((¬ 𝑡 = {∅} ∧ 𝑥𝑡) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
6059expcom 402 . . . . . . . . . . . . . . 15 (𝑥𝑡 → (¬ 𝑡 = {∅} → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
6158, 60jaoa 978 . . . . . . . . . . . . . 14 ((𝑥𝑠𝑥𝑡) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
6228, 61sylbi 208 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑠𝑡) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
6362adantl 473 . . . . . . . . . . . 12 ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
6449, 63jaoi 883 . . . . . . . . . . 11 ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
65 olc 894 . . . . . . . . . . . . . . 15 ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})))
6665expcom 402 . . . . . . . . . . . . . 14 (𝑥 ∈ {∅, 1𝑜} → (𝑡 = {∅} → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
6766adantl 473 . . . . . . . . . . . . 13 (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → (𝑡 = {∅} → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
6867adantrd 485 . . . . . . . . . . . 12 (((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
69 id 22 . . . . . . . . . . . . . . . . . 18 ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) → (¬ 𝑠 = {∅} ∧ 𝑥𝑠))
7069ex 401 . . . . . . . . . . . . . . . . 17 𝑠 = {∅} → (𝑥𝑠 → (¬ 𝑠 = {∅} ∧ 𝑥𝑠)))
7170adantl 473 . . . . . . . . . . . . . . . 16 ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → (𝑥𝑠 → (¬ 𝑠 = {∅} ∧ 𝑥𝑠)))
72 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = {∅} → 𝑡 = {∅})
7372, 52syl6eqss 3815 . . . . . . . . . . . . . . . . . . 19 (𝑡 = {∅} → 𝑡 ⊆ {∅, 1𝑜})
7473sseld 3760 . . . . . . . . . . . . . . . . . 18 (𝑡 = {∅} → (𝑥𝑡𝑥 ∈ {∅, 1𝑜}))
7574anc2li 551 . . . . . . . . . . . . . . . . 17 (𝑡 = {∅} → (𝑥𝑡 → (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})))
7675adantr 472 . . . . . . . . . . . . . . . 16 ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → (𝑥𝑡 → (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})))
7771, 76orim12d 987 . . . . . . . . . . . . . . 15 ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((𝑥𝑠𝑥𝑡) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
7877com12 32 . . . . . . . . . . . . . 14 ((𝑥𝑠𝑥𝑡) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
7928, 78sylbi 208 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑠𝑡) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
8079adantl 473 . . . . . . . . . . . 12 ((¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡)) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
8168, 80jaoi 883 . . . . . . . . . . 11 ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))))
8264, 81orim12d 987 . . . . . . . . . 10 ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})))))
8382com12 32 . . . . . . . . 9 (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})))))
84 or42 951 . . . . . . . . 9 ((((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))) ↔ (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
8583, 84syl6ib 242 . . . . . . . 8 (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
8685a1i 11 . . . . . . 7 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))))
87 4exmid 1074 . . . . . . . 8 (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅})) ∨ ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})))
8887a1i 11 . . . . . . 7 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅})) ∨ ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅}))))
8945, 86, 88mpjaod 886 . . . . . 6 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → ((((𝑠𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ (𝑠𝑡) = {∅} ∧ 𝑥 ∈ (𝑠𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
901, 89syl5bi 233 . . . . 5 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝑥 ∈ if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))))
91 elun 3915 . . . . . 6 (𝑥 ∈ (if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡)) ↔ (𝑥 ∈ if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∨ 𝑥 ∈ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡)))
92 elif 4285 . . . . . . 7 (𝑥 ∈ if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ↔ ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)))
93 elif 4285 . . . . . . 7 (𝑥 ∈ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡) ↔ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡)))
9492, 93orbi12i 938 . . . . . 6 ((𝑥 ∈ if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∨ 𝑥 ∈ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡)) ↔ (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))))
9591, 94sylbbr 227 . . . . 5 ((((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥𝑡))) → 𝑥 ∈ (if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡)))
9690, 95syl6 35 . . . 4 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝑥 ∈ if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)) → 𝑥 ∈ (if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡))))
9796ssrdv 3767 . . 3 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)) ⊆ (if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡)))
98 3on 7775 . . . . . 6 3𝑜 ∈ On
9998a1i 11 . . . . 5 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → 3𝑜 ∈ On)
100 elpwi 4325 . . . . . 6 (𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ 3𝑜)
101 elpwi 4325 . . . . . 6 (𝑡 ∈ 𝒫 3𝑜𝑡 ⊆ 3𝑜)
102 unss 3949 . . . . . . 7 ((𝑠 ⊆ 3𝑜𝑡 ⊆ 3𝑜) ↔ (𝑠𝑡) ⊆ 3𝑜)
103102biimpi 207 . . . . . 6 ((𝑠 ⊆ 3𝑜𝑡 ⊆ 3𝑜) → (𝑠𝑡) ⊆ 3𝑜)
104100, 101, 103syl2an 589 . . . . 5 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝑠𝑡) ⊆ 3𝑜)
10599, 104sselpwd 4968 . . . 4 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝑠𝑡) ∈ 𝒫 3𝑜)
106 eqeq1 2769 . . . . . 6 (𝑟 = (𝑠𝑡) → (𝑟 = {∅} ↔ (𝑠𝑡) = {∅}))
107 id 22 . . . . . 6 (𝑟 = (𝑠𝑡) → 𝑟 = (𝑠𝑡))
108106, 107ifbieq2d 4268 . . . . 5 (𝑟 = (𝑠𝑡) → if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟) = if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)))
109 clsk1indlem.k . . . . 5 𝐾 = (𝑟 ∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟))
110 prex 5065 . . . . . 6 {∅, 1𝑜} ∈ V
111 vex 3353 . . . . . . 7 𝑠 ∈ V
112 vex 3353 . . . . . . 7 𝑡 ∈ V
113111, 112unex 7154 . . . . . 6 (𝑠𝑡) ∈ V
114110, 113ifex 4291 . . . . 5 if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)) ∈ V
115108, 109, 114fvmpt 6471 . . . 4 ((𝑠𝑡) ∈ 𝒫 3𝑜 → (𝐾‘(𝑠𝑡)) = if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)))
116105, 115syl 17 . . 3 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝐾‘(𝑠𝑡)) = if((𝑠𝑡) = {∅}, {∅, 1𝑜}, (𝑠𝑡)))
117 eqeq1 2769 . . . . . . 7 (𝑟 = 𝑠 → (𝑟 = {∅} ↔ 𝑠 = {∅}))
118 id 22 . . . . . . 7 (𝑟 = 𝑠𝑟 = 𝑠)
119117, 118ifbieq2d 4268 . . . . . 6 (𝑟 = 𝑠 → if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟) = if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠))
120110, 111ifex 4291 . . . . . 6 if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∈ V
121119, 109, 120fvmpt 6471 . . . . 5 (𝑠 ∈ 𝒫 3𝑜 → (𝐾𝑠) = if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠))
122121adantr 472 . . . 4 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝐾𝑠) = if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠))
123 eqeq1 2769 . . . . . . 7 (𝑟 = 𝑡 → (𝑟 = {∅} ↔ 𝑡 = {∅}))
124 id 22 . . . . . . 7 (𝑟 = 𝑡𝑟 = 𝑡)
125123, 124ifbieq2d 4268 . . . . . 6 (𝑟 = 𝑡 → if(𝑟 = {∅}, {∅, 1𝑜}, 𝑟) = if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡))
126110, 112ifex 4291 . . . . . 6 if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡) ∈ V
127125, 109, 126fvmpt 6471 . . . . 5 (𝑡 ∈ 𝒫 3𝑜 → (𝐾𝑡) = if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡))
128127adantl 473 . . . 4 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝐾𝑡) = if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡))
129122, 128uneq12d 3930 . . 3 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → ((𝐾𝑠) ∪ (𝐾𝑡)) = (if(𝑠 = {∅}, {∅, 1𝑜}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1𝑜}, 𝑡)))
13097, 116, 1293sstr4d 3808 . 2 ((𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜) → (𝐾‘(𝑠𝑡)) ⊆ ((𝐾𝑠) ∪ (𝐾𝑡)))
131130rgen2a 3124 1 𝑠 ∈ 𝒫 3𝑜𝑡 ∈ 𝒫 3𝑜(𝐾‘(𝑠𝑡)) ⊆ ((𝐾𝑠) ∪ (𝐾𝑡))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  wo 873  w3o 1106   = wceq 1652  wcel 2155  wral 3055  cun 3730  wss 3732  c0 4079  ifcif 4243  𝒫 cpw 4315  {csn 4334  {cpr 4336  cmpt 4888  Oncon0 5908  cfv 6068  1𝑜c1o 7757  3𝑜c3o 7759
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-xor 1634  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-ord 5911  df-on 5912  df-suc 5914  df-iota 6031  df-fun 6070  df-fv 6076  df-1o 7764  df-2o 7765  df-3o 7766
This theorem is referenced by:  clsk1independent  38950
  Copyright terms: Public domain W3C validator