Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Infinity
Eight inequivalent definitions of finite set
isfin2
Next ⟩
fin2i
Metamath Proof Explorer
Ascii
Unicode
Theorem
isfin2
Description:
Definition of a II-finite set.
(Contributed by
Stefan O'Rear
, 16-May-2015)
Ref
Expression
Assertion
isfin2
⊢
A
∈
V
→
A
∈
Fin
II
↔
∀
y
∈
𝒫
𝒫
A
y
≠
∅
∧
[⊂]
Or
y
→
⋃
y
∈
y
Proof
Step
Hyp
Ref
Expression
1
pweq
⊢
z
=
x
→
𝒫
z
=
𝒫
x
2
1
pweqd
⊢
z
=
x
→
𝒫
𝒫
z
=
𝒫
𝒫
x
3
2
raleqdv
⊢
z
=
x
→
∀
y
∈
𝒫
𝒫
z
y
≠
∅
∧
[⊂]
Or
y
→
⋃
y
∈
y
↔
∀
y
∈
𝒫
𝒫
x
y
≠
∅
∧
[⊂]
Or
y
→
⋃
y
∈
y
4
pweq
⊢
x
=
A
→
𝒫
x
=
𝒫
A
5
4
pweqd
⊢
x
=
A
→
𝒫
𝒫
x
=
𝒫
𝒫
A
6
5
raleqdv
⊢
x
=
A
→
∀
y
∈
𝒫
𝒫
x
y
≠
∅
∧
[⊂]
Or
y
→
⋃
y
∈
y
↔
∀
y
∈
𝒫
𝒫
A
y
≠
∅
∧
[⊂]
Or
y
→
⋃
y
∈
y
7
df-fin2
⊢
Fin
II
=
z
|
∀
y
∈
𝒫
𝒫
z
y
≠
∅
∧
[⊂]
Or
y
→
⋃
y
∈
y
8
3
6
7
elab2gw
⊢
A
∈
V
→
A
∈
Fin
II
↔
∀
y
∈
𝒫
𝒫
A
y
≠
∅
∧
[⊂]
Or
y
→
⋃
y
∈
y