Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Ordinal isomorphism, Hartogs's theorem
hartogslem2
Next ⟩
hartogs
Metamath Proof Explorer
Ascii
Unicode
Theorem
hartogslem2
Description:
Lemma for
hartogs
.
(Contributed by
Mario Carneiro
, 14-Jan-2013)
Ref
Expression
Hypotheses
hartogslem.2
⊢
F
=
r
y
|
dom
⁡
r
⊆
A
∧
I
↾
dom
⁡
r
⊆
r
∧
r
⊆
dom
⁡
r
×
dom
⁡
r
∧
r
∖
I
We
dom
⁡
r
∧
y
=
dom
⁡
OrdIso
r
∖
I
dom
⁡
r
hartogslem.3
⊢
R
=
s
t
|
∃
w
∈
y
∃
z
∈
y
s
=
f
⁡
w
∧
t
=
f
⁡
z
∧
w
E
z
Assertion
hartogslem2
⊢
A
∈
V
→
x
∈
On
|
x
≼
A
∈
V
Proof
Step
Hyp
Ref
Expression
1
hartogslem.2
⊢
F
=
r
y
|
dom
⁡
r
⊆
A
∧
I
↾
dom
⁡
r
⊆
r
∧
r
⊆
dom
⁡
r
×
dom
⁡
r
∧
r
∖
I
We
dom
⁡
r
∧
y
=
dom
⁡
OrdIso
r
∖
I
dom
⁡
r
2
hartogslem.3
⊢
R
=
s
t
|
∃
w
∈
y
∃
z
∈
y
s
=
f
⁡
w
∧
t
=
f
⁡
z
∧
w
E
z
3
1
2
hartogslem1
⊢
dom
⁡
F
⊆
𝒫
A
×
A
∧
Fun
⁡
F
∧
A
∈
V
→
ran
⁡
F
=
x
∈
On
|
x
≼
A
4
3
simp3i
⊢
A
∈
V
→
ran
⁡
F
=
x
∈
On
|
x
≼
A
5
3
simp2i
⊢
Fun
⁡
F
6
3
simp1i
⊢
dom
⁡
F
⊆
𝒫
A
×
A
7
sqxpexg
⊢
A
∈
V
→
A
×
A
∈
V
8
7
pwexd
⊢
A
∈
V
→
𝒫
A
×
A
∈
V
9
ssexg
⊢
dom
⁡
F
⊆
𝒫
A
×
A
∧
𝒫
A
×
A
∈
V
→
dom
⁡
F
∈
V
10
6
8
9
sylancr
⊢
A
∈
V
→
dom
⁡
F
∈
V
11
funex
⊢
Fun
⁡
F
∧
dom
⁡
F
∈
V
→
F
∈
V
12
5
10
11
sylancr
⊢
A
∈
V
→
F
∈
V
13
rnexg
⊢
F
∈
V
→
ran
⁡
F
∈
V
14
12
13
syl
⊢
A
∈
V
→
ran
⁡
F
∈
V
15
4
14
eqeltrrd
⊢
A
∈
V
→
x
∈
On
|
x
≼
A
∈
V