Step |
Hyp |
Ref |
Expression |
1 |
|
onelon |
|- ( ( z e. On /\ y e. z ) -> y e. On ) |
2 |
|
vex |
|- z e. _V |
3 |
|
onelss |
|- ( z e. On -> ( y e. z -> y C_ z ) ) |
4 |
3
|
imp |
|- ( ( z e. On /\ y e. z ) -> y C_ z ) |
5 |
|
ssdomg |
|- ( z e. _V -> ( y C_ z -> y ~<_ z ) ) |
6 |
2 4 5
|
mpsyl |
|- ( ( z e. On /\ y e. z ) -> y ~<_ z ) |
7 |
1 6
|
jca |
|- ( ( z e. On /\ y e. z ) -> ( y e. On /\ y ~<_ z ) ) |
8 |
|
domsdomtr |
|- ( ( y ~<_ z /\ z ~< A ) -> y ~< A ) |
9 |
8
|
anim2i |
|- ( ( y e. On /\ ( y ~<_ z /\ z ~< A ) ) -> ( y e. On /\ y ~< A ) ) |
10 |
9
|
anassrs |
|- ( ( ( y e. On /\ y ~<_ z ) /\ z ~< A ) -> ( y e. On /\ y ~< A ) ) |
11 |
7 10
|
sylan |
|- ( ( ( z e. On /\ y e. z ) /\ z ~< A ) -> ( y e. On /\ y ~< A ) ) |
12 |
11
|
exp31 |
|- ( z e. On -> ( y e. z -> ( z ~< A -> ( y e. On /\ y ~< A ) ) ) ) |
13 |
12
|
com12 |
|- ( y e. z -> ( z e. On -> ( z ~< A -> ( y e. On /\ y ~< A ) ) ) ) |
14 |
13
|
impd |
|- ( y e. z -> ( ( z e. On /\ z ~< A ) -> ( y e. On /\ y ~< A ) ) ) |
15 |
|
breq1 |
|- ( x = z -> ( x ~< A <-> z ~< A ) ) |
16 |
15
|
elrab |
|- ( z e. { x e. On | x ~< A } <-> ( z e. On /\ z ~< A ) ) |
17 |
|
breq1 |
|- ( x = y -> ( x ~< A <-> y ~< A ) ) |
18 |
17
|
elrab |
|- ( y e. { x e. On | x ~< A } <-> ( y e. On /\ y ~< A ) ) |
19 |
14 16 18
|
3imtr4g |
|- ( y e. z -> ( z e. { x e. On | x ~< A } -> y e. { x e. On | x ~< A } ) ) |
20 |
19
|
imp |
|- ( ( y e. z /\ z e. { x e. On | x ~< A } ) -> y e. { x e. On | x ~< A } ) |
21 |
20
|
gen2 |
|- A. y A. z ( ( y e. z /\ z e. { x e. On | x ~< A } ) -> y e. { x e. On | x ~< A } ) |
22 |
|
dftr2 |
|- ( Tr { x e. On | x ~< A } <-> A. y A. z ( ( y e. z /\ z e. { x e. On | x ~< A } ) -> y e. { x e. On | x ~< A } ) ) |
23 |
21 22
|
mpbir |
|- Tr { x e. On | x ~< A } |
24 |
|
ssrab2 |
|- { x e. On | x ~< A } C_ On |
25 |
|
ordon |
|- Ord On |
26 |
|
trssord |
|- ( ( Tr { x e. On | x ~< A } /\ { x e. On | x ~< A } C_ On /\ Ord On ) -> Ord { x e. On | x ~< A } ) |
27 |
23 24 25 26
|
mp3an |
|- Ord { x e. On | x ~< A } |
28 |
|
hartogs |
|- ( A e. _V -> { x e. On | x ~<_ A } e. On ) |
29 |
|
sdomdom |
|- ( x ~< A -> x ~<_ A ) |
30 |
29
|
a1i |
|- ( x e. On -> ( x ~< A -> x ~<_ A ) ) |
31 |
30
|
ss2rabi |
|- { x e. On | x ~< A } C_ { x e. On | x ~<_ A } |
32 |
|
ssexg |
|- ( ( { x e. On | x ~< A } C_ { x e. On | x ~<_ A } /\ { x e. On | x ~<_ A } e. On ) -> { x e. On | x ~< A } e. _V ) |
33 |
31 32
|
mpan |
|- ( { x e. On | x ~<_ A } e. On -> { x e. On | x ~< A } e. _V ) |
34 |
|
elong |
|- ( { x e. On | x ~< A } e. _V -> ( { x e. On | x ~< A } e. On <-> Ord { x e. On | x ~< A } ) ) |
35 |
28 33 34
|
3syl |
|- ( A e. _V -> ( { x e. On | x ~< A } e. On <-> Ord { x e. On | x ~< A } ) ) |
36 |
27 35
|
mpbiri |
|- ( A e. _V -> { x e. On | x ~< A } e. On ) |
37 |
|
0elon |
|- (/) e. On |
38 |
|
eleq1 |
|- ( { x e. On | x ~< A } = (/) -> ( { x e. On | x ~< A } e. On <-> (/) e. On ) ) |
39 |
37 38
|
mpbiri |
|- ( { x e. On | x ~< A } = (/) -> { x e. On | x ~< A } e. On ) |
40 |
|
df-ne |
|- ( { x e. On | x ~< A } =/= (/) <-> -. { x e. On | x ~< A } = (/) ) |
41 |
|
rabn0 |
|- ( { x e. On | x ~< A } =/= (/) <-> E. x e. On x ~< A ) |
42 |
40 41
|
bitr3i |
|- ( -. { x e. On | x ~< A } = (/) <-> E. x e. On x ~< A ) |
43 |
|
relsdom |
|- Rel ~< |
44 |
43
|
brrelex2i |
|- ( x ~< A -> A e. _V ) |
45 |
44
|
rexlimivw |
|- ( E. x e. On x ~< A -> A e. _V ) |
46 |
42 45
|
sylbi |
|- ( -. { x e. On | x ~< A } = (/) -> A e. _V ) |
47 |
39 46
|
nsyl4 |
|- ( -. A e. _V -> { x e. On | x ~< A } e. On ) |
48 |
36 47
|
pm2.61i |
|- { x e. On | x ~< A } e. On |