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 ffvelrnd ( ( ( 𝐴𝑉𝐹 : 𝐷𝐴 ∧ ( 𝒫 𝐴 ∩ 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 ) ⊆ 𝐷 ) → ( 𝐵𝐴𝐶𝐵 ∧ ( 𝐹𝐵 ) = ( 𝐹𝐶 ) ) )