This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ⊆ 𝐷 ) → ( 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊊ 𝐵 ∧ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐶 ) ) )