This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oawordeulem

Description: Lemma for oawordex . (Contributed by NM, 11-Dec-2004)

Ref Expression
Hypotheses oawordeulem.1 
|- A e. On
oawordeulem.2 
|- B e. On
oawordeulem.3 
|- S = { y e. On | B C_ ( A +o y ) }
Assertion oawordeulem 
|- ( A C_ B -> E! x e. On ( A +o x ) = B )

Proof

Step Hyp Ref Expression
1 oawordeulem.1 
 |-  A e. On
2 oawordeulem.2 
 |-  B e. On
3 oawordeulem.3 
 |-  S = { y e. On | B C_ ( A +o y ) }
4 3 ssrab3 
 |-  S C_ On
5 oaword2 
 |-  ( ( B e. On /\ A e. On ) -> B C_ ( A +o B ) )
6 2 1 5 mp2an 
 |-  B C_ ( A +o B )
7 oveq2 
 |-  ( y = B -> ( A +o y ) = ( A +o B ) )
8 7 sseq2d 
 |-  ( y = B -> ( B C_ ( A +o y ) <-> B C_ ( A +o B ) ) )
9 8 3 elrab2 
 |-  ( B e. S <-> ( B e. On /\ B C_ ( A +o B ) ) )
10 2 6 9 mpbir2an 
 |-  B e. S
11 10 ne0ii 
 |-  S =/= (/)
12 oninton 
 |-  ( ( S C_ On /\ S =/= (/) ) -> |^| S e. On )
13 4 11 12 mp2an 
 |-  |^| S e. On
14 onzsl 
 |-  ( |^| S e. On <-> ( |^| S = (/) \/ E. z e. On |^| S = suc z \/ ( |^| S e. _V /\ Lim |^| S ) ) )
15 13 14 mpbi 
 |-  ( |^| S = (/) \/ E. z e. On |^| S = suc z \/ ( |^| S e. _V /\ Lim |^| S ) )
16 oveq2 
 |-  ( |^| S = (/) -> ( A +o |^| S ) = ( A +o (/) ) )
17 oa0 
 |-  ( A e. On -> ( A +o (/) ) = A )
18 1 17 ax-mp 
 |-  ( A +o (/) ) = A
19 16 18 eqtrdi 
 |-  ( |^| S = (/) -> ( A +o |^| S ) = A )
20 19 sseq1d 
 |-  ( |^| S = (/) -> ( ( A +o |^| S ) C_ B <-> A C_ B ) )
21 20 biimprd 
 |-  ( |^| S = (/) -> ( A C_ B -> ( A +o |^| S ) C_ B ) )
22 oveq2 
 |-  ( |^| S = suc z -> ( A +o |^| S ) = ( A +o suc z ) )
23 oasuc 
 |-  ( ( A e. On /\ z e. On ) -> ( A +o suc z ) = suc ( A +o z ) )
24 1 23 mpan 
 |-  ( z e. On -> ( A +o suc z ) = suc ( A +o z ) )
25 22 24 sylan9eqr 
 |-  ( ( z e. On /\ |^| S = suc z ) -> ( A +o |^| S ) = suc ( A +o z ) )
26 vex 
 |-  z e. _V
27 26 sucid 
 |-  z e. suc z
28 eleq2 
 |-  ( |^| S = suc z -> ( z e. |^| S <-> z e. suc z ) )
29 27 28 mpbiri 
 |-  ( |^| S = suc z -> z e. |^| S )
30 13 oneli 
 |-  ( z e. |^| S -> z e. On )
31 3 inteqi 
 |-  |^| S = |^| { y e. On | B C_ ( A +o y ) }
32 31 eleq2i 
 |-  ( z e. |^| S <-> z e. |^| { y e. On | B C_ ( A +o y ) } )
33 oveq2 
 |-  ( y = z -> ( A +o y ) = ( A +o z ) )
34 33 sseq2d 
 |-  ( y = z -> ( B C_ ( A +o y ) <-> B C_ ( A +o z ) ) )
