Metamath Proof Explorer

Theorem inawinalem

Description: Lemma for inawina . (Contributed by Mario Carneiro, 8-Jun-2014)

Ref Expression
Assertion inawinalem 
|- ( A e. On -> ( A. x e. A ~P x ~< A -> A. x e. A E. y e. A x ~< y ) )

Proof

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 ) )