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

Theorem clsk3nimkb 43393
Description: If the base set is not empty, axiom K3 does not imply KB. A concrete example with a pseudo-closure function of π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯)) is given. (Contributed by RP, 16-Jun-2021.)
Assertion
Ref Expression
clsk3nimkb Β¬ βˆ€π‘βˆ€π‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) β†’ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏))
Distinct variable group:   π‘˜,𝑏,𝑑,𝑠

Proof of Theorem clsk3nimkb
Dummy variables π‘₯ 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1oex 8490 . . . . 5 1o ∈ V
2 1n0 8502 . . . . . 6 1o β‰  βˆ…
3 nelsn 4664 . . . . . 6 (1o β‰  βˆ… β†’ Β¬ 1o ∈ {βˆ…})
42, 3ax-mp 5 . . . . 5 Β¬ 1o ∈ {βˆ…}
5 eldif 3954 . . . . . 6 (1o ∈ (V βˆ– {βˆ…}) ↔ (1o ∈ V ∧ Β¬ 1o ∈ {βˆ…}))
6 ne0i 4330 . . . . . 6 (1o ∈ (V βˆ– {βˆ…}) β†’ (V βˆ– {βˆ…}) β‰  βˆ…)
75, 6sylbir 234 . . . . 5 ((1o ∈ V ∧ Β¬ 1o ∈ {βˆ…}) β†’ (V βˆ– {βˆ…}) β‰  βˆ…)
81, 4, 7mp2an 691 . . . 4 (V βˆ– {βˆ…}) β‰  βˆ…
9 r19.2zb 4491 . . . 4 ((V βˆ– {βˆ…}) β‰  βˆ… ↔ (βˆ€π‘ ∈ (V βˆ– {βˆ…})βˆƒπ‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ Β¬ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏)) β†’ βˆƒπ‘ ∈ (V βˆ– {βˆ…})βˆƒπ‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ Β¬ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏))))
108, 9mpbi 229 . . 3 (βˆ€π‘ ∈ (V βˆ– {βˆ…})βˆƒπ‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ Β¬ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏)) β†’ βˆƒπ‘ ∈ (V βˆ– {βˆ…})βˆƒπ‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ Β¬ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏)))
11 rexex 3071 . . 3 (βˆƒπ‘ ∈ (V βˆ– {βˆ…})βˆƒπ‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ Β¬ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏)) β†’ βˆƒπ‘βˆƒπ‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ Β¬ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏)))
12 rexanali 3097 . . . . 5 (βˆƒπ‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ Β¬ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏)) ↔ Β¬ βˆ€π‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) β†’ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏)))
1312exbii 1843 . . . 4 (βˆƒπ‘βˆƒπ‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ Β¬ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏)) ↔ βˆƒπ‘ Β¬ βˆ€π‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) β†’ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏)))
14 exnal 1822 . . . 4 (βˆƒπ‘ Β¬ βˆ€π‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) β†’ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏)) ↔ Β¬ βˆ€π‘βˆ€π‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) β†’ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏)))
1513, 14sylbb 218 . . 3 (βˆƒπ‘βˆƒπ‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ Β¬ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏)) β†’ Β¬ βˆ€π‘βˆ€π‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) β†’ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏)))
1610, 11, 153syl 18 . 2 (βˆ€π‘ ∈ (V βˆ– {βˆ…})βˆƒπ‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ Β¬ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏)) β†’ Β¬ βˆ€π‘βˆ€π‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) β†’ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏)))
17 difelpw 5347 . . . . . 6 (𝑏 ∈ (V βˆ– {βˆ…}) β†’ (𝑏 βˆ– π‘₯) ∈ 𝒫 𝑏)
1817adantr 480 . . . . 5 ((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘₯ ∈ 𝒫 𝑏) β†’ (𝑏 βˆ– π‘₯) ∈ 𝒫 𝑏)
1918fmpttd 7119 . . . 4 (𝑏 ∈ (V βˆ– {βˆ…}) β†’ (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯)):𝒫 π‘βŸΆπ’« 𝑏)
20 pwexg 5372 . . . . 5 (𝑏 ∈ (V βˆ– {βˆ…}) β†’ 𝒫 𝑏 ∈ V)
2120, 20elmapd 8850 . . . 4 (𝑏 ∈ (V βˆ– {βˆ…}) β†’ ((π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯)) ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↔ (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯)):𝒫 π‘βŸΆπ’« 𝑏))
2219, 21mpbird 257 . . 3 (𝑏 ∈ (V βˆ– {βˆ…}) β†’ (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯)) ∈ (𝒫 𝑏 ↑m 𝒫 𝑏))
23 simpllr 775 . . . . . . . . 9 ((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) β†’ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯)))
24 difeq2 4112 . . . . . . . . . 10 (π‘₯ = 𝑧 β†’ (𝑏 βˆ– π‘₯) = (𝑏 βˆ– 𝑧))
2524cbvmptv 5255 . . . . . . . . 9 (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯)) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– 𝑧))
2623, 25eqtrdi 2783 . . . . . . . 8 ((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) β†’ π‘˜ = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– 𝑧)))
27 difeq2 4112 . . . . . . . . 9 (𝑧 = (𝑠 βˆͺ 𝑑) β†’ (𝑏 βˆ– 𝑧) = (𝑏 βˆ– (𝑠 βˆͺ 𝑑)))
2827adantl 481 . . . . . . . 8 (((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) ∧ 𝑧 = (𝑠 βˆͺ 𝑑)) β†’ (𝑏 βˆ– 𝑧) = (𝑏 βˆ– (𝑠 βˆͺ 𝑑)))
29 simplll 774 . . . . . . . . 9 ((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) β†’ 𝑏 ∈ (V βˆ– {βˆ…}))
30 simplr 768 . . . . . . . . . . 11 ((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) β†’ 𝑠 ∈ 𝒫 𝑏)
3130elpwid 4607 . . . . . . . . . 10 ((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) β†’ 𝑠 βŠ† 𝑏)
32 simpr 484 . . . . . . . . . . 11 ((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) β†’ 𝑑 ∈ 𝒫 𝑏)
3332elpwid 4607 . . . . . . . . . 10 ((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) β†’ 𝑑 βŠ† 𝑏)
3431, 33unssd 4182 . . . . . . . . 9 ((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) β†’ (𝑠 βˆͺ 𝑑) βŠ† 𝑏)
3529, 34sselpwd 5322 . . . . . . . 8 ((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) β†’ (𝑠 βˆͺ 𝑑) ∈ 𝒫 𝑏)
36 vex 3473 . . . . . . . . . 10 𝑏 ∈ V
3736difexi 5324 . . . . . . . . 9 (𝑏 βˆ– (𝑠 βˆͺ 𝑑)) ∈ V
3837a1i 11 . . . . . . . 8 ((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) β†’ (𝑏 βˆ– (𝑠 βˆͺ 𝑑)) ∈ V)
3926, 28, 35, 38fvmptd 7006 . . . . . . 7 ((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) β†’ (π‘˜β€˜(𝑠 βˆͺ 𝑑)) = (𝑏 βˆ– (𝑠 βˆͺ 𝑑)))
40 difeq2 4112 . . . . . . . . . . 11 (𝑧 = 𝑠 β†’ (𝑏 βˆ– 𝑧) = (𝑏 βˆ– 𝑠))
4140adantl 481 . . . . . . . . . 10 (((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) ∧ 𝑧 = 𝑠) β†’ (𝑏 βˆ– 𝑧) = (𝑏 βˆ– 𝑠))
4236difexi 5324 . . . . . . . . . . 11 (𝑏 βˆ– 𝑠) ∈ V
4342a1i 11 . . . . . . . . . 10 ((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) β†’ (𝑏 βˆ– 𝑠) ∈ V)
4426, 41, 30, 43fvmptd 7006 . . . . . . . . 9 ((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) β†’ (π‘˜β€˜π‘ ) = (𝑏 βˆ– 𝑠))
45 difeq2 4112 . . . . . . . . . . 11 (𝑧 = 𝑑 β†’ (𝑏 βˆ– 𝑧) = (𝑏 βˆ– 𝑑))
4645adantl 481 . . . . . . . . . 10 (((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) ∧ 𝑧 = 𝑑) β†’ (𝑏 βˆ– 𝑧) = (𝑏 βˆ– 𝑑))
4736difexi 5324 . . . . . . . . . . 11 (𝑏 βˆ– 𝑑) ∈ V
4847a1i 11 . . . . . . . . . 10 ((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) β†’ (𝑏 βˆ– 𝑑) ∈ V)
4926, 46, 32, 48fvmptd 7006 . . . . . . . . 9 ((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) β†’ (π‘˜β€˜π‘‘) = (𝑏 βˆ– 𝑑))
5044, 49uneq12d 4160 . . . . . . . 8 ((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = ((𝑏 βˆ– 𝑠) βˆͺ (𝑏 βˆ– 𝑑)))
51 difindi 4277 . . . . . . . 8 (𝑏 βˆ– (𝑠 ∩ 𝑑)) = ((𝑏 βˆ– 𝑠) βˆͺ (𝑏 βˆ– 𝑑))
5250, 51eqtr4di 2785 . . . . . . 7 ((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = (𝑏 βˆ– (𝑠 ∩ 𝑑)))
5339, 52sseq12d 4011 . . . . . 6 ((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) β†’ ((π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ↔ (𝑏 βˆ– (𝑠 βˆͺ 𝑑)) βŠ† (𝑏 βˆ– (𝑠 ∩ 𝑑))))
5453ralbidva 3170 . . . . 5 (((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) β†’ (βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ↔ βˆ€π‘‘ ∈ 𝒫 𝑏(𝑏 βˆ– (𝑠 βˆͺ 𝑑)) βŠ† (𝑏 βˆ– (𝑠 ∩ 𝑑))))
5554ralbidva 3170 . . . 4 ((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) β†’ (βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ↔ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(𝑏 βˆ– (𝑠 βˆͺ 𝑑)) βŠ† (𝑏 βˆ– (𝑠 ∩ 𝑑))))
5652eqeq1d 2729 . . . . . . . 8 ((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) β†’ (((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏 ↔ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏))
5756imbi2d 340 . . . . . . 7 ((((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑑 ∈ 𝒫 𝑏) β†’ (((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏) ↔ ((𝑠 βˆͺ 𝑑) = 𝑏 β†’ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏)))
5857ralbidva 3170 . . . . . 6 (((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) ∧ 𝑠 ∈ 𝒫 𝑏) β†’ (βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏) ↔ βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏)))
5958ralbidva 3170 . . . . 5 ((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) β†’ (βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏) ↔ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏)))
6059notbid 318 . . . 4 ((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) β†’ (Β¬ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏) ↔ Β¬ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏)))
6155, 60anbi12d 630 . . 3 ((𝑏 ∈ (V βˆ– {βˆ…}) ∧ π‘˜ = (π‘₯ ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– π‘₯))) β†’ ((βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ Β¬ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏)) ↔ (βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(𝑏 βˆ– (𝑠 βˆͺ 𝑑)) βŠ† (𝑏 βˆ– (𝑠 ∩ 𝑑)) ∧ Β¬ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏))))
62 pwidg 4618 . . . . . 6 (𝑏 ∈ (V βˆ– {βˆ…}) β†’ 𝑏 ∈ 𝒫 𝑏)
63 ssidd 4001 . . . . . 6 (𝑏 ∈ (V βˆ– {βˆ…}) β†’ 𝑏 βŠ† 𝑏)
64 eldifsnneq 4790 . . . . . 6 (𝑏 ∈ (V βˆ– {βˆ…}) β†’ Β¬ 𝑏 = βˆ…)
65 uneq1 4152 . . . . . . . . . 10 (𝑠 = 𝑏 β†’ (𝑠 βˆͺ 𝑑) = (𝑏 βˆͺ 𝑑))
6665eqeq1d 2729 . . . . . . . . 9 (𝑠 = 𝑏 β†’ ((𝑠 βˆͺ 𝑑) = 𝑏 ↔ (𝑏 βˆͺ 𝑑) = 𝑏))
67 ssequn2 4179 . . . . . . . . 9 (𝑑 βŠ† 𝑏 ↔ (𝑏 βˆͺ 𝑑) = 𝑏)
6866, 67bitr4di 289 . . . . . . . 8 (𝑠 = 𝑏 β†’ ((𝑠 βˆͺ 𝑑) = 𝑏 ↔ 𝑑 βŠ† 𝑏))
69 ineq1 4201 . . . . . . . . . . 11 (𝑠 = 𝑏 β†’ (𝑠 ∩ 𝑑) = (𝑏 ∩ 𝑑))
7069difeq2d 4118 . . . . . . . . . 10 (𝑠 = 𝑏 β†’ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = (𝑏 βˆ– (𝑏 ∩ 𝑑)))
7170eqeq1d 2729 . . . . . . . . 9 (𝑠 = 𝑏 β†’ ((𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏 ↔ (𝑏 βˆ– (𝑏 ∩ 𝑑)) = 𝑏))
7271notbid 318 . . . . . . . 8 (𝑠 = 𝑏 β†’ (Β¬ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏 ↔ Β¬ (𝑏 βˆ– (𝑏 ∩ 𝑑)) = 𝑏))
7368, 72anbi12d 630 . . . . . . 7 (𝑠 = 𝑏 β†’ (((𝑠 βˆͺ 𝑑) = 𝑏 ∧ Β¬ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏) ↔ (𝑑 βŠ† 𝑏 ∧ Β¬ (𝑏 βˆ– (𝑏 ∩ 𝑑)) = 𝑏)))
74 sseq1 4003 . . . . . . . 8 (𝑑 = 𝑏 β†’ (𝑑 βŠ† 𝑏 ↔ 𝑏 βŠ† 𝑏))
75 ineq2 4202 . . . . . . . . . . . . . 14 (𝑑 = 𝑏 β†’ (𝑏 ∩ 𝑑) = (𝑏 ∩ 𝑏))
76 inidm 4214 . . . . . . . . . . . . . 14 (𝑏 ∩ 𝑏) = 𝑏
7775, 76eqtrdi 2783 . . . . . . . . . . . . 13 (𝑑 = 𝑏 β†’ (𝑏 ∩ 𝑑) = 𝑏)
7877difeq2d 4118 . . . . . . . . . . . 12 (𝑑 = 𝑏 β†’ (𝑏 βˆ– (𝑏 ∩ 𝑑)) = (𝑏 βˆ– 𝑏))
79 difid 4366 . . . . . . . . . . . 12 (𝑏 βˆ– 𝑏) = βˆ…
8078, 79eqtrdi 2783 . . . . . . . . . . 11 (𝑑 = 𝑏 β†’ (𝑏 βˆ– (𝑏 ∩ 𝑑)) = βˆ…)
8180eqeq1d 2729 . . . . . . . . . 10 (𝑑 = 𝑏 β†’ ((𝑏 βˆ– (𝑏 ∩ 𝑑)) = 𝑏 ↔ βˆ… = 𝑏))
82 eqcom 2734 . . . . . . . . . 10 (βˆ… = 𝑏 ↔ 𝑏 = βˆ…)
8381, 82bitrdi 287 . . . . . . . . 9 (𝑑 = 𝑏 β†’ ((𝑏 βˆ– (𝑏 ∩ 𝑑)) = 𝑏 ↔ 𝑏 = βˆ…))
8483notbid 318 . . . . . . . 8 (𝑑 = 𝑏 β†’ (Β¬ (𝑏 βˆ– (𝑏 ∩ 𝑑)) = 𝑏 ↔ Β¬ 𝑏 = βˆ…))
8574, 84anbi12d 630 . . . . . . 7 (𝑑 = 𝑏 β†’ ((𝑑 βŠ† 𝑏 ∧ Β¬ (𝑏 βˆ– (𝑏 ∩ 𝑑)) = 𝑏) ↔ (𝑏 βŠ† 𝑏 ∧ Β¬ 𝑏 = βˆ…)))
8673, 85rspc2ev 3620 . . . . . 6 ((𝑏 ∈ 𝒫 𝑏 ∧ 𝑏 ∈ 𝒫 𝑏 ∧ (𝑏 βŠ† 𝑏 ∧ Β¬ 𝑏 = βˆ…)) β†’ βˆƒπ‘  ∈ 𝒫 π‘βˆƒπ‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 ∧ Β¬ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏))
8762, 62, 63, 64, 86syl112anc 1372 . . . . 5 (𝑏 ∈ (V βˆ– {βˆ…}) β†’ βˆƒπ‘  ∈ 𝒫 π‘βˆƒπ‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 ∧ Β¬ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏))
88 rexanali 3097 . . . . . . 7 (βˆƒπ‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 ∧ Β¬ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏) ↔ Β¬ βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏))
8988rexbii 3089 . . . . . 6 (βˆƒπ‘  ∈ 𝒫 π‘βˆƒπ‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 ∧ Β¬ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏) ↔ βˆƒπ‘  ∈ 𝒫 𝑏 Β¬ βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏))
90 rexnal 3095 . . . . . 6 (βˆƒπ‘  ∈ 𝒫 𝑏 Β¬ βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏) ↔ Β¬ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏))
9189, 90sylbb 218 . . . . 5 (βˆƒπ‘  ∈ 𝒫 π‘βˆƒπ‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 ∧ Β¬ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏) β†’ Β¬ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏))
9287, 91syl 17 . . . 4 (𝑏 ∈ (V βˆ– {βˆ…}) β†’ Β¬ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏))
93 inss1 4224 . . . . . . 7 (𝑠 ∩ 𝑑) βŠ† 𝑠
94 ssun1 4168 . . . . . . 7 𝑠 βŠ† (𝑠 βˆͺ 𝑑)
9593, 94sstri 3987 . . . . . 6 (𝑠 ∩ 𝑑) βŠ† (𝑠 βˆͺ 𝑑)
96 sscon 4134 . . . . . 6 ((𝑠 ∩ 𝑑) βŠ† (𝑠 βˆͺ 𝑑) β†’ (𝑏 βˆ– (𝑠 βˆͺ 𝑑)) βŠ† (𝑏 βˆ– (𝑠 ∩ 𝑑)))
9795, 96ax-mp 5 . . . . 5 (𝑏 βˆ– (𝑠 βˆͺ 𝑑)) βŠ† (𝑏 βˆ– (𝑠 ∩ 𝑑))
9897rgen2w 3061 . . . 4 βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(𝑏 βˆ– (𝑠 βˆͺ 𝑑)) βŠ† (𝑏 βˆ– (𝑠 ∩ 𝑑))
9992, 98jctil 519 . . 3 (𝑏 ∈ (V βˆ– {βˆ…}) β†’ (βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(𝑏 βˆ– (𝑠 βˆͺ 𝑑)) βŠ† (𝑏 βˆ– (𝑠 ∩ 𝑑)) ∧ Β¬ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ (𝑏 βˆ– (𝑠 ∩ 𝑑)) = 𝑏)))
10022, 61, 99rspcedvd 3609 . 2 (𝑏 ∈ (V βˆ– {βˆ…}) β†’ βˆƒπ‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) ∧ Β¬ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏)))
10116, 100mprg 3062 1 Β¬ βˆ€π‘βˆ€π‘˜ ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏(π‘˜β€˜(𝑠 βˆͺ 𝑑)) βŠ† ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) β†’ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑏((𝑠 βˆͺ 𝑑) = 𝑏 β†’ ((π‘˜β€˜π‘ ) βˆͺ (π‘˜β€˜π‘‘)) = 𝑏))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 395  βˆ€wal 1532   = wceq 1534  βˆƒwex 1774   ∈ wcel 2099   β‰  wne 2935  βˆ€wral 3056  βˆƒwrex 3065  Vcvv 3469   βˆ– cdif 3941   βˆͺ cun 3942   ∩ cin 3943   βŠ† wss 3944  βˆ…c0 4318  π’« cpw 4598  {csn 4624   ↦ cmpt 5225  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7414  1oc1o 8473   ↑m cmap 8836
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-pow 5359  ax-pr 5423  ax-un 7734
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  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-ne 2936  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  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-rn 5683  df-res 5684  df-ima 5685  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550  df-ov 7417  df-oprab 7418  df-mpo 7419  df-1o 8480  df-map 8838
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator