Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Infinity
The Ackermann bijection
ackbij1lem18
Next ⟩
ackbij1
Metamath Proof Explorer
Ascii
Unicode
Theorem
ackbij1lem18
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
ackbij1lem18
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
∃
b
∈
𝒫
ω
∩
Fin
F
b
=
suc
F
A
Proof
Step
Hyp
Ref
Expression
1
ackbij.f
ω
⊢
F
=
x
∈
𝒫
ω
∩
Fin
⟼
card
⋃
y
∈
x
y
×
𝒫
y
2
difss
ω
⊢
A
∖
⋂
ω
∖
A
⊆
A
3
1
ackbij1lem11
ω
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
∧
A
∖
⋂
ω
∖
A
⊆
A
→
A
∖
⋂
ω
∖
A
∈
𝒫
ω
∩
Fin
4
2
3
mpan2
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
A
∖
⋂
ω
∖
A
∈
𝒫
ω
∩
Fin
5
difss
ω
ω
⊢
ω
∖
A
⊆
ω
6
omsson
ω
⊢
ω
⊆
On
7
5
6
sstri
ω
⊢
ω
∖
A
⊆
On
8
ominf
ω
⊢
¬
ω
∈
Fin
9
elinel2
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
A
∈
Fin
10
difinf
ω
ω
⊢
¬
ω
∈
Fin
∧
A
∈
Fin
→
¬
ω
∖
A
∈
Fin
11
8
9
10
sylancr
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
¬
ω
∖
A
∈
Fin
12
0fin
⊢
∅
∈
Fin
13
eleq1
ω
ω
⊢
ω
∖
A
=
∅
→
ω
∖
A
∈
Fin
↔
∅
∈
Fin
14
12
13
mpbiri
ω
ω
⊢
ω
∖
A
=
∅
→
ω
∖
A
∈
Fin
15
14
necon3bi
ω
ω
⊢
¬
ω
∖
A
∈
Fin
→
ω
∖
A
≠
∅
16
11
15
syl
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
ω
∖
A
≠
∅
17
onint
ω
ω
ω
ω
⊢
ω
∖
A
⊆
On
∧
ω
∖
A
≠
∅
→
⋂
ω
∖
A
∈
ω
∖
A
18
7
16
17
sylancr
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
⋂
ω
∖
A
∈
ω
∖
A
19
18
eldifad
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
⋂
ω
∖
A
∈
ω
20
ackbij1lem4
ω
ω
ω
ω
⊢
⋂
ω
∖
A
∈
ω
→
⋂
ω
∖
A
∈
𝒫
ω
∩
Fin
21
19
20
syl
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
⋂
ω
∖
A
∈
𝒫
ω
∩
Fin
22
ackbij1lem6
ω
ω
ω
ω
ω
ω
ω
⊢
A
∖
⋂
ω
∖
A
∈
𝒫
ω
∩
Fin
∧
⋂
ω
∖
A
∈
𝒫
ω
∩
Fin
→
A
∖
⋂
ω
∖
A
∪
⋂
ω
∖
A
∈
𝒫
ω
∩
Fin
23
4
21
22
syl2anc
ω
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
A
∖
⋂
ω
∖
A
∪
⋂
ω
∖
A
∈
𝒫
ω
∩
Fin
24
18
eldifbd
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
¬
⋂
ω
∖
A
∈
A
25
disjsn
ω
ω
⊢
A
∩
⋂
ω
∖
A
=
∅
↔
¬
⋂
ω
∖
A
∈
A
26
24
25
sylibr
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
A
∩
⋂
ω
∖
A
=
∅
27
ssdisj
ω
ω
ω
ω
⊢
A
∖
⋂
ω
∖
A
⊆
A
∧
A
∩
⋂
ω
∖
A
=
∅
→
A
∖
⋂
ω
∖
A
∩
⋂
ω
∖
A
=
∅
28
2
26
27
sylancr
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
A
∖
⋂
ω
∖
A
∩
⋂
ω
∖
A
=
∅
29
1
ackbij1lem9
ω
ω
ω
ω
ω
ω
ω
ω
ω
ω
⊢
A
∖
⋂
ω
∖
A
∈
𝒫
ω
∩
Fin
∧
⋂
ω
∖
A
∈
𝒫
ω
∩
Fin
∧
A
∖
⋂
ω
∖
A
∩
⋂
ω
∖
A
=
∅
→
F
A
∖
⋂
ω
∖
A
∪
⋂
ω
∖
A
=
F
A
∖
⋂
ω
∖
A
+
𝑜
F
⋂
ω
∖
A
30
4
21
28
29
syl3anc
ω
ω
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
F
A
∖
⋂
ω
∖
A
∪
⋂
ω
∖
A
=
F
A
∖
⋂
ω
∖
A
+
𝑜
F
⋂
ω
∖
A
31
1
ackbij1lem14
ω
ω
ω
ω
⊢
⋂
ω
∖
A
∈
ω
→
F
⋂
ω
∖
A
=
suc
F
⋂
ω
∖
A
32
19
31
syl
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
F
⋂
ω
∖
A
=
suc
F
⋂
ω
∖
A
33
32
oveq2d
ω
ω
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
F
A
∖
⋂
ω
∖
A
+
𝑜
F
⋂
ω
∖
A
=
F
A
∖
⋂
ω
∖
A
+
𝑜
suc
F
⋂
ω
∖
A
34
1
ackbij1lem10
ω
ω
⊢
F
:
𝒫
ω
∩
Fin
⟶
ω
35
34
ffvelrni
ω
ω
ω
ω
⊢
A
∖
⋂
ω
∖
A
∈
𝒫
ω
∩
Fin
→
F
A
∖
⋂
ω
∖
A
∈
ω
36
4
35
syl
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
F
A
∖
⋂
ω
∖
A
∈
ω
37
ackbij1lem3
ω
ω
ω
ω
⊢
⋂
ω
∖
A
∈
ω
→
⋂
ω
∖
A
∈
𝒫
ω
∩
Fin
38
19
37
syl
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
⋂
ω
∖
A
∈
𝒫
ω
∩
Fin
39
34
ffvelrni
ω
ω
ω
ω
⊢
⋂
ω
∖
A
∈
𝒫
ω
∩
Fin
→
F
⋂
ω
∖
A
∈
ω
40
38
39
syl
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
F
⋂
ω
∖
A
∈
ω
41
nnasuc
ω
ω
ω
ω
ω
ω
ω
ω
⊢
F
A
∖
⋂
ω
∖
A
∈
ω
∧
F
⋂
ω
∖
A
∈
ω
→
F
A
∖
⋂
ω
∖
A
+
𝑜
suc
F
⋂
ω
∖
A
=
suc
F
A
∖
⋂
ω
∖
A
+
𝑜
F
⋂
ω
∖
A
42
36
40
41
syl2anc
ω
ω
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
F
A
∖
⋂
ω
∖
A
+
𝑜
suc
F
⋂
ω
∖
A
=
suc
F
A
∖
⋂
ω
∖
A
+
𝑜
F
⋂
ω
∖
A
43
disjdifr
ω
ω
⊢
A
∖
⋂
ω
∖
A
∩
⋂
ω
∖
A
=
∅
44
43
a1i
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
A
∖
⋂
ω
∖
A
∩
⋂
ω
∖
A
=
∅
45
1
ackbij1lem9
ω
ω
ω
ω
ω
ω
ω
ω
ω
ω
⊢
A
∖
⋂
ω
∖
A
∈
𝒫
ω
∩
Fin
∧
⋂
ω
∖
A
∈
𝒫
ω
∩
Fin
∧
A
∖
⋂
ω
∖
A
∩
⋂
ω
∖
A
=
∅
→
F
A
∖
⋂
ω
∖
A
∪
⋂
ω
∖
A
=
F
A
∖
⋂
ω
∖
A
+
𝑜
F
⋂
ω
∖
A
46
4
38
44
45
syl3anc
ω
ω
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
F
A
∖
⋂
ω
∖
A
∪
⋂
ω
∖
A
=
F
A
∖
⋂
ω
∖
A
+
𝑜
F
⋂
ω
∖
A
47
uncom
ω
ω
ω
ω
⊢
A
∖
⋂
ω
∖
A
∪
⋂
ω
∖
A
=
⋂
ω
∖
A
∪
A
∖
⋂
ω
∖
A
48
onnmin
ω
ω
ω
⊢
ω
∖
A
⊆
On
∧
a
∈
ω
∖
A
→
¬
a
∈
⋂
ω
∖
A
49
7
48
mpan
ω
ω
⊢
a
∈
ω
∖
A
→
¬
a
∈
⋂
ω
∖
A
50
49
con2i
ω
ω
⊢
a
∈
⋂
ω
∖
A
→
¬
a
∈
ω
∖
A
51
50
adantl
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
∧
a
∈
⋂
ω
∖
A
→
¬
a
∈
ω
∖
A
52
ordom
ω
⊢
Ord
ω
53
ordelss
ω
ω
ω
ω
ω
⊢
Ord
ω
∧
⋂
ω
∖
A
∈
ω
→
⋂
ω
∖
A
⊆
ω
54
52
19
53
sylancr
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
⋂
ω
∖
A
⊆
ω
55
54
sselda
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
∧
a
∈
⋂
ω
∖
A
→
a
∈
ω
56
eldif
ω
ω
⊢
a
∈
ω
∖
A
↔
a
∈
ω
∧
¬
a
∈
A
57
56
simplbi2
ω
ω
⊢
a
∈
ω
→
¬
a
∈
A
→
a
∈
ω
∖
A
58
57
orrd
ω
ω
⊢
a
∈
ω
→
a
∈
A
∨
a
∈
ω
∖
A
59
58
orcomd
ω
ω
⊢
a
∈
ω
→
a
∈
ω
∖
A
∨
a
∈
A
60
55
59
syl
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
∧
a
∈
⋂
ω
∖
A
→
a
∈
ω
∖
A
∨
a
∈
A
61
orel1
ω
ω
⊢
¬
a
∈
ω
∖
A
→
a
∈
ω
∖
A
∨
a
∈
A
→
a
∈
A
62
51
60
61
sylc
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
∧
a
∈
⋂
ω
∖
A
→
a
∈
A
63
62
ex
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
a
∈
⋂
ω
∖
A
→
a
∈
A
64
63
ssrdv
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
⋂
ω
∖
A
⊆
A
65
undif
ω
ω
ω
⊢
⋂
ω
∖
A
⊆
A
↔
⋂
ω
∖
A
∪
A
∖
⋂
ω
∖
A
=
A
66
64
65
sylib
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
⋂
ω
∖
A
∪
A
∖
⋂
ω
∖
A
=
A
67
47
66
eqtrid
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
A
∖
⋂
ω
∖
A
∪
⋂
ω
∖
A
=
A
68
67
fveq2d
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
F
A
∖
⋂
ω
∖
A
∪
⋂
ω
∖
A
=
F
A
69
46
68
eqtr3d
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
F
A
∖
⋂
ω
∖
A
+
𝑜
F
⋂
ω
∖
A
=
F
A
70
suceq
ω
ω
ω
ω
⊢
F
A
∖
⋂
ω
∖
A
+
𝑜
F
⋂
ω
∖
A
=
F
A
→
suc
F
A
∖
⋂
ω
∖
A
+
𝑜
F
⋂
ω
∖
A
=
suc
F
A
71
69
70
syl
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
suc
F
A
∖
⋂
ω
∖
A
+
𝑜
F
⋂
ω
∖
A
=
suc
F
A
72
42
71
eqtrd
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
F
A
∖
⋂
ω
∖
A
+
𝑜
suc
F
⋂
ω
∖
A
=
suc
F
A
73
30
33
72
3eqtrd
ω
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
F
A
∖
⋂
ω
∖
A
∪
⋂
ω
∖
A
=
suc
F
A
74
fveqeq2
ω
ω
ω
ω
⊢
b
=
A
∖
⋂
ω
∖
A
∪
⋂
ω
∖
A
→
F
b
=
suc
F
A
↔
F
A
∖
⋂
ω
∖
A
∪
⋂
ω
∖
A
=
suc
F
A
75
74
rspcev
ω
ω
ω
ω
ω
ω
⊢
A
∖
⋂
ω
∖
A
∪
⋂
ω
∖
A
∈
𝒫
ω
∩
Fin
∧
F
A
∖
⋂
ω
∖
A
∪
⋂
ω
∖
A
=
suc
F
A
→
∃
b
∈
𝒫
ω
∩
Fin
F
b
=
suc
F
A
76
23
73
75
syl2anc
ω
ω
⊢
A
∈
𝒫
ω
∩
Fin
→
∃
b
∈
𝒫
ω
∩
Fin
F
b
=
suc
F
A