Metamath Proof Explorer


Theorem omeulem1

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

Ref Expression
Assertion omeulem1 A On B On A x On y A A 𝑜 x + 𝑜 y = B

Proof

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