clsk3nimkb

Description: If the base set is not empty, axiom K3 does not imply KB. A concrete example with a pseudo-closure function of k = ( x e. ~P b |-> ( b \ x ) ) is given. (Contributed by RP, 16-Jun-2021)

		Ref	Expression
	Assertion	clsk3nimkb	⊢ ¬ ∀ 𝑏 ∀ 𝑘 ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) → ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) )

Proof

Step	Hyp	Ref	Expression
1		1oex	⊢ 1_o ∈ V
2		1n0	⊢ 1_o ≠ ∅
3		nelsn	⊢ ( 1_o ≠ ∅ → ¬ 1_o ∈ { ∅ } )
4	2 3	ax-mp	⊢ ¬ 1_o ∈ { ∅ }
5		eldif	⊢ ( 1_o ∈ ( V ∖ { ∅ } ) ↔ ( 1_o ∈ V ∧ ¬ 1_o ∈ { ∅ } ) )
6		ne0i	⊢ ( 1_o ∈ ( V ∖ { ∅ } ) → ( V ∖ { ∅ } ) ≠ ∅ )
7	5 6	sylbir	⊢ ( ( 1_o ∈ V ∧ ¬ 1_o ∈ { ∅ } ) → ( V ∖ { ∅ } ) ≠ ∅ )
8	1 4 7	mp2an	⊢ ( V ∖ { ∅ } ) ≠ ∅
9		r19.2zb	⊢ ( ( V ∖ { ∅ } ) ≠ ∅ ↔ ( ∀ 𝑏 ∈ ( V ∖ { ∅ } ) ∃ 𝑘 ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) ∧ ¬ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ) → ∃ 𝑏 ∈ ( V ∖ { ∅ } ) ∃ 𝑘 ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) ∧ ¬ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ) ) )
10	8 9	mpbi	⊢ ( ∀ 𝑏 ∈ ( V ∖ { ∅ } ) ∃ 𝑘 ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) ∧ ¬ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ) → ∃ 𝑏 ∈ ( V ∖ { ∅ } ) ∃ 𝑘 ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) ∧ ¬ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ) )
11		rexex	⊢ ( ∃ 𝑏 ∈ ( V ∖ { ∅ } ) ∃ 𝑘 ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) ∧ ¬ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ) → ∃ 𝑏 ∃ 𝑘 ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) ∧ ¬ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ) )
12		rexanali	⊢ ( ∃ 𝑘 ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) ∧ ¬ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ) ↔ ¬ ∀ 𝑘 ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) → ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ) )
13	12	exbii	⊢ ( ∃ 𝑏 ∃ 𝑘 ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) ∧ ¬ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ) ↔ ∃ 𝑏 ¬ ∀ 𝑘 ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) → ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ) )
14		exnal	⊢ ( ∃ 𝑏 ¬ ∀ 𝑘 ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) → ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ) ↔ ¬ ∀ 𝑏 ∀ 𝑘 ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) → ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ) )
15	13 14	sylbb	⊢ ( ∃ 𝑏 ∃ 𝑘 ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) ∧ ¬ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ) → ¬ ∀ 𝑏 ∀ 𝑘 ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) → ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ) )
16	10 11 15	3syl	⊢ ( ∀ 𝑏 ∈ ( V ∖ { ∅ } ) ∃ 𝑘 ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) ∧ ¬ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ) → ¬ ∀ 𝑏 ∀ 𝑘 ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) → ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ) )
17		difelpw	⊢ ( 𝑏 ∈ ( V ∖ { ∅ } ) → ( 𝑏 ∖ 𝑥 ) ∈ 𝒫 𝑏 )
18	17	adantr	⊢ ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑥 ∈ 𝒫 𝑏 ) → ( 𝑏 ∖ 𝑥 ) ∈ 𝒫 𝑏 )
19	18	fmpttd	⊢ ( 𝑏 ∈ ( V ∖ { ∅ } ) → ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) : 𝒫 𝑏 ⟶ 𝒫 𝑏 )
20		pwexg	⊢ ( 𝑏 ∈ ( V ∖ { ∅ } ) → 𝒫 𝑏 ∈ V )
21	20 20	elmapd	⊢ ( 𝑏 ∈ ( V ∖ { ∅ } ) → ( ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) ↔ ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) : 𝒫 𝑏 ⟶ 𝒫 𝑏 ) )
22	19 21	mpbird	⊢ ( 𝑏 ∈ ( V ∖ { ∅ } ) → ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) )
23		simpllr	⊢ ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) → 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) )
24		difeq2	⊢ ( 𝑥 = 𝑧 → ( 𝑏 ∖ 𝑥 ) = ( 𝑏 ∖ 𝑧 ) )
25	24	cbvmptv	⊢ ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) = ( 𝑧 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑧 ) )
26	23 25	eqtrdi	⊢ ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) → 𝑘 = ( 𝑧 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑧 ) ) )
27		difeq2	⊢ ( 𝑧 = ( 𝑠 ∪ 𝑡 ) → ( 𝑏 ∖ 𝑧 ) = ( 𝑏 ∖ ( 𝑠 ∪ 𝑡 ) ) )
28	27	adantl	⊢ ( ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) ∧ 𝑧 = ( 𝑠 ∪ 𝑡 ) ) → ( 𝑏 ∖ 𝑧 ) = ( 𝑏 ∖ ( 𝑠 ∪ 𝑡 ) ) )
29		simplll	⊢ ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) → 𝑏 ∈ ( V ∖ { ∅ } ) )
30		simplr	⊢ ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) → 𝑠 ∈ 𝒫 𝑏 )
31	30	elpwid	⊢ ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) → 𝑠 ⊆ 𝑏 )
32		simpr	⊢ ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) → 𝑡 ∈ 𝒫 𝑏 )
33	32	elpwid	⊢ ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) → 𝑡 ⊆ 𝑏 )
34	31 33	unssd	⊢ ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) → ( 𝑠 ∪ 𝑡 ) ⊆ 𝑏 )
35	29 34	sselpwd	⊢ ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) → ( 𝑠 ∪ 𝑡 ) ∈ 𝒫 𝑏 )
36		vex	⊢ 𝑏 ∈ V
37	36	difexi	⊢ ( 𝑏 ∖ ( 𝑠 ∪ 𝑡 ) ) ∈ V
38	37	a1i	⊢ ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) → ( 𝑏 ∖ ( 𝑠 ∪ 𝑡 ) ) ∈ V )
39	26 28 35 38	fvmptd	⊢ ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) → ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) = ( 𝑏 ∖ ( 𝑠 ∪ 𝑡 ) ) )
40		difeq2	⊢ ( 𝑧 = 𝑠 → ( 𝑏 ∖ 𝑧 ) = ( 𝑏 ∖ 𝑠 ) )
41	40	adantl	⊢ ( ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) ∧ 𝑧 = 𝑠 ) → ( 𝑏 ∖ 𝑧 ) = ( 𝑏 ∖ 𝑠 ) )
42	36	difexi	⊢ ( 𝑏 ∖ 𝑠 ) ∈ V
43	42	a1i	⊢ ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) → ( 𝑏 ∖ 𝑠 ) ∈ V )
44	26 41 30 43	fvmptd	⊢ ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) → ( 𝑘 ‘ 𝑠 ) = ( 𝑏 ∖ 𝑠 ) )
45		difeq2	⊢ ( 𝑧 = 𝑡 → ( 𝑏 ∖ 𝑧 ) = ( 𝑏 ∖ 𝑡 ) )
46	45	adantl	⊢ ( ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) ∧ 𝑧 = 𝑡 ) → ( 𝑏 ∖ 𝑧 ) = ( 𝑏 ∖ 𝑡 ) )
47	36	difexi	⊢ ( 𝑏 ∖ 𝑡 ) ∈ V
48	47	a1i	⊢ ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) → ( 𝑏 ∖ 𝑡 ) ∈ V )
49	26 46 32 48	fvmptd	⊢ ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) → ( 𝑘 ‘ 𝑡 ) = ( 𝑏 ∖ 𝑡 ) )
50	44 49	uneq12d	⊢ ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = ( ( 𝑏 ∖ 𝑠 ) ∪ ( 𝑏 ∖ 𝑡 ) ) )
51		difindi	⊢ ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = ( ( 𝑏 ∖ 𝑠 ) ∪ ( 𝑏 ∖ 𝑡 ) )
52	50 51	eqtr4di	⊢ ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) )
53	39 52	sseq12d	⊢ ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) → ( ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) ↔ ( 𝑏 ∖ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) ) )
54	53	ralbidva	⊢ ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) → ( ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) ↔ ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑏 ∖ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) ) )
55	54	ralbidva	⊢ ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) → ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑏 ∖ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) ) )
56	52	eqeq1d	⊢ ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) → ( ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ↔ ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ) )
57	56	imbi2d	⊢ ( ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) ∧ 𝑡 ∈ 𝒫 𝑏 ) → ( ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ↔ ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ) ) )
58	57	ralbidva	⊢ ( ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑏 ) → ( ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ↔ ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ) ) )
59	58	ralbidva	⊢ ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) → ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ↔ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ) ) )
60	59	notbid	⊢ ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) → ( ¬ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ↔ ¬ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ) ) )
61	55 60	anbi12d	⊢ ( ( 𝑏 ∈ ( V ∖ { ∅ } ) ∧ 𝑘 = ( 𝑥 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ 𝑥 ) ) ) → ( ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) ∧ ¬ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ) ↔ ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑏 ∖ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) ∧ ¬ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ) ) ) )
62		pwidg	⊢ ( 𝑏 ∈ ( V ∖ { ∅ } ) → 𝑏 ∈ 𝒫 𝑏 )
63		ssidd	⊢ ( 𝑏 ∈ ( V ∖ { ∅ } ) → 𝑏 ⊆ 𝑏 )
64		eldifsnneq	⊢ ( 𝑏 ∈ ( V ∖ { ∅ } ) → ¬ 𝑏 = ∅ )
65		uneq1	⊢ ( 𝑠 = 𝑏 → ( 𝑠 ∪ 𝑡 ) = ( 𝑏 ∪ 𝑡 ) )
66	65	eqeq1d	⊢ ( 𝑠 = 𝑏 → ( ( 𝑠 ∪ 𝑡 ) = 𝑏 ↔ ( 𝑏 ∪ 𝑡 ) = 𝑏 ) )
67		ssequn2	⊢ ( 𝑡 ⊆ 𝑏 ↔ ( 𝑏 ∪ 𝑡 ) = 𝑏 )
68	66 67	bitr4di	⊢ ( 𝑠 = 𝑏 → ( ( 𝑠 ∪ 𝑡 ) = 𝑏 ↔ 𝑡 ⊆ 𝑏 ) )
69		ineq1	⊢ ( 𝑠 = 𝑏 → ( 𝑠 ∩ 𝑡 ) = ( 𝑏 ∩ 𝑡 ) )
70	69	difeq2d	⊢ ( 𝑠 = 𝑏 → ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = ( 𝑏 ∖ ( 𝑏 ∩ 𝑡 ) ) )
71	70	eqeq1d	⊢ ( 𝑠 = 𝑏 → ( ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ↔ ( 𝑏 ∖ ( 𝑏 ∩ 𝑡 ) ) = 𝑏 ) )
72	71	notbid	⊢ ( 𝑠 = 𝑏 → ( ¬ ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ↔ ¬ ( 𝑏 ∖ ( 𝑏 ∩ 𝑡 ) ) = 𝑏 ) )
73	68 72	anbi12d	⊢ ( 𝑠 = 𝑏 → ( ( ( 𝑠 ∪ 𝑡 ) = 𝑏 ∧ ¬ ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ) ↔ ( 𝑡 ⊆ 𝑏 ∧ ¬ ( 𝑏 ∖ ( 𝑏 ∩ 𝑡 ) ) = 𝑏 ) ) )
74		sseq1	⊢ ( 𝑡 = 𝑏 → ( 𝑡 ⊆ 𝑏 ↔ 𝑏 ⊆ 𝑏 ) )
75		ineq2	⊢ ( 𝑡 = 𝑏 → ( 𝑏 ∩ 𝑡 ) = ( 𝑏 ∩ 𝑏 ) )
76		inidm	⊢ ( 𝑏 ∩ 𝑏 ) = 𝑏
77	75 76	eqtrdi	⊢ ( 𝑡 = 𝑏 → ( 𝑏 ∩ 𝑡 ) = 𝑏 )
78	77	difeq2d	⊢ ( 𝑡 = 𝑏 → ( 𝑏 ∖ ( 𝑏 ∩ 𝑡 ) ) = ( 𝑏 ∖ 𝑏 ) )
79		difid	⊢ ( 𝑏 ∖ 𝑏 ) = ∅
80	78 79	eqtrdi	⊢ ( 𝑡 = 𝑏 → ( 𝑏 ∖ ( 𝑏 ∩ 𝑡 ) ) = ∅ )
81	80	eqeq1d	⊢ ( 𝑡 = 𝑏 → ( ( 𝑏 ∖ ( 𝑏 ∩ 𝑡 ) ) = 𝑏 ↔ ∅ = 𝑏 ) )
82		eqcom	⊢ ( ∅ = 𝑏 ↔ 𝑏 = ∅ )
83	81 82	bitrdi	⊢ ( 𝑡 = 𝑏 → ( ( 𝑏 ∖ ( 𝑏 ∩ 𝑡 ) ) = 𝑏 ↔ 𝑏 = ∅ ) )
84	83	notbid	⊢ ( 𝑡 = 𝑏 → ( ¬ ( 𝑏 ∖ ( 𝑏 ∩ 𝑡 ) ) = 𝑏 ↔ ¬ 𝑏 = ∅ ) )
85	74 84	anbi12d	⊢ ( 𝑡 = 𝑏 → ( ( 𝑡 ⊆ 𝑏 ∧ ¬ ( 𝑏 ∖ ( 𝑏 ∩ 𝑡 ) ) = 𝑏 ) ↔ ( 𝑏 ⊆ 𝑏 ∧ ¬ 𝑏 = ∅ ) ) )
86	73 85	rspc2ev	⊢ ( ( 𝑏 ∈ 𝒫 𝑏 ∧ 𝑏 ∈ 𝒫 𝑏 ∧ ( 𝑏 ⊆ 𝑏 ∧ ¬ 𝑏 = ∅ ) ) → ∃ 𝑠 ∈ 𝒫 𝑏 ∃ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 ∧ ¬ ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ) )
87	62 62 63 64 86	syl112anc	⊢ ( 𝑏 ∈ ( V ∖ { ∅ } ) → ∃ 𝑠 ∈ 𝒫 𝑏 ∃ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 ∧ ¬ ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ) )
88		rexanali	⊢ ( ∃ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 ∧ ¬ ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ) ↔ ¬ ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ) )
89	88	rexbii	⊢ ( ∃ 𝑠 ∈ 𝒫 𝑏 ∃ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 ∧ ¬ ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ) ↔ ∃ 𝑠 ∈ 𝒫 𝑏 ¬ ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ) )
90		rexnal	⊢ ( ∃ 𝑠 ∈ 𝒫 𝑏 ¬ ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ) ↔ ¬ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ) )
91	89 90	sylbb	⊢ ( ∃ 𝑠 ∈ 𝒫 𝑏 ∃ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 ∧ ¬ ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ) → ¬ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ) )
92	87 91	syl	⊢ ( 𝑏 ∈ ( V ∖ { ∅ } ) → ¬ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ) )
93		inss1	⊢ ( 𝑠 ∩ 𝑡 ) ⊆ 𝑠
94		ssun1	⊢ 𝑠 ⊆ ( 𝑠 ∪ 𝑡 )
95	93 94	sstri	⊢ ( 𝑠 ∩ 𝑡 ) ⊆ ( 𝑠 ∪ 𝑡 )
96		sscon	⊢ ( ( 𝑠 ∩ 𝑡 ) ⊆ ( 𝑠 ∪ 𝑡 ) → ( 𝑏 ∖ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) )
97	95 96	ax-mp	⊢ ( 𝑏 ∖ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) )
98	97	rgen2w	⊢ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑏 ∖ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) )
99	92 98	jctil	⊢ ( 𝑏 ∈ ( V ∖ { ∅ } ) → ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑏 ∖ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) ∧ ¬ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( 𝑏 ∖ ( 𝑠 ∩ 𝑡 ) ) = 𝑏 ) ) )
100	22 61 99	rspcedvd	⊢ ( 𝑏 ∈ ( V ∖ { ∅ } ) → ∃ 𝑘 ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) ∧ ¬ ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) ) )
101	16 100	mprg	⊢ ¬ ∀ 𝑏 ∀ 𝑘 ∈ ( 𝒫 𝑏 ↑_m 𝒫 𝑏 ) ( ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( 𝑘 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) → ∀ 𝑠 ∈ 𝒫 𝑏 ∀ 𝑡 ∈ 𝒫 𝑏 ( ( 𝑠 ∪ 𝑡 ) = 𝑏 → ( ( 𝑘 ‘ 𝑠 ) ∪ ( 𝑘 ‘ 𝑡 ) ) = 𝑏 ) )

Metamath Proof Explorer

Theorem clsk3nimkb

Proof