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