35 34 onnminsb 
 |-  ( z e. On -> ( z e. |^| { y e. On | B C_ ( A +o y ) } -> -. B C_ ( A +o z ) ) )
36 32 35 biimtrid 
 |-  ( z e. On -> ( z e. |^| S -> -. B C_ ( A +o z ) ) )
37 oacl 
 |-  ( ( A e. On /\ z e. On ) -> ( A +o z ) e. On )
38 1 37 mpan 
 |-  ( z e. On -> ( A +o z ) e. On )
39 ontri1 
 |-  ( ( B e. On /\ ( A +o z ) e. On ) -> ( B C_ ( A +o z ) <-> -. ( A +o z ) e. B ) )
40 2 38 39 sylancr 
 |-  ( z e. On -> ( B C_ ( A +o z ) <-> -. ( A +o z ) e. B ) )
41 40 con2bid 
 |-  ( z e. On -> ( ( A +o z ) e. B <-> -. B C_ ( A +o z ) ) )
42 36 41 sylibrd 
 |-  ( z e. On -> ( z e. |^| S -> ( A +o z ) e. B ) )
43 30 42 mpcom 
 |-  ( z e. |^| S -> ( A +o z ) e. B )
44 2 onordi 
 |-  Ord B
45 ordsucss 
 |-  ( Ord B -> ( ( A +o z ) e. B -> suc ( A +o z ) C_ B ) )
46 44 45 ax-mp 
 |-  ( ( A +o z ) e. B -> suc ( A +o z ) C_ B )
47 29 43 46 3syl 
 |-  ( |^| S = suc z -> suc ( A +o z ) C_ B )
48 47 adantl 
 |-  ( ( z e. On /\ |^| S = suc z ) -> suc ( A +o z ) C_ B )
49 25 48 eqsstrd 
 |-  ( ( z e. On /\ |^| S = suc z ) -> ( A +o |^| S ) C_ B )
50 49 rexlimiva 
 |-  ( E. z e. On |^| S = suc z -> ( A +o |^| S ) C_ B )
51 50 a1d 
 |-  ( E. z e. On |^| S = suc z -> ( A C_ B -> ( A +o |^| S ) C_ B ) )
52 oalim 
 |-  ( ( A e. On /\ ( |^| S e. _V /\ Lim |^| S ) ) -> ( A +o |^| S ) = U_ z e. |^| S ( A +o z ) )
53 1 52 mpan 
 |-  ( ( |^| S e. _V /\ Lim |^| S ) -> ( A +o |^| S ) = U_ z e. |^| S ( A +o z ) )
54 iunss 
 |-  ( U_ z e. |^| S ( A +o z ) C_ B <-> A. z e. |^| S ( A +o z ) C_ B )
55 2 onelssi 
 |-  ( ( A +o z ) e. B -> ( A +o z ) C_ B )
56 43 55 syl 
 |-  ( z e. |^| S -> ( A +o z ) C_ B )
57 54 56 mprgbir 
 |-  U_ z e. |^| S ( A +o z ) C_ B
58 53 57 eqsstrdi 
 |-  ( ( |^| S e. _V /\ Lim |^| S ) -> ( A +o |^| S ) C_ B )
59 58 a1d 
 |-  ( ( |^| S e. _V /\ Lim |^| S ) -> ( A C_ B -> ( A +o |^| S ) C_ B ) )
60 21 51 59 3jaoi 
 |-  ( ( |^| S = (/) \/ E. z e. On |^| S = suc z \/ ( |^| S e. _V /\ Lim |^| S ) ) -> ( A C_ B -> ( A +o |^| S ) C_ B ) )
61 15 60 ax-mp 
 |-  ( A C_ B -> ( A +o |^| S ) C_ B )
62 8 rspcev 
 |-  ( ( B e. On /\ B C_ ( A +o B ) ) -> E. y e. On B C_ ( A +o y ) )
63 2 6 62 mp2an 
 |-  E. y e. On B C_ ( A +o y )
64 nfcv 
 |-  F/_ y B
65 nfcv 
 |-  F/_ y A
66 nfcv 
 |-  F/_ y +o
67 nfrab1 
 |-  F/_ y { y e. On | B C_ ( A +o y ) }
68 67 nfint 
 |-  F/_ y |^| { y e. On | B C_ ( A +o y ) }
69 65 66 68 nfov 
 |-  F/_ y ( A +o |^| { y e. On | B C_ ( A +o y ) } )
70 64 69 nfss 
 |-  F/ y B C_ ( A +o |^| { y e. On | B C_ ( A +o y ) } )
71 oveq2 
 |-  ( y = |^| { y e. On | B C_ ( A +o y ) } -> ( A +o y ) = ( A +o |^| { y e. On | B C_ ( A +o y ) } ) )
72 71 sseq2d 
 |-  ( y = |^| { y e. On | B C_ ( A +o y ) } -> ( B C_ ( A +o y ) <-> B C_ ( A +o |^| { y e. On | B C_ ( A +o y ) } ) ) )
73 70 72 onminsb 
 |-  ( E. y e. On B C_ ( A +o y ) -> B C_ ( A +o |^| { y e. On | B C_ ( A +o y ) } ) )
74 63 73 ax-mp 
 |-  B C_ ( A +o |^| { y e. On | B C_ ( A +o y ) } )
75 31 oveq2i 
 |-  ( A +o |^| S ) = ( A +o |^| { y e. On | B C_ ( A +o y ) } )
76 74 75 sseqtrri 
 |-  B C_ ( A +o |^| S )
77 eqss 
 |-  ( ( A +o |^| S ) = B <-> ( ( A +o |^| S ) C_ B /\ B C_ ( A +o |^| S ) ) )
78 61 76 77 sylanblrc 
 |-  ( A C_ B -> ( A +o |^| S ) = B )
79 oveq2 
 |-  ( x = |^| S -> ( A +o x ) = ( A +o |^| S ) )
80 79 eqeq1d 
 |-  ( x = |^| S -> ( ( A +o x ) = B <-> ( A +o |^| S ) = B ) )
81 80 rspcev 
 |-  ( ( |^| S e. On /\ ( A +o |^| S ) = B ) -> E. x e. On ( A +o x ) = B )
82 13 78 81 sylancr 
 |-  ( A C_ B -> E. x e. On ( A +o x ) = B )
83 eqtr3 
 |-  ( ( ( A +o x ) = B /\ ( A +o y ) = B ) -> ( A +o x ) = ( A +o y ) )
84 oacan 
 |-  ( ( A e. On /\ x e. On /\ y e. On ) -> ( ( A +o x ) = ( A +o y ) <-> x = y ) )
85 1 84 mp3an1 
 |-  ( ( x e. On /\ y e. On ) -> ( ( A +o x ) = ( A +o y ) <-> x = y ) )
86 83 85 imbitrid 
 |-  ( ( x e. On /\ y e. On ) -> ( ( ( A +o x ) = B /\ ( A +o y ) = B ) -> x = y ) )
87 86 rgen2 
 |-  A. x e. On A. y e. On ( ( ( A +o x ) = B /\ ( A +o y ) = B ) -> x = y )
88 oveq2 
 |-  ( x = y -> ( A +o x ) = ( A +o y ) )
89 88 eqeq1d 
 |-  ( x = y -> ( ( A +o x ) = B <-> ( A +o y ) = B ) )
90 89 reu4 
 |-  ( E! x e. On ( A +o x ) = B <-> ( E. x e. On ( A +o x ) = B /\ A. x e. On A. y e. On ( ( ( A +o x ) = B /\ ( A +o y ) = B ) -> x = y ) ) )
91 82 87 90 sylanblrc 
 |-  ( A C_ B -> E! x e. On ( A +o x ) = B )