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 syl5bi
 |-  ( 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 syl5ib
 |-  ( ( 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 )