Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Infinity
The Ackermann bijection
ackbij1lem14
Next ⟩
ackbij1lem15
Metamath Proof Explorer
Ascii
Unicode
Theorem
ackbij1lem14
Description:
Lemma for
ackbij1
.
(Contributed by
Stefan O'Rear
, 18-Nov-2014)
Ref
Expression
Hypothesis
ackbij.f
ω
⊢
F
=
x
∈
𝒫
ω
∩
Fin
⟼
card
⋃
y
∈
x
y
×
𝒫
y
Assertion
ackbij1lem14
ω
⊢
A
∈
ω
→
F
A
=
suc
F
A
Proof
Step
Hyp
Ref
Expression
1
ackbij.f
ω
⊢
F
=
x
∈
𝒫
ω
∩
Fin
⟼
card
⋃
y
∈
x
y
×
𝒫
y
2
1
ackbij1lem8
ω
⊢
A
∈
ω
→
F
A
=
card
𝒫
A
3
pweq
⊢
a
=
∅
→
𝒫
a
=
𝒫
∅
4
3
fveq2d
⊢
a
=
∅
→
card
𝒫
a
=
card
𝒫
∅
5
fveq2
⊢
a
=
∅
→
F
a
=
F
∅
6
suceq
⊢
F
a
=
F
∅
→
suc
F
a
=
suc
F
∅
7
5
6
syl
⊢
a
=
∅
→
suc
F
a
=
suc
F
∅
8
4
7
eqeq12d
⊢
a
=
∅
→
card
𝒫
a
=
suc
F
a
↔
card
𝒫
∅
=
suc
F
∅
9
pweq
⊢
a
=
b
→
𝒫
a
=
𝒫
b
10
9
fveq2d
⊢
a
=
b
→
card
𝒫
a
=
card
𝒫
b
11
fveq2
⊢
a
=
b
→
F
a
=
F
b
12
suceq
⊢
F
a
=
F
b
→
suc
F
a
=
suc
F
b
13
11
12
syl
⊢
a
=
b
→
suc
F
a
=
suc
F
b
14
10
13
eqeq12d
⊢
a
=
b
→
card
𝒫
a
=
suc
F
a
↔
card
𝒫
b
=
suc
F
b
15
pweq
⊢
a
=
suc
b
→
𝒫
a
=
𝒫
suc
b
16
15
fveq2d
⊢
a
=
suc
b
→
card
𝒫
a
=
card
𝒫
suc
b
17
fveq2
⊢
a
=
suc
b
→
F
a
=
F
suc
b
18
suceq
⊢
F
a
=
F
suc
b
→
suc
F
a
=
suc
F
suc
b
19
17
18
syl
⊢
a
=
suc
b
→
suc
F
a
=
suc
F
suc
b
20
16
19
eqeq12d
⊢
a
=
suc
b
→
card
𝒫
a
=
suc
F
a
↔
card
𝒫
suc
b
=
suc
F
suc
b
21
pweq
⊢
a
=
A
→
𝒫
a
=
𝒫
A
22
21
fveq2d
⊢
a
=
A
→
card
𝒫
a
=
card
𝒫
A
23
fveq2
⊢
a
=
A
→
F
a
=
F
A
24
suceq
⊢
F
a
=
F
A
→
suc
F
a
=
suc
F
A
25
23
24
syl
⊢
a
=
A
→
suc
F
a
=
suc
F
A
26
22
25
eqeq12d
⊢
a
=
A
→
card
𝒫
a
=
suc
F
a
↔
card
𝒫
A
=
suc
F
A
27
df-1o
⊢
1
𝑜
=
suc
∅
28
pw0
⊢
𝒫
∅
=
∅
29
28
fveq2i
⊢
card
𝒫
∅
=
card
∅
30
0ex
⊢
∅
∈
V
31
cardsn
⊢
∅
∈
V
→
card
∅
=
1
𝑜
32
30
31
ax-mp
⊢
card
∅
=
1
𝑜
33
29
32
eqtri
⊢
card
𝒫
∅
=
1
𝑜
34
1
ackbij1lem13
⊢
F
∅
=
∅
35
suceq
⊢
F
∅
=
∅
→
suc
F
∅
=
suc
∅
36
34
35
ax-mp
⊢
suc
F
∅
=
suc
∅
37
27
33
36
3eqtr4i
⊢
card
𝒫
∅
=
suc
F
∅
38
oveq2
⊢
card
𝒫
b
=
suc
F
b
→
card
𝒫
b
+
𝑜
card
𝒫
b
=
card
𝒫
b
+
𝑜
suc
F
b
39
38
adantl
ω
⊢
b
∈
ω
∧
card
𝒫
b
=
suc
F
b
→
card
𝒫
b
+
𝑜
card
𝒫
b
=
card
𝒫
b
+
𝑜
suc
F
b
40
ackbij1lem5
ω
⊢
b
∈
ω
→
card
𝒫
suc
b
=
card
𝒫
b
+
𝑜
card
𝒫
b
41
40
adantr
ω
⊢
b
∈
ω
∧
card
𝒫
b
=
suc
F
b
→
card
𝒫
suc
b
=
card
𝒫
b
+
𝑜
card
𝒫
b
42
df-suc
⊢
suc
b
=
b
∪
b
43
42
equncomi
⊢
suc
b
=
b
∪
b
44
43
fveq2i
⊢
F
suc
b
=
F
b
∪
b
45
ackbij1lem4
ω
ω
⊢
b
∈
ω
→
b
∈
𝒫
ω
∩
Fin
46
45
adantr
ω
ω
⊢
b
∈
ω
∧
card
𝒫
b
=
suc
F
b
→
b
∈
𝒫
ω
∩
Fin
47
ackbij1lem3
ω
ω
⊢
b
∈
ω
→
b
∈
𝒫
ω
∩
Fin
48
47
adantr
ω
ω
⊢
b
∈
ω
∧
card
𝒫
b
=
suc
F
b
→
b
∈
𝒫
ω
∩
Fin
49
incom
⊢
b
∩
b
=
b
∩
b
50
nnord
ω
⊢
b
∈
ω
→
Ord
b
51
orddisj
⊢
Ord
b
→
b
∩
b
=
∅
52
50
51
syl
ω
⊢
b
∈
ω
→
b
∩
b
=
∅
53
49
52
eqtrid
ω
⊢
b
∈
ω
→
b
∩
b
=
∅
54
53
adantr
ω
⊢
b
∈
ω
∧
card
𝒫
b
=
suc
F
b
→
b
∩
b
=
∅
55
1
ackbij1lem9
ω
ω
⊢
b
∈
𝒫
ω
∩
Fin
∧
b
∈
𝒫
ω
∩
Fin
∧
b
∩
b
=
∅
→
F
b
∪
b
=
F
b
+
𝑜
F
b
56
46
48
54
55
syl3anc
ω
⊢
b
∈
ω
∧
card
𝒫
b
=
suc
F
b
→
F
b
∪
b
=
F
b
+
𝑜
F
b
57
1
ackbij1lem8
ω
⊢
b
∈
ω
→
F
b
=
card
𝒫
b
58
57
adantr
ω
⊢
b
∈
ω
∧
card
𝒫
b
=
suc
F
b
→
F
b
=
card
𝒫
b
59
58
oveq1d
ω
⊢
b
∈
ω
∧
card
𝒫
b
=
suc
F
b
→
F
b
+
𝑜
F
b
=
card
𝒫
b
+
𝑜
F
b
60
56
59
eqtrd
ω
⊢
b
∈
ω
∧
card
𝒫
b
=
suc
F
b
→
F
b
∪
b
=
card
𝒫
b
+
𝑜
F
b
61
44
60
eqtrid
ω
⊢
b
∈
ω
∧
card
𝒫
b
=
suc
F
b
→
F
suc
b
=
card
𝒫
b
+
𝑜
F
b
62
suceq
⊢
F
suc
b
=
card
𝒫
b
+
𝑜
F
b
→
suc
F
suc
b
=
suc
card
𝒫
b
+
𝑜
F
b
63
61
62
syl
ω
⊢
b
∈
ω
∧
card
𝒫
b
=
suc
F
b
→
suc
F
suc
b
=
suc
card
𝒫
b
+
𝑜
F
b
64
nnfi
ω
⊢
b
∈
ω
→
b
∈
Fin
65
pwfi
⊢
b
∈
Fin
↔
𝒫
b
∈
Fin
66
64
65
sylib
ω
⊢
b
∈
ω
→
𝒫
b
∈
Fin
67
66
adantr
ω
⊢
b
∈
ω
∧
card
𝒫
b
=
suc
F
b
→
𝒫
b
∈
Fin
68
ficardom
ω
⊢
𝒫
b
∈
Fin
→
card
𝒫
b
∈
ω
69
67
68
syl
ω
ω
⊢
b
∈
ω
∧
card
𝒫
b
=
suc
F
b
→
card
𝒫
b
∈
ω
70
1
ackbij1lem10
ω
ω
⊢
F
:
𝒫
ω
∩
Fin
⟶
ω
71
70
ffvelrni
ω
ω
⊢
b
∈
𝒫
ω
∩
Fin
→
F
b
∈
ω
72
48
71
syl
ω
ω
⊢
b
∈
ω
∧
card
𝒫
b
=
suc
F
b
→
F
b
∈
ω
73
nnasuc
ω
ω
⊢
card
𝒫
b
∈
ω
∧
F
b
∈
ω
→
card
𝒫
b
+
𝑜
suc
F
b
=
suc
card
𝒫
b
+
𝑜
F
b
74
69
72
73
syl2anc
ω
⊢
b
∈
ω
∧
card
𝒫
b
=
suc
F
b
→
card
𝒫
b
+
𝑜
suc
F
b
=
suc
card
𝒫
b
+
𝑜
F
b
75
63
74
eqtr4d
ω
⊢
b
∈
ω
∧
card
𝒫
b
=
suc
F
b
→
suc
F
suc
b
=
card
𝒫
b
+
𝑜
suc
F
b
76
39
41
75
3eqtr4d
ω
⊢
b
∈
ω
∧
card
𝒫
b
=
suc
F
b
→
card
𝒫
suc
b
=
suc
F
suc
b
77
76
ex
ω
⊢
b
∈
ω
→
card
𝒫
b
=
suc
F
b
→
card
𝒫
suc
b
=
suc
F
suc
b
78
8
14
20
26
37
77
finds
ω
⊢
A
∈
ω
→
card
𝒫
A
=
suc
F
A
79
2
78
eqtrd
ω
⊢
A
∈
ω
→
F
A
=
suc
F
A