Metamath Proof Explorer


Theorem hashdom

Description: Dominance relation for the size function. (Contributed by Mario Carneiro, 22-Sep-2013) (Revised by Mario Carneiro, 22-Apr-2015)

Ref Expression
Assertion hashdom ( ( 𝐴 ∈ Fin ∧ 𝐵𝑉 ) → ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ↔ 𝐴𝐵 ) )

Proof

Step Hyp Ref Expression
1 fzfi ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ∈ Fin
2 ficardom ( ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ∈ Fin → ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ∈ ω )
3 1 2 ax-mp ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ∈ ω
4 eqid ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
5 4 hashgval ( 𝐴 ∈ Fin → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) )
6 5 ad2antrr ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) )
7 4 hashgval ( ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ∈ Fin → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) = ( ♯ ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) )
8 1 7 ax-mp ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) = ( ♯ ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) )
9 hashcl ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
10 9 ad2antrr ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
11 hashcl ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
12 11 ad2antlr ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
13 simpr ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) )
14 nn0sub2 ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ∈ ℕ0 )
15 10 12 13 14 syl3anc ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ∈ ℕ0 )
16 hashfz1 ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) = ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) )
17 15 16 syl ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) = ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) )
18 8 17 eqtrid ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) = ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) )
19 6 18 oveq12d ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) + ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) )
20 9 nn0cnd ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℂ )
21 11 nn0cnd ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℂ )
22 pncan3 ( ( ( ♯ ‘ 𝐴 ) ∈ ℂ ∧ ( ♯ ‘ 𝐵 ) ∈ ℂ ) → ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ 𝐵 ) )
23 20 21 22 syl2an ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ 𝐵 ) )
24 23 adantr ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ 𝐵 ) )
25 19 24 eqtrd ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) + ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) = ( ♯ ‘ 𝐵 ) )
26 ficardom ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ∈ ω )
27 26 ad2antrr ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( card ‘ 𝐴 ) ∈ ω )
28 4 hashgadd ( ( ( card ‘ 𝐴 ) ∈ ω ∧ ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) + ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) )
29 27 3 28 sylancl ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) + ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) )
30 4 hashgval ( 𝐵 ∈ Fin → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) = ( ♯ ‘ 𝐵 ) )
31 30 ad2antlr ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) = ( ♯ ‘ 𝐵 ) )
32 25 29 31 3eqtr4d ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) )
33 32 fveq2d ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) ) )
34 4 hashgf1o ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) : ω –1-1-onto→ ℕ0
35 nnacl ( ( ( card ‘ 𝐴 ) ∈ ω ∧ ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ∈ ω ) → ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ∈ ω )
36 27 3 35 sylancl ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ∈ ω )
37 f1ocnvfv1 ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) : ω –1-1-onto→ ℕ0 ∧ ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) ) = ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) )
38 34 36 37 sylancr ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) ) = ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) )
39 ficardom ( 𝐵 ∈ Fin → ( card ‘ 𝐵 ) ∈ ω )
40 39 ad2antlr ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( card ‘ 𝐵 ) ∈ ω )
41 f1ocnvfv1 ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) : ω –1-1-onto→ ℕ0 ∧ ( card ‘ 𝐵 ) ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) ) = ( card ‘ 𝐵 ) )
42 34 40 41 sylancr ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) ) = ( card ‘ 𝐵 ) )
43 33 38 42 3eqtr3d ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) = ( card ‘ 𝐵 ) )
44 oveq2 ( 𝑦 = ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) → ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) )
45 44 eqeq1d ( 𝑦 = ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) → ( ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( card ‘ 𝐵 ) ↔ ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) = ( card ‘ 𝐵 ) ) )
46 45 rspcev ( ( ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ∈ ω ∧ ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) = ( card ‘ 𝐵 ) ) → ∃ 𝑦 ∈ ω ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( card ‘ 𝐵 ) )
47 3 43 46 sylancr ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ∃ 𝑦 ∈ ω ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( card ‘ 𝐵 ) )
48 47 ex ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) → ∃ 𝑦 ∈ ω ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( card ‘ 𝐵 ) ) )
49 cardnn ( 𝑦 ∈ ω → ( card ‘ 𝑦 ) = 𝑦 )
50 49 adantl ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ ω ) → ( card ‘ 𝑦 ) = 𝑦 )
51 50 oveq2d ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ ω ) → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) = ( ( card ‘ 𝐴 ) +o 𝑦 ) )
52 51 eqeq1d ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ ω ) → ( ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) = ( card ‘ 𝐵 ) ↔ ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( card ‘ 𝐵 ) ) )
53 fveq2 ( ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) = ( card ‘ 𝐵 ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) )
54 nnfi ( 𝑦 ∈ ω → 𝑦 ∈ Fin )
55 ficardom ( 𝑦 ∈ Fin → ( card ‘ 𝑦 ) ∈ ω )
56 4 hashgadd ( ( ( card ‘ 𝐴 ) ∈ ω ∧ ( card ‘ 𝑦 ) ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) + ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝑦 ) ) ) )
57 26 55 56 syl2an ( ( 𝐴 ∈ Fin ∧ 𝑦 ∈ Fin ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) + ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝑦 ) ) ) )
58 4 hashgval ( 𝑦 ∈ Fin → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝑦 ) ) = ( ♯ ‘ 𝑦 ) )
59 5 58 oveqan12d ( ( 𝐴 ∈ Fin ∧ 𝑦 ∈ Fin ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) + ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝑦 ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) )
60 57 59 eqtrd ( ( 𝐴 ∈ Fin ∧ 𝑦 ∈ Fin ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) )
61 60 adantlr ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ Fin ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) )
62 30 ad2antlr ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ Fin ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) = ( ♯ ‘ 𝐵 ) )
63 61 62 eqeq12d ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ Fin ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) ↔ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) = ( ♯ ‘ 𝐵 ) ) )
64 hashcl ( 𝑦 ∈ Fin → ( ♯ ‘ 𝑦 ) ∈ ℕ0 )
65 64 nn0ge0d ( 𝑦 ∈ Fin → 0 ≤ ( ♯ ‘ 𝑦 ) )
66 65 adantl ( ( 𝐴 ∈ Fin ∧ 𝑦 ∈ Fin ) → 0 ≤ ( ♯ ‘ 𝑦 ) )
67 9 nn0red ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℝ )
68 64 nn0red ( 𝑦 ∈ Fin → ( ♯ ‘ 𝑦 ) ∈ ℝ )
69 addge01 ( ( ( ♯ ‘ 𝐴 ) ∈ ℝ ∧ ( ♯ ‘ 𝑦 ) ∈ ℝ ) → ( 0 ≤ ( ♯ ‘ 𝑦 ) ↔ ( ♯ ‘ 𝐴 ) ≤ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) ) )
70 67 68 69 syl2an ( ( 𝐴 ∈ Fin ∧ 𝑦 ∈ Fin ) → ( 0 ≤ ( ♯ ‘ 𝑦 ) ↔ ( ♯ ‘ 𝐴 ) ≤ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) ) )
71 66 70 mpbid ( ( 𝐴 ∈ Fin ∧ 𝑦 ∈ Fin ) → ( ♯ ‘ 𝐴 ) ≤ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) )
72 71 adantlr ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ Fin ) → ( ♯ ‘ 𝐴 ) ≤ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) )
73 breq2 ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) = ( ♯ ‘ 𝐵 ) → ( ( ♯ ‘ 𝐴 ) ≤ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) ↔ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) )
74 72 73 syl5ibcom ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ Fin ) → ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) = ( ♯ ‘ 𝐵 ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) )
75 63 74 sylbid ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ Fin ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) )
76 54 75 sylan2 ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ ω ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) )
77 53 76 syl5 ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ ω ) → ( ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) = ( card ‘ 𝐵 ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) )
78 52 77 sylbird ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ ω ) → ( ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( card ‘ 𝐵 ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) )
79 78 rexlimdva ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ∃ 𝑦 ∈ ω ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( card ‘ 𝐵 ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) )
80 48 79 impbid ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ↔ ∃ 𝑦 ∈ ω ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( card ‘ 𝐵 ) ) )
81 nnawordex ( ( ( card ‘ 𝐴 ) ∈ ω ∧ ( card ‘ 𝐵 ) ∈ ω ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ ∃ 𝑦 ∈ ω ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( card ‘ 𝐵 ) ) )
82 26 39 81 syl2an ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ ∃ 𝑦 ∈ ω ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( card ‘ 𝐵 ) ) )
83 finnum ( 𝐴 ∈ Fin → 𝐴 ∈ dom card )
84 finnum ( 𝐵 ∈ Fin → 𝐵 ∈ dom card )
85 carddom2 ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ 𝐴𝐵 ) )
86 83 84 85 syl2an ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ 𝐴𝐵 ) )
87 80 82 86 3bitr2d ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ↔ 𝐴𝐵 ) )
88 87 adantlr ( ( ( 𝐴 ∈ Fin ∧ 𝐵𝑉 ) ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ↔ 𝐴𝐵 ) )
89 hashxrcl ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℝ* )
90 89 ad2antrr ( ( ( 𝐴 ∈ Fin ∧ 𝐵𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐴 ) ∈ ℝ* )
91 pnfge ( ( ♯ ‘ 𝐴 ) ∈ ℝ* → ( ♯ ‘ 𝐴 ) ≤ +∞ )
92 90 91 syl ( ( ( 𝐴 ∈ Fin ∧ 𝐵𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐴 ) ≤ +∞ )
93 hashinf ( ( 𝐵𝑉 ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) = +∞ )
94 93 adantll ( ( ( 𝐴 ∈ Fin ∧ 𝐵𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) = +∞ )
95 92 94 breqtrrd ( ( ( 𝐴 ∈ Fin ∧ 𝐵𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) )
96 isinffi ( ( ¬ 𝐵 ∈ Fin ∧ 𝐴 ∈ Fin ) → ∃ 𝑓 𝑓 : 𝐴1-1𝐵 )
97 96 ancoms ( ( 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin ) → ∃ 𝑓 𝑓 : 𝐴1-1𝐵 )
98 97 adantlr ( ( ( 𝐴 ∈ Fin ∧ 𝐵𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → ∃ 𝑓 𝑓 : 𝐴1-1𝐵 )
99 brdomg ( 𝐵𝑉 → ( 𝐴𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴1-1𝐵 ) )
100 99 ad2antlr ( ( ( 𝐴 ∈ Fin ∧ 𝐵𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → ( 𝐴𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴1-1𝐵 ) )
101 98 100 mpbird ( ( ( 𝐴 ∈ Fin ∧ 𝐵𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → 𝐴𝐵 )
102 95 101 2thd ( ( ( 𝐴 ∈ Fin ∧ 𝐵𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ↔ 𝐴𝐵 ) )
103 88 102 pm2.61dan ( ( 𝐴 ∈ Fin ∧ 𝐵𝑉 ) → ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ↔ 𝐴𝐵 ) )