Metamath Proof Explorer

Theorem omeulem1

Description: Lemma for omeu : existence part. (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Assertion omeulem1 
|- ( ( A e. On /\ B e. On /\ A =/= (/) ) -> E. x e. On E. y e. A ( ( A .o x ) +o y ) = B )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( A e. On /\ B e. On /\ A =/= (/) ) -> B e. On )
2 sucelon 
 |-  ( B e. On <-> suc B e. On )
3 1 2 sylib 
 |-  ( ( A e. On /\ B e. On /\ A =/= (/) ) -> suc B e. On )
4 simp1 
 |-  ( ( A e. On /\ B e. On /\ A =/= (/) ) -> A e. On )
5 on0eln0 
 |-  ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
6 5 biimpar 
 |-  ( ( A e. On /\ A =/= (/) ) -> (/) e. A )
7 6 3adant2 
 |-  ( ( A e. On /\ B e. On /\ A =/= (/) ) -> (/) e. A )
8 omword2 
 |-  ( ( ( suc B e. On /\ A e. On ) /\ (/) e. A ) -> suc B C_ ( A .o suc B ) )
9 3 4 7 8 syl21anc 
 |-  ( ( A e. On /\ B e. On /\ A =/= (/) ) -> suc B C_ ( A .o suc B ) )
10 sucidg 
 |-  ( B e. On -> B e. suc B )
11 ssel 
 |-  ( suc B C_ ( A .o suc B ) -> ( B e. suc B -> B e. ( A .o suc B ) ) )
12 10 11 syl5 
 |-  ( suc B C_ ( A .o suc B ) -> ( B e. On -> B e. ( A .o suc B ) ) )
13 9 1 12 sylc 
 |-  ( ( A e. On /\ B e. On /\ A =/= (/) ) -> B e. ( A .o suc B ) )
14 suceq 
 |-  ( x = B -> suc x = suc B )
15 14 oveq2d 
 |-  ( x = B -> ( A .o suc x ) = ( A .o suc B ) )
16 15 eleq2d 
 |-  ( x = B -> ( B e. ( A .o suc x ) <-> B e. ( A .o suc B ) ) )
17 16 rspcev 
 |-  ( ( B e. On /\ B e. ( A .o suc B ) ) -> E. x e. On B e. ( A .o suc x ) )
18 1 13 17 syl2anc 
 |-  ( ( A e. On /\ B e. On /\ A =/= (/) ) -> E. x e. On B e. ( A .o suc x ) )
19 suceq 
 |-  ( x = z -> suc x = suc z )
20 19 oveq2d 
 |-  ( x = z -> ( A .o suc x ) = ( A .o suc z ) )
21 20 eleq2d 
 |-  ( x = z -> ( B e. ( A .o suc x ) <-> B e. ( A .o suc z ) ) )
22 21 onminex 
 |-  ( E. x e. On B e. ( A .o suc x ) -> E. x e. On ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) ) )
23 vex 
 |-  x e. _V
24 23 elon 
 |-  ( x e. On <-> Ord x )
25 ordzsl 
 |-  ( Ord x <-> ( x = (/) \/ E. w e. On x = suc w \/ Lim x ) )
26 24 25 bitri 
 |-  ( x e. On <-> ( x = (/) \/ E. w e. On x = suc w \/ Lim x ) )
27 oveq2 
 |-  ( x = (/) -> ( A .o x ) = ( A .o (/) ) )
28 om0 
 |-  ( A e. On -> ( A .o (/) ) = (/) )
29 27 28 sylan9eqr 
 |-  ( ( A e. On /\ x = (/) ) -> ( A .o x ) = (/) )
30 ne0i 
 |-  ( B e. ( A .o x ) -> ( A .o x ) =/= (/) )
31 30 necon2bi 
 |-  ( ( A .o x ) = (/) -> -. B e. ( A .o x ) )
32 29 31 syl 
 |-  ( ( A e. On /\ x = (/) ) -> -. B e. ( A .o x ) )
33 32 ex 
 |-  ( A e. On -> ( x = (/) -> -. B e. ( A .o x ) ) )
34 33 a1d 
 |-  ( A e. On -> ( A. z e. x -. B e. ( A .o suc z ) -> ( x = (/) -> -. B e. ( A .o x ) ) ) )
35 34 3ad2ant1 
 |-  ( ( A e. On /\ B e. On /\ A =/= (/) ) -> ( A. z e. x -. B e. ( A .o suc z ) -> ( x = (/) -> -. B e. ( A .o x ) ) ) )
