Database
ZFC (ZERMELO-FRAENKEL WITH CHOICE) SET THEORY
ZFC Set Theory - add Countable Choice and Dependent Choice
Introduce the Axiom of Countable Choice
axcc2lem
Next ⟩
axcc2
Metamath Proof Explorer
Ascii
Unicode
Theorem
axcc2lem
Description:
Lemma for
axcc2
.
(Contributed by
Mario Carneiro
, 8-Feb-2013)
Ref
Expression
Hypotheses
axcc2lem.1
ω
⊢
K
=
n
∈
ω
⟼
if
F
n
=
∅
∅
F
n
axcc2lem.2
ω
⊢
A
=
n
∈
ω
⟼
n
×
K
n
axcc2lem.3
ω
⊢
G
=
n
∈
ω
⟼
2
nd
f
A
n
Assertion
axcc2lem
ω
ω
⊢
∃
g
g
Fn
ω
∧
∀
n
∈
ω
F
n
≠
∅
→
g
n
∈
F
n
Proof
Step
Hyp
Ref
Expression
1
axcc2lem.1
ω
⊢
K
=
n
∈
ω
⟼
if
F
n
=
∅
∅
F
n
2
axcc2lem.2
ω
⊢
A
=
n
∈
ω
⟼
n
×
K
n
3
axcc2lem.3
ω
⊢
G
=
n
∈
ω
⟼
2
nd
f
A
n
4
fvex
⊢
2
nd
f
A
n
∈
V
5
4
3
fnmpti
ω
⊢
G
Fn
ω
6
snex
⊢
n
∈
V
7
fvex
⊢
K
n
∈
V
8
6
7
xpex
⊢
n
×
K
n
∈
V
9
2
fvmpt2
ω
⊢
n
∈
ω
∧
n
×
K
n
∈
V
→
A
n
=
n
×
K
n
10
8
9
mpan2
ω
⊢
n
∈
ω
→
A
n
=
n
×
K
n
11
vex
⊢
n
∈
V
12
11
snnz
⊢
n
≠
∅
13
0ex
⊢
∅
∈
V
14
13
snnz
⊢
∅
≠
∅
15
iftrue
⊢
F
n
=
∅
→
if
F
n
=
∅
∅
F
n
=
∅
16
15
neeq1d
⊢
F
n
=
∅
→
if
F
n
=
∅
∅
F
n
≠
∅
↔
∅
≠
∅
17
14
16
mpbiri
⊢
F
n
=
∅
→
if
F
n
=
∅
∅
F
n
≠
∅
18
iffalse
⊢
¬
F
n
=
∅
→
if
F
n
=
∅
∅
F
n
=
F
n
19
neqne
⊢
¬
F
n
=
∅
→
F
n
≠
∅
20
18
19
eqnetrd
⊢
¬
F
n
=
∅
→
if
F
n
=
∅
∅
F
n
≠
∅
21
17
20
pm2.61i
⊢
if
F
n
=
∅
∅
F
n
≠
∅
22
p0ex
⊢
∅
∈
V
23
fvex
⊢
F
n
∈
V
24
22
23
ifex
⊢
if
F
n
=
∅
∅
F
n
∈
V
25
1
fvmpt2
ω
⊢
n
∈
ω
∧
if
F
n
=
∅
∅
F
n
∈
V
→
K
n
=
if
F
n
=
∅
∅
F
n
26
24
25
mpan2
ω
⊢
n
∈
ω
→
K
n
=
if
F
n
=
∅
∅
F
n
27
26
neeq1d
ω
⊢
n
∈
ω
→
K
n
≠
∅
↔
if
F
n
=
∅
∅
F
n
≠
∅
28
21
27
mpbiri
ω
⊢
n
∈
ω
→
K
n
≠
∅
29
xpnz
⊢
n
≠
∅
∧
K
n
≠
∅
↔
n
×
K
n
≠
∅
30
29
biimpi
⊢
n
≠
∅
∧
K
n
≠
∅
→
n
×
K
n
≠
∅
31
12
28
30
sylancr
ω
⊢
n
∈
ω
→
n
×
K
n
≠
∅
32
10
31
eqnetrd
ω
⊢
n
∈
ω
→
A
n
≠
∅
33
8
2
fnmpti
ω
⊢
A
Fn
ω
34
fnfvelrn
ω
ω
⊢
A
Fn
ω
∧
n
∈
ω
→
A
n
∈
ran
A
35
33
34
mpan
ω
⊢
n
∈
ω
→
A
n
∈
ran
A
36
neeq1
⊢
z
=
A
n
→
z
≠
∅
↔
A
n
≠
∅
37
fveq2
⊢
z
=
A
n
→
f
z
=
f
A
n
38
id
⊢
z
=
A
n
→
z
=
A
n
39
37
38
eleq12d
⊢
z
=
A
n
→
f
z
∈
z
↔
f
A
n
∈
A
n
40
36
39
imbi12d
⊢
z
=
A
n
→
z
≠
∅
→
f
z
∈
z
↔
A
n
≠
∅
→
f
A
n
∈
A
n
41
40
rspccv
⊢
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
→
A
n
∈
ran
A
→
A
n
≠
∅
→
f
A
n
∈
A
n
42
35
41
syl5
ω
⊢
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
→
n
∈
ω
→
A
n
≠
∅
→
f
A
n
∈
A
n
43
32
42
mpdi
ω
⊢
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
→
n
∈
ω
→
f
A
n
∈
A
n
44
43
impcom
ω
⊢
n
∈
ω
∧
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
→
f
A
n
∈
A
n
45
10
eleq2d
ω
⊢
n
∈
ω
→
f
A
n
∈
A
n
↔
f
A
n
∈
n
×
K
n
46
45
adantr
ω
⊢
n
∈
ω
∧
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
→
f
A
n
∈
A
n
↔
f
A
n
∈
n
×
K
n
47
44
46
mpbid
ω
⊢
n
∈
ω
∧
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
→
f
A
n
∈
n
×
K
n
48
xp2nd
⊢
f
A
n
∈
n
×
K
n
→
2
nd
f
A
n
∈
K
n
49
47
48
syl
ω
⊢
n
∈
ω
∧
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
→
2
nd
f
A
n
∈
K
n
50
49
3adant3
ω
⊢
n
∈
ω
∧
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
∧
F
n
≠
∅
→
2
nd
f
A
n
∈
K
n
51
3
fvmpt2
ω
⊢
n
∈
ω
∧
2
nd
f
A
n
∈
V
→
G
n
=
2
nd
f
A
n
52
4
51
mpan2
ω
⊢
n
∈
ω
→
G
n
=
2
nd
f
A
n
53
52
3ad2ant1
ω
⊢
n
∈
ω
∧
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
∧
F
n
≠
∅
→
G
n
=
2
nd
f
A
n
54
53
eqcomd
ω
⊢
n
∈
ω
∧
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
∧
F
n
≠
∅
→
2
nd
f
A
n
=
G
n
55
26
3ad2ant1
ω
⊢
n
∈
ω
∧
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
∧
F
n
≠
∅
→
K
n
=
if
F
n
=
∅
∅
F
n
56
ifnefalse
⊢
F
n
≠
∅
→
if
F
n
=
∅
∅
F
n
=
F
n
57
56
3ad2ant3
ω
⊢
n
∈
ω
∧
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
∧
F
n
≠
∅
→
if
F
n
=
∅
∅
F
n
=
F
n
58
55
57
eqtrd
ω
⊢
n
∈
ω
∧
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
∧
F
n
≠
∅
→
K
n
=
F
n
59
50
54
58
3eltr3d
ω
⊢
n
∈
ω
∧
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
∧
F
n
≠
∅
→
G
n
∈
F
n
60
59
3expia
ω
⊢
n
∈
ω
∧
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
→
F
n
≠
∅
→
G
n
∈
F
n
61
60
expcom
ω
⊢
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
→
n
∈
ω
→
F
n
≠
∅
→
G
n
∈
F
n
62
61
ralrimiv
ω
⊢
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
→
∀
n
∈
ω
F
n
≠
∅
→
G
n
∈
F
n
63
omex
ω
⊢
ω
∈
V
64
fnex
ω
ω
⊢
G
Fn
ω
∧
ω
∈
V
→
G
∈
V
65
5
63
64
mp2an
⊢
G
∈
V
66
fneq1
ω
ω
⊢
g
=
G
→
g
Fn
ω
↔
G
Fn
ω
67
fveq1
⊢
g
=
G
→
g
n
=
G
n
68
67
eleq1d
⊢
g
=
G
→
g
n
∈
F
n
↔
G
n
∈
F
n
69
68
imbi2d
⊢
g
=
G
→
F
n
≠
∅
→
g
n
∈
F
n
↔
F
n
≠
∅
→
G
n
∈
F
n
70
69
ralbidv
ω
ω
⊢
g
=
G
→
∀
n
∈
ω
F
n
≠
∅
→
g
n
∈
F
n
↔
∀
n
∈
ω
F
n
≠
∅
→
G
n
∈
F
n
71
66
70
anbi12d
ω
ω
ω
ω
⊢
g
=
G
→
g
Fn
ω
∧
∀
n
∈
ω
F
n
≠
∅
→
g
n
∈
F
n
↔
G
Fn
ω
∧
∀
n
∈
ω
F
n
≠
∅
→
G
n
∈
F
n
72
65
71
spcev
ω
ω
ω
ω
⊢
G
Fn
ω
∧
∀
n
∈
ω
F
n
≠
∅
→
G
n
∈
F
n
→
∃
g
g
Fn
ω
∧
∀
n
∈
ω
F
n
≠
∅
→
g
n
∈
F
n
73
5
62
72
sylancr
ω
ω
⊢
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
→
∃
g
g
Fn
ω
∧
∀
n
∈
ω
F
n
≠
∅
→
g
n
∈
F
n
74
8
a1i
ω
ω
⊢
ω
∈
V
∧
n
∈
ω
→
n
×
K
n
∈
V
75
74
2
fmptd
ω
ω
⊢
ω
∈
V
→
A
:
ω
⟶
V
76
63
75
ax-mp
ω
⊢
A
:
ω
⟶
V
77
sneq
⊢
n
=
k
→
n
=
k
78
fveq2
⊢
n
=
k
→
K
n
=
K
k
79
77
78
xpeq12d
⊢
n
=
k
→
n
×
K
n
=
k
×
K
k
80
79
2
8
fvmpt3i
ω
⊢
k
∈
ω
→
A
k
=
k
×
K
k
81
80
adantl
ω
ω
⊢
n
∈
ω
∧
k
∈
ω
→
A
k
=
k
×
K
k
82
81
eqeq2d
ω
ω
⊢
n
∈
ω
∧
k
∈
ω
→
A
n
=
A
k
↔
A
n
=
k
×
K
k
83
10
adantr
ω
ω
⊢
n
∈
ω
∧
k
∈
ω
→
A
n
=
n
×
K
n
84
83
eqeq1d
ω
ω
⊢
n
∈
ω
∧
k
∈
ω
→
A
n
=
k
×
K
k
↔
n
×
K
n
=
k
×
K
k
85
xp11
⊢
n
≠
∅
∧
K
n
≠
∅
→
n
×
K
n
=
k
×
K
k
↔
n
=
k
∧
K
n
=
K
k
86
12
28
85
sylancr
ω
⊢
n
∈
ω
→
n
×
K
n
=
k
×
K
k
↔
n
=
k
∧
K
n
=
K
k
87
11
sneqr
⊢
n
=
k
→
n
=
k
88
87
adantr
⊢
n
=
k
∧
K
n
=
K
k
→
n
=
k
89
86
88
syl6bi
ω
⊢
n
∈
ω
→
n
×
K
n
=
k
×
K
k
→
n
=
k
90
89
adantr
ω
ω
⊢
n
∈
ω
∧
k
∈
ω
→
n
×
K
n
=
k
×
K
k
→
n
=
k
91
84
90
sylbid
ω
ω
⊢
n
∈
ω
∧
k
∈
ω
→
A
n
=
k
×
K
k
→
n
=
k
92
82
91
sylbid
ω
ω
⊢
n
∈
ω
∧
k
∈
ω
→
A
n
=
A
k
→
n
=
k
93
92
rgen2
ω
ω
⊢
∀
n
∈
ω
∀
k
∈
ω
A
n
=
A
k
→
n
=
k
94
dff13
ω
ω
ω
ω
⊢
A
:
ω
⟶
1-1
V
↔
A
:
ω
⟶
V
∧
∀
n
∈
ω
∀
k
∈
ω
A
n
=
A
k
→
n
=
k
95
76
93
94
mpbir2an
ω
⊢
A
:
ω
⟶
1-1
V
96
f1f1orn
ω
ω
⊢
A
:
ω
⟶
1-1
V
→
A
:
ω
⟶
1-1 onto
ran
A
97
63
f1oen
ω
ω
⊢
A
:
ω
⟶
1-1 onto
ran
A
→
ω
≈
ran
A
98
ensym
ω
ω
⊢
ω
≈
ran
A
→
ran
A
≈
ω
99
96
97
98
3syl
ω
ω
⊢
A
:
ω
⟶
1-1
V
→
ran
A
≈
ω
100
2
rneqi
ω
⊢
ran
A
=
ran
n
∈
ω
⟼
n
×
K
n
101
dmmptg
ω
ω
ω
⊢
∀
n
∈
ω
n
×
K
n
∈
V
→
dom
n
∈
ω
⟼
n
×
K
n
=
ω
102
8
a1i
ω
⊢
n
∈
ω
→
n
×
K
n
∈
V
103
101
102
mprg
ω
ω
⊢
dom
n
∈
ω
⟼
n
×
K
n
=
ω
104
103
63
eqeltri
ω
⊢
dom
n
∈
ω
⟼
n
×
K
n
∈
V
105
funmpt
ω
⊢
Fun
n
∈
ω
⟼
n
×
K
n
106
funrnex
ω
ω
ω
⊢
dom
n
∈
ω
⟼
n
×
K
n
∈
V
→
Fun
n
∈
ω
⟼
n
×
K
n
→
ran
n
∈
ω
⟼
n
×
K
n
∈
V
107
104
105
106
mp2
ω
⊢
ran
n
∈
ω
⟼
n
×
K
n
∈
V
108
100
107
eqeltri
⊢
ran
A
∈
V
109
breq1
ω
ω
⊢
a
=
ran
A
→
a
≈
ω
↔
ran
A
≈
ω
110
raleq
⊢
a
=
ran
A
→
∀
z
∈
a
z
≠
∅
→
f
z
∈
z
↔
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
111
110
exbidv
⊢
a
=
ran
A
→
∃
f
∀
z
∈
a
z
≠
∅
→
f
z
∈
z
↔
∃
f
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
112
109
111
imbi12d
ω
ω
⊢
a
=
ran
A
→
a
≈
ω
→
∃
f
∀
z
∈
a
z
≠
∅
→
f
z
∈
z
↔
ran
A
≈
ω
→
∃
f
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
113
ax-cc
ω
⊢
a
≈
ω
→
∃
f
∀
z
∈
a
z
≠
∅
→
f
z
∈
z
114
108
112
113
vtocl
ω
⊢
ran
A
≈
ω
→
∃
f
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
115
95
99
114
mp2b
⊢
∃
f
∀
z
∈
ran
A
z
≠
∅
→
f
z
∈
z
116
73
115
exlimiiv
ω
ω
⊢
∃
g
g
Fn
ω
∧
∀
n
∈
ω
F
n
≠
∅
→
g
n
∈
F
n