Theorem clsk3nimkb 41539

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 8280	. . . . 5 ⊢ 1o ∈ V
2		1n0 8286	. . . . . 6 ⊢ 1o ≠ ∅
3		nelsn 4598	. . . . . 6 ⊢ (1o ≠ ∅ → ¬ 1o ∈ {∅})
4	2, 3	ax-mp 5	. . . . 5 ⊢ ¬ 1o ∈ {∅}
5		eldif 3893	. . . . . 6 ⊢ (1o ∈ (V ∖ {∅}) ↔ (1o ∈ V ∧ ¬ 1o ∈ {∅}))
6		ne0i 4265	. . . . . 6 ⊢ (1o ∈ (V ∖ {∅}) → (V ∖ {∅}) ≠ ∅)
7	5, 6	sylbir 234	. . . . 5 ⊢ ((1o ∈ V ∧ ¬ 1o ∈ {∅}) → (V ∖ {∅}) ≠ ∅)
8	1, 4, 7	mp2an 688	. . . 4 ⊢ (V ∖ {∅}) ≠ ∅
9		r19.2zb 4423	. . . 4 ⊢ ((V ∖ {∅}) ≠ ∅ ↔ (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))))
10	8, 9	mpbi 229	. . 3 ⊢ (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
11		rexex 3167	. . 3 ⊢ (∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ∃𝑏∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
12		rexanali 3191	. . . . 5 ⊢ (∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) ↔ ¬ ∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
13	12	exbii 1851	. . . 4 ⊢ (∃𝑏∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) ↔ ∃𝑏 ¬ ∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
14		exnal 1830	. . . 4 ⊢ (∃𝑏 ¬ ∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) ↔ ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
15	13, 14	sylbb 218	. . 3 ⊢ (∃𝑏∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
16	10, 11, 15	3syl 18	. 2 ⊢ (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
17		difelpw 5269	. . . . . 6 ⊢ (𝑏 ∈ (V ∖ {∅}) → (𝑏 ∖ 𝑥) ∈ 𝒫 𝑏)
18	17	adantr 480	. . . . 5 ⊢ ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑥 ∈ 𝒫 𝑏) → (𝑏 ∖ 𝑥) ∈ 𝒫 𝑏)
19	18	fmpttd 6971	. . . 4 ⊢ (𝑏 ∈ (V ∖ {∅}) → (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)):𝒫 𝑏⟶𝒫 𝑏)
20		pwexg 5296	. . . . 5 ⊢ (𝑏 ∈ (V ∖ {∅}) → 𝒫 𝑏 ∈ V)
21	20, 20	elmapd 8587	. . . 4 ⊢ (𝑏 ∈ (V ∖ {∅}) → ((𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)) ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↔ (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)):𝒫 𝑏⟶𝒫 𝑏))
22	19, 21	mpbird 256	. . 3 ⊢ (𝑏 ∈ (V ∖ {∅}) → (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)) ∈ (𝒫 𝑏 ↑m 𝒫 𝑏))
23		simpllr 772	. . . . . . . . 9 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)))
24		difeq2 4047	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑏 ∖ 𝑥) = (𝑏 ∖ 𝑧))
25	24	cbvmptv 5183	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑧))
26	23, 25	eqtrdi 2795	. . . . . . . 8 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑘 = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑧)))
27		difeq2 4047	. . . . . . . . 9 ⊢ (𝑧 = (𝑠 ∪ 𝑡) → (𝑏 ∖ 𝑧) = (𝑏 ∖ (𝑠 ∪ 𝑡)))
28	27	adantl 481	. . . . . . . 8 ⊢ (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = (𝑠 ∪ 𝑡)) → (𝑏 ∖ 𝑧) = (𝑏 ∖ (𝑠 ∪ 𝑡)))
29		simplll 771	. . . . . . . . 9 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑏 ∈ (V ∖ {∅}))
30		simplr 765	. . . . . . . . . . 11 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑠 ∈ 𝒫 𝑏)
31	30	elpwid 4541	. . . . . . . . . 10 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑠 ⊆ 𝑏)
32		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑡 ∈ 𝒫 𝑏)
33	32	elpwid 4541	. . . . . . . . . 10 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑡 ⊆ 𝑏)
34	31, 33	unssd 4116	. . . . . . . . 9 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑠 ∪ 𝑡) ⊆ 𝑏)
35	29, 34	sselpwd 5245	. . . . . . . 8 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑠 ∪ 𝑡) ∈ 𝒫 𝑏)
36		vex 3426	. . . . . . . . . 10 ⊢ 𝑏 ∈ V
37	36	difexi 5247	. . . . . . . . 9 ⊢ (𝑏 ∖ (𝑠 ∪ 𝑡)) ∈ V
38	37	a1i 11	. . . . . . . 8 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏 ∖ (𝑠 ∪ 𝑡)) ∈ V)
39	26, 28, 35, 38	fvmptd 6864	. . . . . . 7 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘‘(𝑠 ∪ 𝑡)) = (𝑏 ∖ (𝑠 ∪ 𝑡)))
40		difeq2 4047	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑠 → (𝑏 ∖ 𝑧) = (𝑏 ∖ 𝑠))
41	40	adantl 481	. . . . . . . . . 10 ⊢ (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = 𝑠) → (𝑏 ∖ 𝑧) = (𝑏 ∖ 𝑠))
42	36	difexi 5247	. . . . . . . . . . 11 ⊢ (𝑏 ∖ 𝑠) ∈ V
43	42	a1i 11	. . . . . . . . . 10 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏 ∖ 𝑠) ∈ V)
44	26, 41, 30, 43	fvmptd 6864	. . . . . . . . 9 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘‘𝑠) = (𝑏 ∖ 𝑠))
45		difeq2 4047	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑡 → (𝑏 ∖ 𝑧) = (𝑏 ∖ 𝑡))
46	45	adantl 481	. . . . . . . . . 10 ⊢ (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = 𝑡) → (𝑏 ∖ 𝑧) = (𝑏 ∖ 𝑡))
47	36	difexi 5247	. . . . . . . . . . 11 ⊢ (𝑏 ∖ 𝑡) ∈ V
48	47	a1i 11	. . . . . . . . . 10 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏 ∖ 𝑡) ∈ V)
49	26, 46, 32, 48	fvmptd 6864	. . . . . . . . 9 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘‘𝑡) = (𝑏 ∖ 𝑡))
50	44, 49	uneq12d 4094	. . . . . . . 8 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = ((𝑏 ∖ 𝑠) ∪ (𝑏 ∖ 𝑡)))
51		difindi 4212	. . . . . . . 8 ⊢ (𝑏 ∖ (𝑠 ∩ 𝑡)) = ((𝑏 ∖ 𝑠) ∪ (𝑏 ∖ 𝑡))
52	50, 51	eqtr4di 2797	. . . . . . 7 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = (𝑏 ∖ (𝑠 ∩ 𝑡)))
53	39, 52	sseq12d 3950	. . . . . 6 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ (𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡))))
54	53	ralbidva 3119	. . . . 5 ⊢ (((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) → (∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡))))
55	54	ralbidva 3119	. . . 4 ⊢ ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) → (∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡))))
56	52	eqeq1d 2740	. . . . . . . 8 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏 ↔ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
57	56	imbi2d 340	. . . . . . 7 ⊢ ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏) ↔ ((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)))
58	57	ralbidva 3119	. . . . . 6 ⊢ (((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) → (∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏) ↔ ∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)))
59	58	ralbidva 3119	. . . . 5 ⊢ ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) → (∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏) ↔ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)))
60	59	notbid 317	. . . 4 ⊢ ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) → (¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏) ↔ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)))
61	55, 60	anbi12d 630	. . 3 ⊢ ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) → ((∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) ↔ (∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))))
62		pwidg 4552	. . . . . 6 ⊢ (𝑏 ∈ (V ∖ {∅}) → 𝑏 ∈ 𝒫 𝑏)
63		ssidd 3940	. . . . . 6 ⊢ (𝑏 ∈ (V ∖ {∅}) → 𝑏 ⊆ 𝑏)
64		eldifsnneq 4721	. . . . . 6 ⊢ (𝑏 ∈ (V ∖ {∅}) → ¬ 𝑏 = ∅)
65		uneq1 4086	. . . . . . . . . 10 ⊢ (𝑠 = 𝑏 → (𝑠 ∪ 𝑡) = (𝑏 ∪ 𝑡))
66	65	eqeq1d 2740	. . . . . . . . 9 ⊢ (𝑠 = 𝑏 → ((𝑠 ∪ 𝑡) = 𝑏 ↔ (𝑏 ∪ 𝑡) = 𝑏))
67		ssequn2 4113	. . . . . . . . 9 ⊢ (𝑡 ⊆ 𝑏 ↔ (𝑏 ∪ 𝑡) = 𝑏)
68	66, 67	bitr4di 288	. . . . . . . 8 ⊢ (𝑠 = 𝑏 → ((𝑠 ∪ 𝑡) = 𝑏 ↔ 𝑡 ⊆ 𝑏))
69		ineq1 4136	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑏 → (𝑠 ∩ 𝑡) = (𝑏 ∩ 𝑡))
70	69	difeq2d 4053	. . . . . . . . . 10 ⊢ (𝑠 = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = (𝑏 ∖ (𝑏 ∩ 𝑡)))
71	70	eqeq1d 2740	. . . . . . . . 9 ⊢ (𝑠 = 𝑏 → ((𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏 ↔ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏))
72	71	notbid 317	. . . . . . . 8 ⊢ (𝑠 = 𝑏 → (¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏 ↔ ¬ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏))
73	68, 72	anbi12d 630	. . . . . . 7 ⊢ (𝑠 = 𝑏 → (((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) ↔ (𝑡 ⊆ 𝑏 ∧ ¬ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏)))
74		sseq1 3942	. . . . . . . 8 ⊢ (𝑡 = 𝑏 → (𝑡 ⊆ 𝑏 ↔ 𝑏 ⊆ 𝑏))
75		ineq2 4137	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑏 → (𝑏 ∩ 𝑡) = (𝑏 ∩ 𝑏))
76		inidm 4149	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∩ 𝑏) = 𝑏
77	75, 76	eqtrdi 2795	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑏 → (𝑏 ∩ 𝑡) = 𝑏)
78	77	difeq2d 4053	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑏 → (𝑏 ∖ (𝑏 ∩ 𝑡)) = (𝑏 ∖ 𝑏))
79		difid 4301	. . . . . . . . . . . 12 ⊢ (𝑏 ∖ 𝑏) = ∅
80	78, 79	eqtrdi 2795	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑏 → (𝑏 ∖ (𝑏 ∩ 𝑡)) = ∅)
81	80	eqeq1d 2740	. . . . . . . . . 10 ⊢ (𝑡 = 𝑏 → ((𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏 ↔ ∅ = 𝑏))
82		eqcom 2745	. . . . . . . . . 10 ⊢ (∅ = 𝑏 ↔ 𝑏 = ∅)
83	81, 82	bitrdi 286	. . . . . . . . 9 ⊢ (𝑡 = 𝑏 → ((𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏 ↔ 𝑏 = ∅))
84	83	notbid 317	. . . . . . . 8 ⊢ (𝑡 = 𝑏 → (¬ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏 ↔ ¬ 𝑏 = ∅))
85	74, 84	anbi12d 630	. . . . . . 7 ⊢ (𝑡 = 𝑏 → ((𝑡 ⊆ 𝑏 ∧ ¬ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏) ↔ (𝑏 ⊆ 𝑏 ∧ ¬ 𝑏 = ∅)))
86	73, 85	rspc2ev 3564	. . . . . 6 ⊢ ((𝑏 ∈ 𝒫 𝑏 ∧ 𝑏 ∈ 𝒫 𝑏 ∧ (𝑏 ⊆ 𝑏 ∧ ¬ 𝑏 = ∅)) → ∃𝑠 ∈ 𝒫 𝑏∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
87	62, 62, 63, 64, 86	syl112anc 1372	. . . . 5 ⊢ (𝑏 ∈ (V ∖ {∅}) → ∃𝑠 ∈ 𝒫 𝑏∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
88		rexanali 3191	. . . . . . 7 ⊢ (∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) ↔ ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
89	88	rexbii 3177	. . . . . 6 ⊢ (∃𝑠 ∈ 𝒫 𝑏∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) ↔ ∃𝑠 ∈ 𝒫 𝑏 ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
90		rexnal 3165	. . . . . 6 ⊢ (∃𝑠 ∈ 𝒫 𝑏 ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) ↔ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
91	89, 90	sylbb 218	. . . . 5 ⊢ (∃𝑠 ∈ 𝒫 𝑏∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) → ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
92	87, 91	syl 17	. . . 4 ⊢ (𝑏 ∈ (V ∖ {∅}) → ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))
93		inss1 4159	. . . . . . 7 ⊢ (𝑠 ∩ 𝑡) ⊆ 𝑠
94		ssun1 4102	. . . . . . 7 ⊢ 𝑠 ⊆ (𝑠 ∪ 𝑡)
95	93, 94	sstri 3926	. . . . . 6 ⊢ (𝑠 ∩ 𝑡) ⊆ (𝑠 ∪ 𝑡)
96		sscon 4069	. . . . . 6 ⊢ ((𝑠 ∩ 𝑡) ⊆ (𝑠 ∪ 𝑡) → (𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)))
97	95, 96	ax-mp 5	. . . . 5 ⊢ (𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡))
98	97	rgen2w 3076	. . . 4 ⊢ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡))
99	92, 98	jctil 519	. . 3 ⊢ (𝑏 ∈ (V ∖ {∅}) → (∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)))
100	22, 61, 99	rspcedvd 3555	. 2 ⊢ (𝑏 ∈ (V ∖ {∅}) → ∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))
101	16, 100	mprg 3077	1 ⊢ ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395  ∀wal 1537   = wceq 1539  ∃wex 1783   ∈ wcel 2108   ≠ wne 2942  ∀wral 3063  ∃wrex 3064  Vcvv 3422   ∖ cdif 3880   ∪ cun 3881   ∩ cin 3882   ⊆ wss 3883  ∅c0 4253  𝒫 cpw 4530  {csn 4558   ↦ cmpt 5153  ⟶wf 6414  ‘cfv 6418  (class class class)co 7255  1_oc1o 8260   ↑_m cmap 8573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-1o 8267  df-map 8575

This theorem is referenced by: (None)