Theorem clsk3nimkb 44794

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 8459	. . . . 5 ⊢ 1o ∈ V
2		1n0 8468	. . . . . 6 ⊢ 1o ≠ ∅
3		nelsn 4632	. . . . . 6 ⊢ (1o ≠ ∅ → ¬ 1o ∈ {∅})
4	2, 3	ax-mp 5	. . . . 5 ⊢ ¬ 1o ∈ {∅}
5		eldif 3915	. . . . . 6 ⊢ (1o ∈ (V ∖ {∅}) ↔ (1o ∈ V ∧ ¬ 1o ∈ {∅}))
6		ne0i 4294	. . . . . 6 ⊢ (1o ∈ (V ∖ {∅}) → (V ∖ {∅}) ≠ ∅)
7	5, 6	sylbir 238	. . . . 5 ⊢ ((1o ∈ V ∧ ¬ 1o ∈ {∅}) → (V ∖ {∅}) ≠ ∅)
8	1, 4, 7	mp2an 704	. . . 4 ⊢ (V ∖ {∅}) ≠ ∅
9		r19.2zb 4461	. . . 4 ⊢ ((V ∖ {∅}) ≠ ∅ ↔ (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))))
10	8, 9	mpbi 233	. . 3 ⊢ (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
11		rexex 3095	. . 3 ⊢ (∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ∃𝑏∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
12		rexanali 3119	. . . . 5 ⊢ (∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) ↔ ¬ ∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
13	12	exbii 1878	. . . 4 ⊢ (∃𝑏∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) ↔ ∃𝑏 ¬ ∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
14		exnal 1857	. . . 4 ⊢ (∃𝑏 ¬ ∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) ↔ ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
15	13, 14	sylbb 222	. . 3 ⊢ (∃𝑏∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
16	10, 11, 15	3syl 19	. 2 ⊢ (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
17		difelpw 5324	. . . . . 6 ⊢ (𝑏 ∈ (V ∖ {∅}) → (𝑏 ∖ 𝑥) ∈ 𝒫 𝑏)
18	17	adantr 485	. . . . 5 ⊢ ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑥 ∈ 𝒫 𝑏) → (𝑏 ∖ 𝑥) ∈ 𝒫 𝑏)
19	18	fmpttd 7110	. . . 4 ⊢ (𝑏 ∈ (V ∖ {∅}) → (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)):𝒫 𝑏⟶𝒫 𝑏)
20		pwexg 5349	. . . . 5 ⊢ (𝑏 ∈ (V ∖ {∅}) → 𝒫 𝑏 ∈ V)
21	20, 20	elmapd 8833	. . . 4 ⊢ (𝑏 ∈ (V ∖ {∅}) → ((𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)) ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↔ (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)):𝒫 𝑏⟶𝒫 𝑏))
22	19, 21	mpbird 260	. . 3 ⊢ (𝑏 ∈ (V ∖ {∅}) → (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)) ∈ (𝒫 𝑏 ↑m 𝒫 𝑏))
23		simpllr 787	. . . . . . . . 9 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)))
24		difeq2 4075	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑏 ∖ 𝑥) = (𝑏 ∖ 𝑧))
25	24	cbvmptv 5215	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑧))
26	23, 25	eqtrdi 2814	. . . . . . . 8 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑘 = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑧)))
27		difeq2 4075	. . . . . . . . 9 ⊢ (𝑧 = (𝑠 ∪ 𝑡) → (𝑏 ∖ 𝑧) = (𝑏 ∖ (𝑠 ∪ 𝑡)))
28	27	adantl 486	. . . . . . . 8 ⊢ (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = (𝑠 ∪ 𝑡)) → (𝑏 ∖ 𝑧) = (𝑏 ∖ (𝑠 ∪ 𝑡)))
29		simplll 786	. . . . . . . . 9 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑏 ∈ (V ∖ {∅}))
30		simplr 780	. . . . . . . . . . 11 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑠 ∈ 𝒫 𝑏)
31	30	elpwid 4571	. . . . . . . . . 10 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑠 ⊆ 𝑏)
32		simpr 489	. . . . . . . . . . 11 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑡 ∈ 𝒫 𝑏)
33	32	elpwid 4571	. . . . . . . . . 10 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑡 ⊆ 𝑏)
34	31, 33	unssd 4145	. . . . . . . . 9 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑠 ∪ 𝑡) ⊆ 𝑏)
35	29, 34	sselpwd 5299	. . . . . . . 8 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑠 ∪ 𝑡) ∈ 𝒫 𝑏)
36		vex 3459	. . . . . . . . . 10 ⊢ 𝑏 ∈ V
37	36	difexi 5301	. . . . . . . . 9 ⊢ (𝑏 ∖ (𝑠 ∪ 𝑡)) ∈ V
38	37	a1i 11	. . . . . . . 8 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏 ∖ (𝑠 ∪ 𝑡)) ∈ V)
39	26, 28, 35, 38	fvmptd 6997	. . . . . . 7 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘‘(𝑠 ∪ 𝑡)) = (𝑏 ∖ (𝑠 ∪ 𝑡)))
40		difeq2 4075	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑠 → (𝑏 ∖ 𝑧) = (𝑏 ∖ 𝑠))
41	40	adantl 486	. . . . . . . . . 10 ⊢ (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = 𝑠) → (𝑏 ∖ 𝑧) = (𝑏 ∖ 𝑠))
42	36	difexi 5301	. . . . . . . . . . 11 ⊢ (𝑏 ∖ 𝑠) ∈ V
43	42	a1i 11	. . . . . . . . . 10 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏 ∖ 𝑠) ∈ V)
44	26, 41, 30, 43	fvmptd 6997	. . . . . . . . 9 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘‘𝑠) = (𝑏 ∖ 𝑠))
45		difeq2 4075	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑡 → (𝑏 ∖ 𝑧) = (𝑏 ∖ 𝑡))
46	45	adantl 486	. . . . . . . . . 10 ⊢ (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = 𝑡) → (𝑏 ∖ 𝑧) = (𝑏 ∖ 𝑡))
47	36	difexi 5301	. . . . . . . . . . 11 ⊢ (𝑏 ∖ 𝑡) ∈ V
48	47	a1i 11	. . . . . . . . . 10 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏 ∖ 𝑡) ∈ V)
49	26, 46, 32, 48	fvmptd 6997	. . . . . . . . 9 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘‘𝑡) = (𝑏 ∖ 𝑡))
50	44, 49	uneq12d 4123	. . . . . . . 8 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = ((𝑏 ∖ 𝑠) ∪ (𝑏 ∖ 𝑡)))
51		difindi 4245	. . . . . . . 8 ⊢ (𝑏 ∖ (𝑠 ∩ 𝑡)) = ((𝑏 ∖ 𝑠) ∪ (𝑏 ∖ 𝑡))
52	50, 51	eqtr4di 2816	. . . . . . 7 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = (𝑏 ∖ (𝑠 ∩ 𝑡)))
53	39, 52	sseq12d 3970	. . . . . 6 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ (𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡))))
54	53	ralbidva 3186	. . . . 5 ⊢ (((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) → (∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡))))
55	54	ralbidva 3186	. . . 4 ⊢ ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) → (∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡))))
56	52	eqeq1d 2765	. . . . . . . 8 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏 ↔ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
57	56	imbi2d 343	. . . . . . 7 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏) ↔ ((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)))
58	57	ralbidva 3186	. . . . . 6 ⊢ (((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) → (∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏) ↔ ∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)))
59	58	ralbidva 3186	. . . . 5 ⊢ ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) → (∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏) ↔ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)))
60	59	notbid 321	. . . 4 ⊢ ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) → (¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏) ↔ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)))
61	55, 60	anbi12d 643	. . 3 ⊢ ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) → ((∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) ↔ (∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))))
62		pwidg 4582	. . . . . 6 ⊢ (𝑏 ∈ (V ∖ {∅}) → 𝑏 ∈ 𝒫 𝑏)
63		ssidd 3960	. . . . . 6 ⊢ (𝑏 ∈ (V ∖ {∅}) → 𝑏 ⊆ 𝑏)
64		eldifsnneq 4759	. . . . . 6 ⊢ (𝑏 ∈ (V ∖ {∅}) → ¬ 𝑏 = ∅)
65		uneq1 4115	. . . . . . . . . 10 ⊢ (𝑠 = 𝑏 → (𝑠 ∪ 𝑡) = (𝑏 ∪ 𝑡))
66	65	eqeq1d 2765	. . . . . . . . 9 ⊢ (𝑠 = 𝑏 → ((𝑠 ∪ 𝑡) = 𝑏 ↔ (𝑏 ∪ 𝑡) = 𝑏))
67		ssequn2 4142	. . . . . . . . 9 ⊢ (𝑡 ⊆ 𝑏 ↔ (𝑏 ∪ 𝑡) = 𝑏)
68	66, 67	bitr4di 292	. . . . . . . 8 ⊢ (𝑠 = 𝑏 → ((𝑠 ∪ 𝑡) = 𝑏 ↔ 𝑡 ⊆ 𝑏))
69		ineq1 4166	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑏 → (𝑠 ∩ 𝑡) = (𝑏 ∩ 𝑡))
70	69	difeq2d 4081	. . . . . . . . . 10 ⊢ (𝑠 = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = (𝑏 ∖ (𝑏 ∩ 𝑡)))
71	70	eqeq1d 2765	. . . . . . . . 9 ⊢ (𝑠 = 𝑏 → ((𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏 ↔ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏))
72	71	notbid 321	. . . . . . . 8 ⊢ (𝑠 = 𝑏 → (¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏 ↔ ¬ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏))
73	68, 72	anbi12d 643	. . . . . . 7 ⊢ (𝑠 = 𝑏 → (((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) ↔ (𝑡 ⊆ 𝑏 ∧ ¬ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏)))
74		sseq1 3962	. . . . . . . 8 ⊢ (𝑡 = 𝑏 → (𝑡 ⊆ 𝑏 ↔ 𝑏 ⊆ 𝑏))
75		ineq2 4167	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑏 → (𝑏 ∩ 𝑡) = (𝑏 ∩ 𝑏))
76		inidm 4179	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∩ 𝑏) = 𝑏
77	75, 76	eqtrdi 2814	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑏 → (𝑏 ∩ 𝑡) = 𝑏)
78	77	difeq2d 4081	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑏 → (𝑏 ∖ (𝑏 ∩ 𝑡)) = (𝑏 ∖ 𝑏))
79		difid 4332	. . . . . . . . . . . 12 ⊢ (𝑏 ∖ 𝑏) = ∅
80	78, 79	eqtrdi 2814	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑏 → (𝑏 ∖ (𝑏 ∩ 𝑡)) = ∅)
81	80	eqeq1d 2765	. . . . . . . . . 10 ⊢ (𝑡 = 𝑏 → ((𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏 ↔ ∅ = 𝑏))
82		eqcom 2770	. . . . . . . . . 10 ⊢ (∅ = 𝑏 ↔ 𝑏 = ∅)
83	81, 82	bitrdi 290	. . . . . . . . 9 ⊢ (𝑡 = 𝑏 → ((𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏 ↔ 𝑏 = ∅))
84	83	notbid 321	. . . . . . . 8 ⊢ (𝑡 = 𝑏 → (¬ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏 ↔ ¬ 𝑏 = ∅))
85	74, 84	anbi12d 643	. . . . . . 7 ⊢ (𝑡 = 𝑏 → ((𝑡 ⊆ 𝑏 ∧ ¬ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏) ↔ (𝑏 ⊆ 𝑏 ∧ ¬ 𝑏 = ∅)))
86	73, 85	rspc2ev 3594	. . . . . 6 ⊢ ((𝑏 ∈ 𝒫 𝑏 ∧ 𝑏 ∈ 𝒫 𝑏 ∧ (𝑏 ⊆ 𝑏 ∧ ¬ 𝑏 = ∅)) → ∃𝑠 ∈ 𝒫 𝑏∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
87	62, 62, 63, 64, 86	syl112anc 1401	. . . . 5 ⊢ (𝑏 ∈ (V ∖ {∅}) → ∃𝑠 ∈ 𝒫 𝑏∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
88		rexanali 3119	. . . . . . 7 ⊢ (∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) ↔ ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
89	88	rexbii 3112	. . . . . 6 ⊢ (∃𝑠 ∈ 𝒫 𝑏∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) ↔ ∃𝑠 ∈ 𝒫 𝑏 ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
90		rexnal 3117	. . . . . 6 ⊢ (∃𝑠 ∈ 𝒫 𝑏 ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) ↔ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
91	89, 90	sylbb 222	. . . . 5 ⊢ (∃𝑠 ∈ 𝒫 𝑏∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) → ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
92	87, 91	syl 18	. . . 4 ⊢ (𝑏 ∈ (V ∖ {∅}) → ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
93		inss1 4189	. . . . . . 7 ⊢ (𝑠 ∩ 𝑡) ⊆ 𝑠
94		ssun1 4131	. . . . . . 7 ⊢ 𝑠 ⊆ (𝑠 ∪ 𝑡)
95	93, 94	sstri 3946	. . . . . 6 ⊢ (𝑠 ∩ 𝑡) ⊆ (𝑠 ∪ 𝑡)
96		sscon 4097	. . . . . 6 ⊢ ((𝑠 ∩ 𝑡) ⊆ (𝑠 ∪ 𝑡) → (𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)))
97	95, 96	ax-mp 5	. . . . 5 ⊢ (𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡))
98	97	rgen2w 3084	. . . 4 ⊢ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡))
99	92, 98	jctil 528	. . 3 ⊢ (𝑏 ∈ (V ∖ {∅}) → (∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)))
100	22, 61, 99	rspcedvd 3583	. 2 ⊢ (𝑏 ∈ (V ∖ {∅}) → ∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
101	16, 100	mprg 3085	1 ⊢ ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 400  ∀wal 1568   = wceq 1570  ∃wex 1809   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  ∃wrex 3089  Vcvv 3455   ∖ cdif 3902   ∪ cun 3903   ∩ cin 3904   ⊆ wss 3905  ∅c0 4286  𝒫 cpw 4562  {csn 4589   ↦ cmpt 5192  ⟶wf 6532  ‘cfv 6536  (class class class)co 7410  1_oc1o 8442   ↑_m cmap 8820

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-1o 8449  df-map 8822

This theorem is used by: (None)