Step |
Hyp |
Ref |
Expression |
1 |
|
sdomdom |
|- ( ~P x ~< A -> ~P x ~<_ A ) |
2 |
|
ondomen |
|- ( ( A e. On /\ ~P x ~<_ A ) -> ~P x e. dom card ) |
3 |
|
isnum2 |
|- ( ~P x e. dom card <-> E. y e. On y ~~ ~P x ) |
4 |
2 3
|
sylib |
|- ( ( A e. On /\ ~P x ~<_ A ) -> E. y e. On y ~~ ~P x ) |
5 |
1 4
|
sylan2 |
|- ( ( A e. On /\ ~P x ~< A ) -> E. y e. On y ~~ ~P x ) |
6 |
|
ensdomtr |
|- ( ( y ~~ ~P x /\ ~P x ~< A ) -> y ~< A ) |
7 |
6
|
ad2ant2l |
|- ( ( ( y e. On /\ y ~~ ~P x ) /\ ( A e. On /\ ~P x ~< A ) ) -> y ~< A ) |
8 |
|
sdomel |
|- ( ( y e. On /\ A e. On ) -> ( y ~< A -> y e. A ) ) |
9 |
8
|
ad2ant2r |
|- ( ( ( y e. On /\ y ~~ ~P x ) /\ ( A e. On /\ ~P x ~< A ) ) -> ( y ~< A -> y e. A ) ) |
10 |
7 9
|
mpd |
|- ( ( ( y e. On /\ y ~~ ~P x ) /\ ( A e. On /\ ~P x ~< A ) ) -> y e. A ) |
11 |
|
vex |
|- x e. _V |
12 |
11
|
canth2 |
|- x ~< ~P x |
13 |
|
ensym |
|- ( y ~~ ~P x -> ~P x ~~ y ) |
14 |
|
sdomentr |
|- ( ( x ~< ~P x /\ ~P x ~~ y ) -> x ~< y ) |
15 |
12 13 14
|
sylancr |
|- ( y ~~ ~P x -> x ~< y ) |
16 |
15
|
ad2antlr |
|- ( ( ( y e. On /\ y ~~ ~P x ) /\ ( A e. On /\ ~P x ~< A ) ) -> x ~< y ) |
17 |
10 16
|
jca |
|- ( ( ( y e. On /\ y ~~ ~P x ) /\ ( A e. On /\ ~P x ~< A ) ) -> ( y e. A /\ x ~< y ) ) |
18 |
17
|
expcom |
|- ( ( A e. On /\ ~P x ~< A ) -> ( ( y e. On /\ y ~~ ~P x ) -> ( y e. A /\ x ~< y ) ) ) |
19 |
18
|
reximdv2 |
|- ( ( A e. On /\ ~P x ~< A ) -> ( E. y e. On y ~~ ~P x -> E. y e. A x ~< y ) ) |
20 |
5 19
|
mpd |
|- ( ( A e. On /\ ~P x ~< A ) -> E. y e. A x ~< y ) |
21 |
20
|
ex |
|- ( A e. On -> ( ~P x ~< A -> E. y e. A x ~< y ) ) |
22 |
21
|
ralimdv |
|- ( A e. On -> ( A. x e. A ~P x ~< A -> A. x e. A E. y e. A x ~< y ) ) |