36 35 imp 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ A. z e. x -. B e. ( A .o suc z ) ) -> ( x = (/) -> -. B e. ( A .o x ) ) )
37 simp3 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x = suc w ) -> x = suc w )
38 simp2 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x = suc w ) -> A. z e. x -. B e. ( A .o suc z ) )
39 raleq 
 |-  ( x = suc w -> ( A. z e. x -. B e. ( A .o suc z ) <-> A. z e. suc w -. B e. ( A .o suc z ) ) )
40 vex 
 |-  w e. _V
41 40 sucid 
 |-  w e. suc w
42 suceq 
 |-  ( z = w -> suc z = suc w )
43 42 oveq2d 
 |-  ( z = w -> ( A .o suc z ) = ( A .o suc w ) )
44 43 eleq2d 
 |-  ( z = w -> ( B e. ( A .o suc z ) <-> B e. ( A .o suc w ) ) )
45 44 notbid 
 |-  ( z = w -> ( -. B e. ( A .o suc z ) <-> -. B e. ( A .o suc w ) ) )
46 45 rspcv 
 |-  ( w e. suc w -> ( A. z e. suc w -. B e. ( A .o suc z ) -> -. B e. ( A .o suc w ) ) )
47 41 46 ax-mp 
 |-  ( A. z e. suc w -. B e. ( A .o suc z ) -> -. B e. ( A .o suc w ) )
48 39 47 syl6bi 
 |-  ( x = suc w -> ( A. z e. x -. B e. ( A .o suc z ) -> -. B e. ( A .o suc w ) ) )
49 37 38 48 sylc 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x = suc w ) -> -. B e. ( A .o suc w ) )
50 oveq2 
 |-  ( x = suc w -> ( A .o x ) = ( A .o suc w ) )
51 50 eleq2d 
 |-  ( x = suc w -> ( B e. ( A .o x ) <-> B e. ( A .o suc w ) ) )
52 51 notbid 
 |-  ( x = suc w -> ( -. B e. ( A .o x ) <-> -. B e. ( A .o suc w ) ) )
53 52 biimpar 
 |-  ( ( x = suc w /\ -. B e. ( A .o suc w ) ) -> -. B e. ( A .o x ) )
54 37 49 53 syl2anc 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x = suc w ) -> -. B e. ( A .o x ) )
55 54 3expia 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ A. z e. x -. B e. ( A .o suc z ) ) -> ( x = suc w -> -. B e. ( A .o x ) ) )
56 55 rexlimdvw 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ A. z e. x -. B e. ( A .o suc z ) ) -> ( E. w e. On x = suc w -> -. B e. ( A .o x ) ) )
57 ralnex 
 |-  ( A. z e. x -. B e. ( A .o suc z ) <-> -. E. z e. x B e. ( A .o suc z ) )
58 simpr 
 |-  ( ( Lim x /\ A e. On ) -> A e. On )
59 23 a1i 
 |-  ( ( Lim x /\ A e. On ) -> x e. _V )
60 simpl 
 |-  ( ( Lim x /\ A e. On ) -> Lim x )
61 omlim 
 |-  ( ( A e. On /\ ( x e. _V /\ Lim x ) ) -> ( A .o x ) = U_ z e. x ( A .o z ) )
62 58 59 60 61 syl12anc 
 |-  ( ( Lim x /\ A e. On ) -> ( A .o x ) = U_ z e. x ( A .o z ) )
63 62 eleq2d 
 |-  ( ( Lim x /\ A e. On ) -> ( B e. ( A .o x ) <-> B e. U_ z e. x ( A .o z ) ) )
64 eliun 
 |-  ( B e. U_ z e. x ( A .o z ) <-> E. z e. x B e. ( A .o z ) )
65 limord 
 |-  ( Lim x -> Ord x )
66 65 3ad2ant1 
 |-  ( ( Lim x /\ A e. On /\ z e. x ) -> Ord x )
67 66 24 sylibr 
 |-  ( ( Lim x /\ A e. On /\ z e. x ) -> x e. On )
68 simp3 
 |-  ( ( Lim x /\ A e. On /\ z e. x ) -> z e. x )
69 onelon 
 |-  ( ( x e. On /\ z e. x ) -> z e. On )
70 67 68 69 syl2anc 
 |-  ( ( Lim x /\ A e. On /\ z e. x ) -> z e. On )
