Database
REAL AND COMPLEX NUMBERS
Elementary integer functions
The ` # ` (set size) function
fz1isolem
Next ⟩
fz1iso
Metamath Proof Explorer
Ascii
Unicode
Theorem
fz1isolem
Description:
Lemma for
fz1iso
.
(Contributed by
Mario Carneiro
, 2-Apr-2014)
Ref
Expression
Hypotheses
fz1iso.1
ω
⊢
G
=
rec
n
∈
V
⟼
n
+
1
1
↾
ω
fz1iso.2
⊢
B
=
ℕ
∩
<
-1
A
+
1
fz1iso.3
ω
⊢
C
=
ω
∩
G
-1
A
+
1
fz1iso.4
⊢
O
=
OrdIso
R
A
Assertion
fz1isolem
⊢
R
Or
A
∧
A
∈
Fin
→
∃
f
f
Isom
<
,
R
1
…
A
A
Proof
Step
Hyp
Ref
Expression
1
fz1iso.1
ω
⊢
G
=
rec
n
∈
V
⟼
n
+
1
1
↾
ω
2
fz1iso.2
⊢
B
=
ℕ
∩
<
-1
A
+
1
3
fz1iso.3
ω
⊢
C
=
ω
∩
G
-1
A
+
1
4
fz1iso.4
⊢
O
=
OrdIso
R
A
5
hashcl
⊢
A
∈
Fin
→
A
∈
ℕ
0
6
5
adantl
⊢
R
Or
A
∧
A
∈
Fin
→
A
∈
ℕ
0
7
nnuz
⊢
ℕ
=
ℤ
≥
1
8
1z
⊢
1
∈
ℤ
9
8
1
om2uzisoi
ω
⊢
G
Isom
E
,
<
ω
ℤ
≥
1
10
isoeq5
ω
ω
⊢
ℕ
=
ℤ
≥
1
→
G
Isom
E
,
<
ω
ℕ
↔
G
Isom
E
,
<
ω
ℤ
≥
1
11
9
10
mpbiri
ω
⊢
ℕ
=
ℤ
≥
1
→
G
Isom
E
,
<
ω
ℕ
12
7
11
ax-mp
ω
⊢
G
Isom
E
,
<
ω
ℕ
13
isocnv
ω
ω
⊢
G
Isom
E
,
<
ω
ℕ
→
G
-1
Isom
<
,
E
ℕ
ω
14
12
13
ax-mp
ω
⊢
G
-1
Isom
<
,
E
ℕ
ω
15
nn0p1nn
⊢
A
∈
ℕ
0
→
A
+
1
∈
ℕ
16
fvex
⊢
G
-1
A
+
1
∈
V
17
16
epini
⊢
E
-1
G
-1
A
+
1
=
G
-1
A
+
1
18
17
ineq2i
ω
ω
⊢
ω
∩
E
-1
G
-1
A
+
1
=
ω
∩
G
-1
A
+
1
19
3
18
eqtr4i
ω
⊢
C
=
ω
∩
E
-1
G
-1
A
+
1
20
2
19
isoini2
ω
⊢
G
-1
Isom
<
,
E
ℕ
ω
∧
A
+
1
∈
ℕ
→
G
-1
↾
B
Isom
<
,
E
B
C
21
14
15
20
sylancr
⊢
A
∈
ℕ
0
→
G
-1
↾
B
Isom
<
,
E
B
C
22
6
21
syl
⊢
R
Or
A
∧
A
∈
Fin
→
G
-1
↾
B
Isom
<
,
E
B
C
23
nnz
⊢
f
∈
ℕ
→
f
∈
ℤ
24
6
nn0zd
⊢
R
Or
A
∧
A
∈
Fin
→
A
∈
ℤ
25
eluz
⊢
f
∈
ℤ
∧
A
∈
ℤ
→
A
∈
ℤ
≥
f
↔
f
≤
A
26
23
24
25
syl2anr
⊢
R
Or
A
∧
A
∈
Fin
∧
f
∈
ℕ
→
A
∈
ℤ
≥
f
↔
f
≤
A
27
zleltp1
⊢
f
∈
ℤ
∧
A
∈
ℤ
→
f
≤
A
↔
f
<
A
+
1
28
23
24
27
syl2anr
⊢
R
Or
A
∧
A
∈
Fin
∧
f
∈
ℕ
→
f
≤
A
↔
f
<
A
+
1
29
ovex
⊢
A
+
1
∈
V
30
vex
⊢
f
∈
V
31
30
eliniseg
⊢
A
+
1
∈
V
→
f
∈
<
-1
A
+
1
↔
f
<
A
+
1
32
29
31
ax-mp
⊢
f
∈
<
-1
A
+
1
↔
f
<
A
+
1
33
28
32
bitr4di
⊢
R
Or
A
∧
A
∈
Fin
∧
f
∈
ℕ
→
f
≤
A
↔
f
∈
<
-1
A
+
1
34
26
33
bitr2d
⊢
R
Or
A
∧
A
∈
Fin
∧
f
∈
ℕ
→
f
∈
<
-1
A
+
1
↔
A
∈
ℤ
≥
f
35
34
pm5.32da
⊢
R
Or
A
∧
A
∈
Fin
→
f
∈
ℕ
∧
f
∈
<
-1
A
+
1
↔
f
∈
ℕ
∧
A
∈
ℤ
≥
f
36
2
elin2
⊢
f
∈
B
↔
f
∈
ℕ
∧
f
∈
<
-1
A
+
1
37
elfzuzb
⊢
f
∈
1
…
A
↔
f
∈
ℤ
≥
1
∧
A
∈
ℤ
≥
f
38
elnnuz
⊢
f
∈
ℕ
↔
f
∈
ℤ
≥
1
39
38
anbi1i
⊢
f
∈
ℕ
∧
A
∈
ℤ
≥
f
↔
f
∈
ℤ
≥
1
∧
A
∈
ℤ
≥
f
40
37
39
bitr4i
⊢
f
∈
1
…
A
↔
f
∈
ℕ
∧
A
∈
ℤ
≥
f
41
35
36
40
3bitr4g
⊢
R
Or
A
∧
A
∈
Fin
→
f
∈
B
↔
f
∈
1
…
A
42
41
eqrdv
⊢
R
Or
A
∧
A
∈
Fin
→
B
=
1
…
A
43
isoeq4
⊢
B
=
1
…
A
→
G
-1
↾
B
Isom
<
,
E
B
C
↔
G
-1
↾
B
Isom
<
,
E
1
…
A
C
44
42
43
syl
⊢
R
Or
A
∧
A
∈
Fin
→
G
-1
↾
B
Isom
<
,
E
B
C
↔
G
-1
↾
B
Isom
<
,
E
1
…
A
C
45
22
44
mpbid
⊢
R
Or
A
∧
A
∈
Fin
→
G
-1
↾
B
Isom
<
,
E
1
…
A
C
46
4
oion
⊢
A
∈
Fin
→
dom
O
∈
On
47
46
adantl
⊢
R
Or
A
∧
A
∈
Fin
→
dom
O
∈
On
48
simpr
⊢
R
Or
A
∧
A
∈
Fin
→
A
∈
Fin
49
wofi
⊢
R
Or
A
∧
A
∈
Fin
→
R
We
A
50
4
oien
⊢
A
∈
Fin
∧
R
We
A
→
dom
O
≈
A
51
48
49
50
syl2anc
⊢
R
Or
A
∧
A
∈
Fin
→
dom
O
≈
A
52
enfii
⊢
A
∈
Fin
∧
dom
O
≈
A
→
dom
O
∈
Fin
53
48
51
52
syl2anc
⊢
R
Or
A
∧
A
∈
Fin
→
dom
O
∈
Fin
54
47
53
elind
⊢
R
Or
A
∧
A
∈
Fin
→
dom
O
∈
On
∩
Fin
55
onfin2
ω
⊢
ω
=
On
∩
Fin
56
54
55
eleqtrrdi
ω
⊢
R
Or
A
∧
A
∈
Fin
→
dom
O
∈
ω
57
eqid
ω
ω
⊢
rec
n
∈
V
⟼
n
+
1
0
↾
ω
=
rec
n
∈
V
⟼
n
+
1
0
↾
ω
58
0z
⊢
0
∈
ℤ
59
1
57
8
58
uzrdgxfr
ω
ω
⊢
dom
O
∈
ω
→
G
dom
O
=
rec
n
∈
V
⟼
n
+
1
0
↾
ω
dom
O
+
1
-
0
60
1m0e1
⊢
1
−
0
=
1
61
60
oveq2i
ω
ω
⊢
rec
n
∈
V
⟼
n
+
1
0
↾
ω
dom
O
+
1
-
0
=
rec
n
∈
V
⟼
n
+
1
0
↾
ω
dom
O
+
1
62
59
61
eqtrdi
ω
ω
⊢
dom
O
∈
ω
→
G
dom
O
=
rec
n
∈
V
⟼
n
+
1
0
↾
ω
dom
O
+
1
63
56
62
syl
ω
⊢
R
Or
A
∧
A
∈
Fin
→
G
dom
O
=
rec
n
∈
V
⟼
n
+
1
0
↾
ω
dom
O
+
1
64
51
ensymd
⊢
R
Or
A
∧
A
∈
Fin
→
A
≈
dom
O
65
cardennn
ω
⊢
A
≈
dom
O
∧
dom
O
∈
ω
→
card
A
=
dom
O
66
64
56
65
syl2anc
⊢
R
Or
A
∧
A
∈
Fin
→
card
A
=
dom
O
67
66
fveq2d
ω
ω
⊢
R
Or
A
∧
A
∈
Fin
→
rec
n
∈
V
⟼
n
+
1
0
↾
ω
card
A
=
rec
n
∈
V
⟼
n
+
1
0
↾
ω
dom
O
68
57
hashgval
ω
⊢
A
∈
Fin
→
rec
n
∈
V
⟼
n
+
1
0
↾
ω
card
A
=
A
69
68
adantl
ω
⊢
R
Or
A
∧
A
∈
Fin
→
rec
n
∈
V
⟼
n
+
1
0
↾
ω
card
A
=
A
70
67
69
eqtr3d
ω
⊢
R
Or
A
∧
A
∈
Fin
→
rec
n
∈
V
⟼
n
+
1
0
↾
ω
dom
O
=
A
71
70
oveq1d
ω
⊢
R
Or
A
∧
A
∈
Fin
→
rec
n
∈
V
⟼
n
+
1
0
↾
ω
dom
O
+
1
=
A
+
1
72
63
71
eqtrd
⊢
R
Or
A
∧
A
∈
Fin
→
G
dom
O
=
A
+
1
73
72
fveq2d
⊢
R
Or
A
∧
A
∈
Fin
→
G
-1
G
dom
O
=
G
-1
A
+
1
74
isof1o
ω
ω
⊢
G
Isom
E
,
<
ω
ℕ
→
G
:
ω
⟶
1-1 onto
ℕ
75
12
74
ax-mp
ω
⊢
G
:
ω
⟶
1-1 onto
ℕ
76
f1ocnvfv1
ω
ω
⊢
G
:
ω
⟶
1-1 onto
ℕ
∧
dom
O
∈
ω
→
G
-1
G
dom
O
=
dom
O
77
75
56
76
sylancr
⊢
R
Or
A
∧
A
∈
Fin
→
G
-1
G
dom
O
=
dom
O
78
73
77
eqtr3d
⊢
R
Or
A
∧
A
∈
Fin
→
G
-1
A
+
1
=
dom
O
79
78
ineq2d
ω
ω
⊢
R
Or
A
∧
A
∈
Fin
→
ω
∩
G
-1
A
+
1
=
ω
∩
dom
O
80
ordom
ω
⊢
Ord
ω
81
ordelss
ω
ω
ω
⊢
Ord
ω
∧
dom
O
∈
ω
→
dom
O
⊆
ω
82
80
56
81
sylancr
ω
⊢
R
Or
A
∧
A
∈
Fin
→
dom
O
⊆
ω
83
sseqin2
ω
ω
⊢
dom
O
⊆
ω
↔
ω
∩
dom
O
=
dom
O
84
82
83
sylib
ω
⊢
R
Or
A
∧
A
∈
Fin
→
ω
∩
dom
O
=
dom
O
85
79
84
eqtrd
ω
⊢
R
Or
A
∧
A
∈
Fin
→
ω
∩
G
-1
A
+
1
=
dom
O
86
3
85
eqtrid
⊢
R
Or
A
∧
A
∈
Fin
→
C
=
dom
O
87
isoeq5
⊢
C
=
dom
O
→
G
-1
↾
B
Isom
<
,
E
1
…
A
C
↔
G
-1
↾
B
Isom
<
,
E
1
…
A
dom
O
88
86
87
syl
⊢
R
Or
A
∧
A
∈
Fin
→
G
-1
↾
B
Isom
<
,
E
1
…
A
C
↔
G
-1
↾
B
Isom
<
,
E
1
…
A
dom
O
89
45
88
mpbid
⊢
R
Or
A
∧
A
∈
Fin
→
G
-1
↾
B
Isom
<
,
E
1
…
A
dom
O
90
4
oiiso
⊢
A
∈
Fin
∧
R
We
A
→
O
Isom
E
,
R
dom
O
A
91
48
49
90
syl2anc
⊢
R
Or
A
∧
A
∈
Fin
→
O
Isom
E
,
R
dom
O
A
92
isotr
⊢
G
-1
↾
B
Isom
<
,
E
1
…
A
dom
O
∧
O
Isom
E
,
R
dom
O
A
→
O
∘
G
-1
↾
B
Isom
<
,
R
1
…
A
A
93
89
91
92
syl2anc
⊢
R
Or
A
∧
A
∈
Fin
→
O
∘
G
-1
↾
B
Isom
<
,
R
1
…
A
A
94
isof1o
⊢
O
∘
G
-1
↾
B
Isom
<
,
R
1
…
A
A
→
O
∘
G
-1
↾
B
:
1
…
A
⟶
1-1 onto
A
95
f1of
⊢
O
∘
G
-1
↾
B
:
1
…
A
⟶
1-1 onto
A
→
O
∘
G
-1
↾
B
:
1
…
A
⟶
A
96
93
94
95
3syl
⊢
R
Or
A
∧
A
∈
Fin
→
O
∘
G
-1
↾
B
:
1
…
A
⟶
A
97
fzfid
⊢
R
Or
A
∧
A
∈
Fin
→
1
…
A
∈
Fin
98
96
97
fexd
⊢
R
Or
A
∧
A
∈
Fin
→
O
∘
G
-1
↾
B
∈
V
99
isoeq1
⊢
f
=
O
∘
G
-1
↾
B
→
f
Isom
<
,
R
1
…
A
A
↔
O
∘
G
-1
↾
B
Isom
<
,
R
1
…
A
A
100
98
93
99
spcedv
⊢
R
Or
A
∧
A
∈
Fin
→
∃
f
f
Isom
<
,
R
1
…
A
A