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 ⊢ A ∈ Fin ∧ B ∈ V → A ≤ B ↔ A ≼ B

Proof

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