71 suceloni 
 |-  ( z e. On -> suc z e. On )
72 70 71 syl 
 |-  ( ( Lim x /\ A e. On /\ z e. x ) -> suc z e. On )
73 simp2 
 |-  ( ( Lim x /\ A e. On /\ z e. x ) -> A e. On )
74 sssucid 
 |-  z C_ suc z
75 omwordi 
 |-  ( ( z e. On /\ suc z e. On /\ A e. On ) -> ( z C_ suc z -> ( A .o z ) C_ ( A .o suc z ) ) )
76 74 75 mpi 
 |-  ( ( z e. On /\ suc z e. On /\ A e. On ) -> ( A .o z ) C_ ( A .o suc z ) )
77 70 72 73 76 syl3anc 
 |-  ( ( Lim x /\ A e. On /\ z e. x ) -> ( A .o z ) C_ ( A .o suc z ) )
78 77 sseld 
 |-  ( ( Lim x /\ A e. On /\ z e. x ) -> ( B e. ( A .o z ) -> B e. ( A .o suc z ) ) )
79 78 3expia 
 |-  ( ( Lim x /\ A e. On ) -> ( z e. x -> ( B e. ( A .o z ) -> B e. ( A .o suc z ) ) ) )
80 79 reximdvai 
 |-  ( ( Lim x /\ A e. On ) -> ( E. z e. x B e. ( A .o z ) -> E. z e. x B e. ( A .o suc z ) ) )
81 64 80 syl5bi 
 |-  ( ( Lim x /\ A e. On ) -> ( B e. U_ z e. x ( A .o z ) -> E. z e. x B e. ( A .o suc z ) ) )
82 63 81 sylbid 
 |-  ( ( Lim x /\ A e. On ) -> ( B e. ( A .o x ) -> E. z e. x B e. ( A .o suc z ) ) )
83 82 con3d 
 |-  ( ( Lim x /\ A e. On ) -> ( -. E. z e. x B e. ( A .o suc z ) -> -. B e. ( A .o x ) ) )
84 57 83 syl5bi 
 |-  ( ( Lim x /\ A e. On ) -> ( A. z e. x -. B e. ( A .o suc z ) -> -. B e. ( A .o x ) ) )
85 84 expimpd 
 |-  ( Lim x -> ( ( A e. On /\ A. z e. x -. B e. ( A .o suc z ) ) -> -. B e. ( A .o x ) ) )
86 85 com12 
 |-  ( ( A e. On /\ A. z e. x -. B e. ( A .o suc z ) ) -> ( Lim x -> -. B e. ( A .o x ) ) )
87 86 3ad2antl1 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ A. z e. x -. B e. ( A .o suc z ) ) -> ( Lim x -> -. B e. ( A .o x ) ) )
88 36 56 87 3jaod 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ A. z e. x -. B e. ( A .o suc z ) ) -> ( ( x = (/) \/ E. w e. On x = suc w \/ Lim x ) -> -. B e. ( A .o x ) ) )
89 26 88 syl5bi 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ A. z e. x -. B e. ( A .o suc z ) ) -> ( x e. On -> -. B e. ( A .o x ) ) )
90 89 impr 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) ) -> -. B e. ( A .o x ) )
91 simpl1 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) ) -> A e. On )
92 simprr 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) ) -> x e. On )
93 omcl 
 |-  ( ( A e. On /\ x e. On ) -> ( A .o x ) e. On )
94 91 92 93 syl2anc 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) ) -> ( A .o x ) e. On )
95 simpl2 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) ) -> B e. On )
96 ontri1 
 |-  ( ( ( A .o x ) e. On /\ B e. On ) -> ( ( A .o x ) C_ B <-> -. B e. ( A .o x ) ) )
97 94 95 96 syl2anc 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) ) -> ( ( A .o x ) C_ B <-> -. B e. ( A .o x ) ) )
98 90 97 mpbird 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) ) -> ( A .o x ) C_ B )
99 oawordex 
 |-  ( ( ( A .o x ) e. On /\ B e. On ) -> ( ( A .o x ) C_ B <-> E. y e. On ( ( A .o x ) +o y ) = B ) )
