Metamath Proof Explorer


Theorem oawordeulem

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

Ref Expression
Hypotheses oawordeulem.1 A On
oawordeulem.2 B On
oawordeulem.3 S = y On | B A + 𝑜 y
Assertion oawordeulem A B ∃! x On A + 𝑜 x = B

Proof

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