Theorem clsk3nimkb 45039

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.

Step	Hyp	Ref	Expression
1		1oex 8486	. . . . 5 ⊢ 1o ∈ V
2		1n0 8495	. . . . . 6 ⊢ 1o ≠ ∅
3		nelsn 4627	. . . . . 6 ⊢ (1o ≠ ∅ → ¬ 1o ∈ {∅})
4	2, 3	ax-mp 5	. . . . 5 ⊢ ¬ 1o ∈ {∅}
5		eldif 3909	. . . . . 6 ⊢ (1o ∈ (V ∖ {∅}) ↔ (1o ∈ V ∧ ¬ 1o ∈ {∅}))
6		ne0i 4287	. . . . . 6 ⊢ (1o ∈ (V ∖ {∅}) → (V ∖ {∅}) ≠ ∅)
7	5, 6	sylbir 238	. . . . 5 ⊢ ((1o ∈ V ∧ ¬ 1o ∈ {∅}) → (V ∖ {∅}) ≠ ∅)
8	1, 4, 7	mp2an 705	. . . 4 ⊢ (V ∖ {∅}) ≠ ∅
9		r19.2zb 4456	. . . 4 ⊢ ((V ∖ {∅}) ≠ ∅ ↔ (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))))
10	8, 9	mpbi 233	. . 3 ⊢ (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
11		rexex 3093	. . 3 ⊢ (∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ∃𝑏∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
12		rexanali 3117	. . . . 5 ⊢ (∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) ↔ ¬ ∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
13	12	exbii 1881	. . . 4 ⊢ (∃𝑏∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) ↔ ∃𝑏 ¬ ∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
14		exnal 1860	. . . 4 ⊢ (∃𝑏 ¬ ∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) ↔ ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
15	13, 14	sylbb 222	. . 3 ⊢ (∃𝑏∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
16	10, 11, 15	3syl 19	. 2 ⊢ (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
17		difelpw 5315	. . . . . 6 ⊢ (𝑏 ∈ (V ∖ {∅}) → (𝑏 ∖ 𝑥) ∈ 𝒫 𝑏)
18	17	adantr 486	. . . . 5 ⊢ ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑥 ∈ 𝒫 𝑏) → (𝑏 ∖ 𝑥) ∈ 𝒫 𝑏)
19	18	fmpttd 7115	. . . 4 ⊢ (𝑏 ∈ (V ∖ {∅}) → (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)):𝒫 𝑏⟶𝒫 𝑏)
20		pwexg 5340	. . . . 5 ⊢ (𝑏 ∈ (V ∖ {∅}) → 𝒫 𝑏 ∈ V)
21	20, 20	elmapd 8860	. . . 4 ⊢ (𝑏 ∈ (V ∖ {∅}) → ((𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)) ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↔ (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)):𝒫 𝑏⟶𝒫 𝑏))
22	19, 21	mpbird 260	. . 3 ⊢ (𝑏 ∈ (V ∖ {∅}) → (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)) ∈ (𝒫 𝑏 ↑m 𝒫 𝑏))
23		simpllr 788	. . . . . . . . 9 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)))
24		difeq2 4068	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑏 ∖ 𝑥) = (𝑏 ∖ 𝑧))
25	24	cbvmptv 5209	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑧))
26	23, 25	eqtrdi 2812	. . . . . . . 8 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑘 = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑧)))
27		difeq2 4068	. . . . . . . . 9 ⊢ (𝑧 = (𝑠 ∪ 𝑡) → (𝑏 ∖ 𝑧) = (𝑏 ∖ (𝑠 ∪ 𝑡)))
28	27	adantl 487	. . . . . . . 8 ⊢ (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = (𝑠 ∪ 𝑡)) → (𝑏 ∖ 𝑧) = (𝑏 ∖ (𝑠 ∪ 𝑡)))
29		simplll 787	. . . . . . . . 9 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑏 ∈ (V ∖ {∅}))
30		simplr 781	. . . . . . . . . . 11 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑠 ∈ 𝒫 𝑏)
31	30	elpwid 4566	. . . . . . . . . 10 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑠 ⊆ 𝑏)
32		simpr 490	. . . . . . . . . . 11 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑡 ∈ 𝒫 𝑏)
33	32	elpwid 4566	. . . . . . . . . 10 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑡 ⊆ 𝑏)
34	31, 33	unssd 4138	. . . . . . . . 9 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑠 ∪ 𝑡) ⊆ 𝑏)
35	29, 34	sselpwd 5290	. . . . . . . 8 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑠 ∪ 𝑡) ∈ 𝒫 𝑏)
36		vex 3455	. . . . . . . . . 10 ⊢ 𝑏 ∈ V
37	36	difexi 5292	. . . . . . . . 9 ⊢ (𝑏 ∖ (𝑠 ∪ 𝑡)) ∈ V
38	37	a1i 11	. . . . . . . 8 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏 ∖ (𝑠 ∪ 𝑡)) ∈ V)
39	26, 28, 35, 38	fvmptd 7001	. . . . . . 7 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘‘(𝑠 ∪ 𝑡)) = (𝑏 ∖ (𝑠 ∪ 𝑡)))
40		difeq2 4068	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑠 → (𝑏 ∖ 𝑧) = (𝑏 ∖ 𝑠))
41	40	adantl 487	. . . . . . . . . 10 ⊢ (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = 𝑠) → (𝑏 ∖ 𝑧) = (𝑏 ∖ 𝑠))
42	36	difexi 5292	. . . . . . . . . . 11 ⊢ (𝑏 ∖ 𝑠) ∈ V
43	42	a1i 11	. . . . . . . . . 10 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏 ∖ 𝑠) ∈ V)
44	26, 41, 30, 43	fvmptd 7001	. . . . . . . . 9 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘‘𝑠) = (𝑏 ∖ 𝑠))
45		difeq2 4068	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑡 → (𝑏 ∖ 𝑧) = (𝑏 ∖ 𝑡))
46	45	adantl 487	. . . . . . . . . 10 ⊢ (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = 𝑡) → (𝑏 ∖ 𝑧) = (𝑏 ∖ 𝑡))
47	36	difexi 5292	. . . . . . . . . . 11 ⊢ (𝑏 ∖ 𝑡) ∈ V
48	47	a1i 11	. . . . . . . . . 10 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏 ∖ 𝑡) ∈ V)
49	26, 46, 32, 48	fvmptd 7001	. . . . . . . . 9 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘‘𝑡) = (𝑏 ∖ 𝑡))
50	44, 49	uneq12d 4116	. . . . . . . 8 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = ((𝑏 ∖ 𝑠) ∪ (𝑏 ∖ 𝑡)))
51		difindi 4238	. . . . . . . 8 ⊢ (𝑏 ∖ (𝑠 ∩ 𝑡)) = ((𝑏 ∖ 𝑠) ∪ (𝑏 ∖ 𝑡))
52	50, 51	eqtr4di 2814	. . . . . . 7 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = (𝑏 ∖ (𝑠 ∩ 𝑡)))
53	39, 52	sseq12d 3964	. . . . . 6 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ (𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡))))
54	53	ralbidva 3184	. . . . 5 ⊢ (((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) → (∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡))))
55	54	ralbidva 3184	. . . 4 ⊢ ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) → (∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡))))
56	52	eqeq1d 2763	. . . . . . . 8 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏 ↔ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
57	56	imbi2d 343	. . . . . . 7 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏) ↔ ((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)))
58	57	ralbidva 3184	. . . . . 6 ⊢ (((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) → (∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏) ↔ ∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)))
59	58	ralbidva 3184	. . . . 5 ⊢ ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) → (∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏) ↔ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)))
60	59	notbid 321	. . . 4 ⊢ ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) → (¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏) ↔ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)))
61	55, 60	anbi12d 644	. . 3 ⊢ ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) → ((∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) ↔ (∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))))
62		pwidg 4577	. . . . . 6 ⊢ (𝑏 ∈ (V ∖ {∅}) → 𝑏 ∈ 𝒫 𝑏)
63		ssidd 3954	. . . . . 6 ⊢ (𝑏 ∈ (V ∖ {∅}) → 𝑏 ⊆ 𝑏)
64		eldifsnneq 4754	. . . . . 6 ⊢ (𝑏 ∈ (V ∖ {∅}) → ¬ 𝑏 = ∅)
65		uneq1 4108	. . . . . . . . . 10 ⊢ (𝑠 = 𝑏 → (𝑠 ∪ 𝑡) = (𝑏 ∪ 𝑡))
66	65	eqeq1d 2763	. . . . . . . . 9 ⊢ (𝑠 = 𝑏 → ((𝑠 ∪ 𝑡) = 𝑏 ↔ (𝑏 ∪ 𝑡) = 𝑏))
67		ssequn2 4135	. . . . . . . . 9 ⊢ (𝑡 ⊆ 𝑏 ↔ (𝑏 ∪ 𝑡) = 𝑏)
68	66, 67	bitr4di 292	. . . . . . . 8 ⊢ (𝑠 = 𝑏 → ((𝑠 ∪ 𝑡) = 𝑏 ↔ 𝑡 ⊆ 𝑏))
69		ineq1 4159	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑏 → (𝑠 ∩ 𝑡) = (𝑏 ∩ 𝑡))
70	69	difeq2d 4074	. . . . . . . . . 10 ⊢ (𝑠 = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = (𝑏 ∖ (𝑏 ∩ 𝑡)))
71	70	eqeq1d 2763	. . . . . . . . 9 ⊢ (𝑠 = 𝑏 → ((𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏 ↔ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏))
72	71	notbid 321	. . . . . . . 8 ⊢ (𝑠 = 𝑏 → (¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏 ↔ ¬ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏))
73	68, 72	anbi12d 644	. . . . . . 7 ⊢ (𝑠 = 𝑏 → (((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) ↔ (𝑡 ⊆ 𝑏 ∧ ¬ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏)))
74		sseq1 3956	. . . . . . . 8 ⊢ (𝑡 = 𝑏 → (𝑡 ⊆ 𝑏 ↔ 𝑏 ⊆ 𝑏))
75		ineq2 4160	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑏 → (𝑏 ∩ 𝑡) = (𝑏 ∩ 𝑏))
76		inidm 4172	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∩ 𝑏) = 𝑏
77	75, 76	eqtrdi 2812	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑏 → (𝑏 ∩ 𝑡) = 𝑏)
78	77	difeq2d 4074	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑏 → (𝑏 ∖ (𝑏 ∩ 𝑡)) = (𝑏 ∖ 𝑏))
79		difid 4325	. . . . . . . . . . . 12 ⊢ (𝑏 ∖ 𝑏) = ∅
80	78, 79	eqtrdi 2812	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑏 → (𝑏 ∖ (𝑏 ∩ 𝑡)) = ∅)
81	80	eqeq1d 2763	. . . . . . . . . 10 ⊢ (𝑡 = 𝑏 → ((𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏 ↔ ∅ = 𝑏))
82		eqcom 2768	. . . . . . . . . 10 ⊢ (∅ = 𝑏 ↔ 𝑏 = ∅)
83	81, 82	bitrdi 290	. . . . . . . . 9 ⊢ (𝑡 = 𝑏 → ((𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏 ↔ 𝑏 = ∅))
84	83	notbid 321	. . . . . . . 8 ⊢ (𝑡 = 𝑏 → (¬ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏 ↔ ¬ 𝑏 = ∅))
85	74, 84	anbi12d 644	. . . . . . 7 ⊢ (𝑡 = 𝑏 → ((𝑡 ⊆ 𝑏 ∧ ¬ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏) ↔ (𝑏 ⊆ 𝑏 ∧ ¬ 𝑏 = ∅)))
86	73, 85	rspc2ev 3589	. . . . . 6 ⊢ ((𝑏 ∈ 𝒫 𝑏 ∧ 𝑏 ∈ 𝒫 𝑏 ∧ (𝑏 ⊆ 𝑏 ∧ ¬ 𝑏 = ∅)) → ∃𝑠 ∈ 𝒫 𝑏∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
87	62, 62, 63, 64, 86	syl112anc 1401	. . . . 5 ⊢ (𝑏 ∈ (V ∖ {∅}) → ∃𝑠 ∈ 𝒫 𝑏∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
88		rexanali 3117	. . . . . . 7 ⊢ (∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) ↔ ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
89	88	rexbii 3110	. . . . . 6 ⊢ (∃𝑠 ∈ 𝒫 𝑏∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) ↔ ∃𝑠 ∈ 𝒫 𝑏 ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
90		rexnal 3115	. . . . . 6 ⊢ (∃𝑠 ∈ 𝒫 𝑏 ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) ↔ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
91	89, 90	sylbb 222	. . . . 5 ⊢ (∃𝑠 ∈ 𝒫 𝑏∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) → ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
92	87, 91	syl 18	. . . 4 ⊢ (𝑏 ∈ (V ∖ {∅}) → ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
93		inss1 4182	. . . . . . 7 ⊢ (𝑠 ∩ 𝑡) ⊆ 𝑠
94		ssun1 4124	. . . . . . 7 ⊢ 𝑠 ⊆ (𝑠 ∪ 𝑡)
95	93, 94	sstri 3940	. . . . . 6 ⊢ (𝑠 ∩ 𝑡) ⊆ (𝑠 ∪ 𝑡)
96		sscon 4090	. . . . . 6 ⊢ ((𝑠 ∩ 𝑡) ⊆ (𝑠 ∪ 𝑡) → (𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)))
97	95, 96	ax-mp 5	. . . . 5 ⊢ (𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡))
98	97	rgen2w 3082	. . . 4 ⊢ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡))
99	92, 98	jctil 529	. . 3 ⊢ (𝑏 ∈ (V ∖ {∅}) → (∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)))
100	22, 61, 99	rspcedvd 3579	. 2 ⊢ (𝑏 ∈ (V ∖ {∅}) → ∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
101	16, 100	mprg 3083	1 ⊢ ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  Vcvv 3451   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  𝒫 cpw 4557  {csn 4584   ↦ cmpt 5186  ⟶wf 6534  ‘cfv 6538  (class class class)co 7420  1_oc1o 8469   ↑_m cmap 8847

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-1o 8476  df-map 8849

This theorem is used by: (None)