100 94 95 99 syl2anc 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) ) -> ( ( A .o x ) C_ B <-> E. y e. On ( ( A .o x ) +o y ) = B ) )
101 98 100 mpbid 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) ) -> E. y e. On ( ( A .o x ) +o y ) = B )
102 101 3adantr1 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) ) -> E. y e. On ( ( A .o x ) +o y ) = B )
103 simp3r 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) /\ ( y e. On /\ ( ( A .o x ) +o y ) = B ) ) -> ( ( A .o x ) +o y ) = B )
104 simp21 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) /\ ( y e. On /\ ( ( A .o x ) +o y ) = B ) ) -> B e. ( A .o suc x ) )
105 simp11 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) /\ ( y e. On /\ ( ( A .o x ) +o y ) = B ) ) -> A e. On )
106 simp23 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) /\ ( y e. On /\ ( ( A .o x ) +o y ) = B ) ) -> x e. On )
107 omsuc 
 |-  ( ( A e. On /\ x e. On ) -> ( A .o suc x ) = ( ( A .o x ) +o A ) )
108 105 106 107 syl2anc 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) /\ ( y e. On /\ ( ( A .o x ) +o y ) = B ) ) -> ( A .o suc x ) = ( ( A .o x ) +o A ) )
109 104 108 eleqtrd 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) /\ ( y e. On /\ ( ( A .o x ) +o y ) = B ) ) -> B e. ( ( A .o x ) +o A ) )
110 103 109 eqeltrd 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) /\ ( y e. On /\ ( ( A .o x ) +o y ) = B ) ) -> ( ( A .o x ) +o y ) e. ( ( A .o x ) +o A ) )
111 simp3l 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) /\ ( y e. On /\ ( ( A .o x ) +o y ) = B ) ) -> y e. On )
112 105 106 93 syl2anc 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) /\ ( y e. On /\ ( ( A .o x ) +o y ) = B ) ) -> ( A .o x ) e. On )
113 oaord 
 |-  ( ( y e. On /\ A e. On /\ ( A .o x ) e. On ) -> ( y e. A <-> ( ( A .o x ) +o y ) e. ( ( A .o x ) +o A ) ) )
114 111 105 112 113 syl3anc 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) /\ ( y e. On /\ ( ( A .o x ) +o y ) = B ) ) -> ( y e. A <-> ( ( A .o x ) +o y ) e. ( ( A .o x ) +o A ) ) )
115 110 114 mpbird 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) /\ ( y e. On /\ ( ( A .o x ) +o y ) = B ) ) -> y e. A )
116 115 103 jca 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) /\ ( y e. On /\ ( ( A .o x ) +o y ) = B ) ) -> ( y e. A /\ ( ( A .o x ) +o y ) = B ) )
117 116 3expia 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) ) -> ( ( y e. On /\ ( ( A .o x ) +o y ) = B ) -> ( y e. A /\ ( ( A .o x ) +o y ) = B ) ) )
118 117 reximdv2 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) ) -> ( E. y e. On ( ( A .o x ) +o y ) = B -> E. y e. A ( ( A .o x ) +o y ) = B ) )
119 102 118 mpd 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) ) -> E. y e. A ( ( A .o x ) +o y ) = B )
120 119 expcom 
 |-  ( ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) /\ x e. On ) -> ( ( A e. On /\ B e. On /\ A =/= (/) ) -> E. y e. A ( ( A .o x ) +o y ) = B ) )
121 120 3expia 
 |-  ( ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) ) -> ( x e. On -> ( ( A e. On /\ B e. On /\ A =/= (/) ) -> E. y e. A ( ( A .o x ) +o y ) = B ) ) )
122 121 com13 
 |-  ( ( A e. On /\ B e. On /\ A =/= (/) ) -> ( x e. On -> ( ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) ) -> E. y e. A ( ( A .o x ) +o y ) = B ) ) )
123 122 reximdvai 
 |-  ( ( A e. On /\ B e. On /\ A =/= (/) ) -> ( E. x e. On ( B e. ( A .o suc x ) /\ A. z e. x -. B e. ( A .o suc z ) ) -> E. x e. On E. y e. A ( ( A .o x ) +o y ) = B ) )
124 22 123 syl5 
 |-  ( ( A e. On /\ B e. On /\ A =/= (/) ) -> ( E. x e. On B e. ( A .o suc x ) -> E. x e. On E. y e. A ( ( A .o x ) +o y ) = B ) )
125 18 124 mpd 
 |-  ( ( A e. On /\ B e. On /\ A =/= (/) ) -> E. x e. On E. y e. A ( ( A .o x ) +o y ) = B )