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

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 ∧ 𝐵 ∈ 𝑉 ) → ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ↔ 𝐴 ≼ 𝐵 ) )