Theorem canth4

Description: An "effective" form of Cantor's theorem canth . For any function F from the powerset of A to A , there are two definable sets B and C which witness non-injectivity of F . Corollary 1.3 of KanamoriPincus p. 416. (Contributed by Mario Carneiro, 18-May-2015)

	Ref	Expression
Hypotheses	canth4.1	⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) }
	canth4.2	⊢ 𝐵 = ∪ dom 𝑊
	canth4.3	⊢ 𝐶 = ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐹 ‘ 𝐵 ) } )
Assertion	canth4	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → ( 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊊ 𝐵 ∧ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		canth4.1	⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) }
2		canth4.2	⊢ 𝐵 = ∪ dom 𝑊
3		canth4.3	⊢ 𝐶 = ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐹 ‘ 𝐵 ) } )
4		eqid	⊢ 𝐵 = 𝐵
5		eqid	⊢ ( 𝑊 ‘ 𝐵 ) = ( 𝑊 ‘ 𝐵 )
6	4 5	pm3.2i	⊢ ( 𝐵 = 𝐵 ∧ ( 𝑊 ‘ 𝐵 ) = ( 𝑊 ‘ 𝐵 ) )
7		simp1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → 𝐴 ∈ 𝑉 )
8		simpl2	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ dom card ) ) → 𝐹 : 𝐷 ⟶ 𝐴 )
9		simp3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 )
10	9	sselda	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ dom card ) ) → 𝑥 ∈ 𝐷 )
11	8 10	ffvelcdmd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ dom card ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 )
12	1 7 11 2	fpwwe	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → ( ( 𝐵 𝑊 ( 𝑊 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐵 ) ↔ ( 𝐵 = 𝐵 ∧ ( 𝑊 ‘ 𝐵 ) = ( 𝑊 ‘ 𝐵 ) ) ) )
13	6 12	mpbiri	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → ( 𝐵 𝑊 ( 𝑊 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐵 ) )
14	13	simpld	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → 𝐵 𝑊 ( 𝑊 ‘ 𝐵 ) )
15	1 7	fpwwelem	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → ( 𝐵 𝑊 ( 𝑊 ‘ 𝐵 ) ↔ ( ( 𝐵 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝐵 ) ⊆ ( 𝐵 × 𝐵 ) ) ∧ ( ( 𝑊 ‘ 𝐵 ) We 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( ◡ ( 𝑊 ‘ 𝐵 ) “ { 𝑦 } ) ) = 𝑦 ) ) ) )
16	14 15	mpbid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → ( ( 𝐵 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝐵 ) ⊆ ( 𝐵 × 𝐵 ) ) ∧ ( ( 𝑊 ‘ 𝐵 ) We 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( ◡ ( 𝑊 ‘ 𝐵 ) “ { 𝑦 } ) ) = 𝑦 ) ) )
17	16	simpld	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → ( 𝐵 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝐵 ) ⊆ ( 𝐵 × 𝐵 ) ) )
18	17	simpld	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → 𝐵 ⊆ 𝐴 )
19		cnvimass	⊢ ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐹 ‘ 𝐵 ) } ) ⊆ dom ( 𝑊 ‘ 𝐵 )
20	3 19	eqsstri	⊢ 𝐶 ⊆ dom ( 𝑊 ‘ 𝐵 )
21	17	simprd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → ( 𝑊 ‘ 𝐵 ) ⊆ ( 𝐵 × 𝐵 ) )
22		dmss	⊢ ( ( 𝑊 ‘ 𝐵 ) ⊆ ( 𝐵 × 𝐵 ) → dom ( 𝑊 ‘ 𝐵 ) ⊆ dom ( 𝐵 × 𝐵 ) )
23	21 22	syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → dom ( 𝑊 ‘ 𝐵 ) ⊆ dom ( 𝐵 × 𝐵 ) )
24		dmxpid	⊢ dom ( 𝐵 × 𝐵 ) = 𝐵
25	23 24	sseqtrdi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → dom ( 𝑊 ‘ 𝐵 ) ⊆ 𝐵 )
26	20 25	sstrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → 𝐶 ⊆ 𝐵 )
27	13	simprd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → ( 𝐹 ‘ 𝐵 ) ∈ 𝐵 )
28	16	simprd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → ( ( 𝑊 ‘ 𝐵 ) We 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( ◡ ( 𝑊 ‘ 𝐵 ) “ { 𝑦 } ) ) = 𝑦 ) )
29	28	simpld	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → ( 𝑊 ‘ 𝐵 ) We 𝐵 )
30		weso	⊢ ( ( 𝑊 ‘ 𝐵 ) We 𝐵 → ( 𝑊 ‘ 𝐵 ) Or 𝐵 )
31	29 30	syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → ( 𝑊 ‘ 𝐵 ) Or 𝐵 )
32		sonr	⊢ ( ( ( 𝑊 ‘ 𝐵 ) Or 𝐵 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐵 ) → ¬ ( 𝐹 ‘ 𝐵 ) ( 𝑊 ‘ 𝐵 ) ( 𝐹 ‘ 𝐵 ) )
33	31 27 32	syl2anc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → ¬ ( 𝐹 ‘ 𝐵 ) ( 𝑊 ‘ 𝐵 ) ( 𝐹 ‘ 𝐵 ) )
34	3	eleq2i	⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ↔ ( 𝐹 ‘ 𝐵 ) ∈ ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐹 ‘ 𝐵 ) } ) )
35		fvex	⊢ ( 𝐹 ‘ 𝐵 ) ∈ V
36	35	eliniseg	⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ V → ( ( 𝐹 ‘ 𝐵 ) ∈ ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐹 ‘ 𝐵 ) } ) ↔ ( 𝐹 ‘ 𝐵 ) ( 𝑊 ‘ 𝐵 ) ( 𝐹 ‘ 𝐵 ) ) )
37	35 36	ax-mp	⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐹 ‘ 𝐵 ) } ) ↔ ( 𝐹 ‘ 𝐵 ) ( 𝑊 ‘ 𝐵 ) ( 𝐹 ‘ 𝐵 ) )
38	34 37	bitri	⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ↔ ( 𝐹 ‘ 𝐵 ) ( 𝑊 ‘ 𝐵 ) ( 𝐹 ‘ 𝐵 ) )
39	33 38	sylnibr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → ¬ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 )
40	26 27 39	ssnelpssd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → 𝐶 ⊊ 𝐵 )
41		sneq	⊢ ( 𝑦 = ( 𝐹 ‘ 𝐵 ) → { 𝑦 } = { ( 𝐹 ‘ 𝐵 ) } )
42	41	imaeq2d	⊢ ( 𝑦 = ( 𝐹 ‘ 𝐵 ) → ( ◡ ( 𝑊 ‘ 𝐵 ) “ { 𝑦 } ) = ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐹 ‘ 𝐵 ) } ) )
43	42 3	eqtr4di	⊢ ( 𝑦 = ( 𝐹 ‘ 𝐵 ) → ( ◡ ( 𝑊 ‘ 𝐵 ) “ { 𝑦 } ) = 𝐶 )
44	43	fveq2d	⊢ ( 𝑦 = ( 𝐹 ‘ 𝐵 ) → ( 𝐹 ‘ ( ◡ ( 𝑊 ‘ 𝐵 ) “ { 𝑦 } ) ) = ( 𝐹 ‘ 𝐶 ) )
45		id	⊢ ( 𝑦 = ( 𝐹 ‘ 𝐵 ) → 𝑦 = ( 𝐹 ‘ 𝐵 ) )
46	44 45	eqeq12d	⊢ ( 𝑦 = ( 𝐹 ‘ 𝐵 ) → ( ( 𝐹 ‘ ( ◡ ( 𝑊 ‘ 𝐵 ) “ { 𝑦 } ) ) = 𝑦 ↔ ( 𝐹 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐵 ) ) )
47	28	simprd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( ◡ ( 𝑊 ‘ 𝐵 ) “ { 𝑦 } ) ) = 𝑦 )
48	46 47 27	rspcdva	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → ( 𝐹 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐵 ) )
49	48	eqcomd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐶 ) )
50	18 40 49	3jca	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐷 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝐷 ) → ( 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊊ 𝐵 ∧ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐶 ) ) )