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+10↾ω=rec⁡x∈V⟼x+10↾ω
5 4 hashgval ⊢A∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡A=A
6 5 ad2antrr ⊢A∈Fin∧B∈Fin∧A≤B→rec⁡x∈V⟼x+10↾ω⁡card⁡A=A
7 4 hashgval ⊢1…B−A∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡1…B−A=1…B−A
8 1 7 ax-mp ⊢rec⁡x∈V⟼x+10↾ω⁡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 eqtrid ⊢A∈Fin∧B∈Fin∧A≤B→rec⁡x∈V⟼x+10↾ω⁡card⁡1…B−A=B−A
19 6 18 oveq12d ⊢A∈Fin∧B∈Fin∧A≤B→rec⁡x∈V⟼x+10↾ω⁡card⁡A+rec⁡x∈V⟼x+10↾ω⁡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+10↾ω⁡card⁡A+rec⁡x∈V⟼x+10↾ω⁡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+10↾ω⁡card⁡A+𝑜card⁡1…B−A=rec⁡x∈V⟼x+10↾ω⁡card⁡A+rec⁡x∈V⟼x+10↾ω⁡card⁡1…B−A
29 27 3 28 sylancl ⊢A∈Fin∧B∈Fin∧A≤B→rec⁡x∈V⟼x+10↾ω⁡card⁡A+𝑜card⁡1…B−A=rec⁡x∈V⟼x+10↾ω⁡card⁡A+rec⁡x∈V⟼x+10↾ω⁡card⁡1…B−A
30 4 hashgval ⊢B∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡B=B
31 30 ad2antlr ⊢A∈Fin∧B∈Fin∧A≤B→rec⁡x∈V⟼x+10↾ω⁡card⁡B=B
32 25 29 31 3eqtr4d ⊢A∈Fin∧B∈Fin∧A≤B→rec⁡x∈V⟼x+10↾ω⁡card⁡A+𝑜card⁡1…B−A=rec⁡x∈V⟼x+10↾ω⁡card⁡B
33 32 fveq2d ⊢A∈Fin∧B∈Fin∧A≤B→rec⁡x∈V⟼x+10↾ω-1⁡rec⁡x∈V⟼x+10↾ω⁡card⁡A+𝑜card⁡1…B−A=rec⁡x∈V⟼x+10↾ω-1⁡rec⁡x∈V⟼x+10↾ω⁡card⁡B
34 4 hashgf1o ⊢rec⁡x∈V⟼x+10↾ω:ω⟶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+10↾ω:ω⟶1-1 ontoℕ0∧card⁡A+𝑜card⁡1…B−A∈ω→rec⁡x∈V⟼x+10↾ω-1⁡rec⁡x∈V⟼x+10↾ω⁡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+10↾ω-1⁡rec⁡x∈V⟼x+10↾ω⁡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+10↾ω:ω⟶1-1 ontoℕ0∧card⁡B∈ω→rec⁡x∈V⟼x+10↾ω-1⁡rec⁡x∈V⟼x+10↾ω⁡card⁡B=card⁡B
42 34 40 41 sylancr ⊢A∈Fin∧B∈Fin∧A≤B→rec⁡x∈V⟼x+10↾ω-1⁡rec⁡x∈V⟼x+10↾ω⁡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+10↾ω⁡card⁡A+𝑜card⁡y=rec⁡x∈V⟼x+10↾ω⁡card⁡B
54 nnfi ⊢y∈ω→y∈Fin
55 ficardom ⊢y∈Fin→card⁡y∈ω
56 4 hashgadd ⊢card⁡A∈ω∧card⁡y∈ω→rec⁡x∈V⟼x+10↾ω⁡card⁡A+𝑜card⁡y=rec⁡x∈V⟼x+10↾ω⁡card⁡A+rec⁡x∈V⟼x+10↾ω⁡card⁡y
57 26 55 56 syl2an ⊢A∈Fin∧y∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡A+𝑜card⁡y=rec⁡x∈V⟼x+10↾ω⁡card⁡A+rec⁡x∈V⟼x+10↾ω⁡card⁡y
58 4 hashgval ⊢y∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡y=y
59 5 58 oveqan12d ⊢A∈Fin∧y∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡A+rec⁡x∈V⟼x+10↾ω⁡card⁡y=A+y
60 57 59 eqtrd ⊢A∈Fin∧y∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡A+𝑜card⁡y=A+y
61 60 adantlr ⊢A∈Fin∧B∈Fin∧y∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡A+𝑜card⁡y=A+y
62 30 ad2antlr ⊢A∈Fin∧B∈Fin∧y∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡B=B
63 61 62 eqeq12d ⊢A∈Fin∧B∈Fin∧y∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡A+𝑜card⁡y=rec⁡x∈V⟼x+10↾ω⁡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+10↾ω⁡card⁡A+𝑜card⁡y=rec⁡x∈V⟼x+10↾ω⁡card⁡B→A≤B
76 54 75 sylan2 ⊢A∈Fin∧B∈Fin∧y∈ω→rec⁡x∈V⟼x+10↾ω⁡card⁡A+𝑜card⁡y=rec⁡x∈V⟼x+10↾ω⁡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→∃ff:A⟶1-1B
97 96 ancoms ⊢A∈Fin∧¬B∈Fin→∃ff:A⟶1-1B
98 97 adantlr ⊢A∈Fin∧B∈V∧¬B∈Fin→∃ff:A⟶1-1B
99 brdomg ⊢B∈V→A≼B↔∃ff:A⟶1-1B
100 99 ad2antlr ⊢A∈Fin∧B∈V∧¬B∈Fin→A≼B↔∃ff:A⟶1-1B
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