Metamath Proof Explorer

Theorem canthnumlem

Description: Lemma for canthnum . (Contributed by Mario Carneiro, 19-May-2015)

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

Proof

Step Hyp Ref Expression
1 canth4.1 ⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) }
2 canth4.2 ⊢ 𝐵 = ∪ dom 𝑊
3 canth4.3 ⊢ 𝐶 = ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐹 ‘ 𝐵 ) } )
4 f1f ⊢ ( 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 → 𝐹 : ( 𝒫 𝐴 ∩ dom card ) ⟶ 𝐴 )
5 ssid ⊢ ( 𝒫 𝐴 ∩ dom card ) ⊆ ( 𝒫 𝐴 ∩ dom card )
6 1 2 3 canth4 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ ( 𝒫 𝐴 ∩ dom card ) ) → ( 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊊ 𝐵 ∧ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐶 ) ) )
7 5 6 mp3an3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) ⟶ 𝐴 ) → ( 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊊ 𝐵 ∧ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐶 ) ) )
8 4 7 sylan2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → ( 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊊ 𝐵 ∧ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐶 ) ) )
9 8 simp3d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐶 ) )
10 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 )
11 8 simp1d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → 𝐵 ⊆ 𝐴 )
12 elpw2g ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 ∈ 𝒫 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
13 12 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → ( 𝐵 ∈ 𝒫 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
14 11 13 mpbird ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → 𝐵 ∈ 𝒫 𝐴 )
15 eqid ⊢ 𝐵 = 𝐵
16 eqid ⊢ ( 𝑊 ‘ 𝐵 ) = ( 𝑊 ‘ 𝐵 )
17 15 16 pm3.2i ⊢ ( 𝐵 = 𝐵 ∧ ( 𝑊 ‘ 𝐵 ) = ( 𝑊 ‘ 𝐵 ) )
18 simpl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → 𝐴 ∈ 𝑉 )
19 10 4 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → 𝐹 : ( 𝒫 𝐴 ∩ dom card ) ⟶ 𝐴 )
20 19 ffvelrnda ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ dom card ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 )
21 1 18 20 2 fpwwe ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → ( ( 𝐵 𝑊 ( 𝑊 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐵 ) ↔ ( 𝐵 = 𝐵 ∧ ( 𝑊 ‘ 𝐵 ) = ( 𝑊 ‘ 𝐵 ) ) ) )
22 17 21 mpbiri ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → ( 𝐵 𝑊 ( 𝑊 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐵 ) )
23 22 simpld ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → 𝐵 𝑊 ( 𝑊 ‘ 𝐵 ) )
24 1 18 fpwwelem ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → ( 𝐵 𝑊 ( 𝑊 ‘ 𝐵 ) ↔ ( ( 𝐵 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝐵 ) ⊆ ( 𝐵 × 𝐵 ) ) ∧ ( ( 𝑊 ‘ 𝐵 ) We 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( ◡ ( 𝑊 ‘ 𝐵 ) “ { 𝑦 } ) ) = 𝑦 ) ) ) )
25 23 24 mpbid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → ( ( 𝐵 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝐵 ) ⊆ ( 𝐵 × 𝐵 ) ) ∧ ( ( 𝑊 ‘ 𝐵 ) We 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( ◡ ( 𝑊 ‘ 𝐵 ) “ { 𝑦 } ) ) = 𝑦 ) ) )
26 25 simprld ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → ( 𝑊 ‘ 𝐵 ) We 𝐵 )
27 fvex ⊢ ( 𝑊 ‘ 𝐵 ) ∈ V
28 weeq1 ⊢ ( 𝑟 = ( 𝑊 ‘ 𝐵 ) → ( 𝑟 We 𝐵 ↔ ( 𝑊 ‘ 𝐵 ) We 𝐵 ) )
29 27 28 spcev ⊢ ( ( 𝑊 ‘ 𝐵 ) We 𝐵 → ∃ 𝑟 𝑟 We 𝐵 )
30 26 29 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → ∃ 𝑟 𝑟 We 𝐵 )
31 ween ⊢ ( 𝐵 ∈ dom card ↔ ∃ 𝑟 𝑟 We 𝐵 )
32 30 31 sylibr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → 𝐵 ∈ dom card )
33 14 32 elind ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → 𝐵 ∈ ( 𝒫 𝐴 ∩ dom card ) )
34 8 simp2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → 𝐶 ⊊ 𝐵 )
35 34 pssssd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → 𝐶 ⊆ 𝐵 )
36 35 11 sstrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → 𝐶 ⊆ 𝐴 )
37 elpw2g ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐶 ∈ 𝒫 𝐴 ↔ 𝐶 ⊆ 𝐴 ) )
38 37 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → ( 𝐶 ∈ 𝒫 𝐴 ↔ 𝐶 ⊆ 𝐴 ) )
39 36 38 mpbird ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → 𝐶 ∈ 𝒫 𝐴 )
40 ssnum ⊢ ( ( 𝐵 ∈ dom card ∧ 𝐶 ⊆ 𝐵 ) → 𝐶 ∈ dom card )
41 32 35 40 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → 𝐶 ∈ dom card )
42 39 41 elind ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → 𝐶 ∈ ( 𝒫 𝐴 ∩ dom card ) )
43 f1fveq ⊢ ( ( 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ∧ ( 𝐵 ∈ ( 𝒫 𝐴 ∩ dom card ) ∧ 𝐶 ∈ ( 𝒫 𝐴 ∩ dom card ) ) ) → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐶 ) ↔ 𝐵 = 𝐶 ) )
44 10 33 42 43 syl12anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐶 ) ↔ 𝐵 = 𝐶 ) )
45 9 44 mpbid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → 𝐵 = 𝐶 )
46 34 pssned ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → 𝐶 ≠ 𝐵 )
47 46 necomd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → 𝐵 ≠ 𝐶 )
48 47 neneqd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 ) → ¬ 𝐵 = 𝐶 )
49 45 48 pm2.65da ⊢ ( 𝐴 ∈ 𝑉 → ¬ 𝐹 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 )