Metamath Proof Explorer

Theorem oaun3lem1

Description: The class of all ordinal sums of elements from two ordinals is ordinal. Lemma for oaun3 . (Contributed by RP, 13-Feb-2025)

Ref Expression
Assertion oaun3lem1 
|- ( ( A e. On /\ B e. On ) -> Ord { x | E. a e. A E. b e. B x = ( a +o b ) } )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ a ( A e. On /\ B e. On )
2 nfcv 
 |-  F/_ a y
3 nfre1 
 |-  F/ a E. a e. A E. b e. B x = ( a +o b )
4 3 nfsab 
 |-  F/ a z e. { x | E. a e. A E. b e. B x = ( a +o b ) }
5 2 4 nfralw 
 |-  F/ a A. z e. y z e. { x | E. a e. A E. b e. B x = ( a +o b ) }
6 nfv 
 |-  F/ b ( ( A e. On /\ B e. On ) /\ a e. A )
7 nfcv 
 |-  F/_ b y
8 nfcv 
 |-  F/_ b A
9 nfre1 
 |-  F/ b E. b e. B x = ( a +o b )
10 8 9 nfrexw 
 |-  F/ b E. a e. A E. b e. B x = ( a +o b )
11 10 nfsab 
 |-  F/ b z e. { x | E. a e. A E. b e. B x = ( a +o b ) }
12 7 11 nfralw 
 |-  F/ b A. z e. y z e. { x | E. a e. A E. b e. B x = ( a +o b ) }
13 simp-4l 
 |-  ( ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ z e. ( a +o b ) ) /\ z e. a ) -> A e. On )
14 simplrl 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ z e. ( a +o b ) ) -> a e. A )
15 14 anim1ci 
 |-  ( ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ z e. ( a +o b ) ) /\ z e. a ) -> ( z e. a /\ a e. A ) )
16 ontr1 
 |-  ( A e. On -> ( ( z e. a /\ a e. A ) -> z e. A ) )
17 13 15 16 sylc 
 |-  ( ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ z e. ( a +o b ) ) /\ z e. a ) -> z e. A )
18 simpr 
 |-  ( ( A e. On /\ B e. On ) -> B e. On )
19 ne0i 
 |-  ( b e. B -> B =/= (/) )
20 19 adantl 
 |-  ( ( a e. A /\ b e. B ) -> B =/= (/) )
21 on0eln0 
 |-  ( B e. On -> ( (/) e. B <-> B =/= (/) ) )
22 21 biimpar 
 |-  ( ( B e. On /\ B =/= (/) ) -> (/) e. B )
23 18 20 22 syl2an 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> (/) e. B )
24 onelon 
 |-  ( ( A e. On /\ a e. A ) -> a e. On )
25 24 ad2ant2r 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> a e. On )
26 simpr 
 |-  ( ( a e. A /\ b e. B ) -> b e. B )
27 onelon 
 |-  ( ( B e. On /\ b e. B ) -> b e. On )
28 18 26 27 syl2an 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> b e. On )
29 oacl 
 |-  ( ( a e. On /\ b e. On ) -> ( a +o b ) e. On )
30 25 28 29 syl2anc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> ( a +o b ) e. On )
31 onelon 
 |-  ( ( ( a +o b ) e. On /\ z e. ( a +o b ) ) -> z e. On )
32 30 31 sylan 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ z e. ( a +o b ) ) -> z e. On )
33 oa0 
 |-  ( z e. On -> ( z +o (/) ) = z )
34 32 33 syl 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ z e. ( a +o b ) ) -> ( z +o (/) ) = z )
35 34 eqcomd 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ z e. ( a +o b ) ) -> z = ( z +o (/) ) )
36 oveq2 
 |-  ( y = (/) -> ( z +o y ) = ( z +o (/) ) )
37 36 rspceeqv 
 |-  ( ( (/) e. B /\ z = ( z +o (/) ) ) -> E. y e. B z = ( z +o y ) )
38 23 35 37 syl2an2r 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ z e. ( a +o b ) ) -> E. y e. B z = ( z +o y ) )
39 38 adantr 
 |-  ( ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ z e. ( a +o b ) ) /\ z e. a ) -> E. y e. B z = ( z +o y ) )
40 oveq1 
 |-  ( w = z -> ( w +o y ) = ( z +o y ) )
41 40 eqeq2d 
 |-  ( w = z -> ( z = ( w +o y ) <-> z = ( z +o y ) ) )
42 41 rexbidv 
 |-  ( w = z -> ( E. y e. B z = ( w +o y ) <-> E. y e. B z = ( z +o y ) ) )
43 42 rspcev 
 |-  ( ( z e. A /\ E. y e. B z = ( z +o y ) ) -> E. w e. A E. y e. B z = ( w +o y ) )
44 17 39 43 syl2anc 
 |-  ( ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ z e. ( a +o b ) ) /\ z e. a ) -> E. w e. A E. y e. B z = ( w +o y ) )
45 18 adantr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> B e. On )
46 25 45 jca 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> ( a e. On /\ B e. On ) )
47 46 adantr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ z e. ( a +o b ) ) -> ( a e. On /\ B e. On ) )
48 oacl 
 |-  ( ( a e. On /\ B e. On ) -> ( a +o B ) e. On )
49 25 45 48 syl2anc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> ( a +o B ) e. On )
50 eloni 
 |-  ( ( a +o b ) e. On -> Ord ( a +o b ) )
51 eloni 
 |-  ( ( a +o B ) e. On -> Ord ( a +o B ) )
52 50 51 anim12i 
 |-  ( ( ( a +o b ) e. On /\ ( a +o B ) e. On ) -> ( Ord ( a +o b ) /\ Ord ( a +o B ) ) )
53 30 49 52 syl2anc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> ( Ord ( a +o b ) /\ Ord ( a +o B ) ) )
54 45 25 jca 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> ( B e. On /\ a e. On ) )
55 26 adantl 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> b e. B )
56 oaordi 
 |-  ( ( B e. On /\ a e. On ) -> ( b e. B -> ( a +o b ) e. ( a +o B ) ) )
57 54 55 56 sylc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> ( a +o b ) e. ( a +o B ) )
58 ordelpss 
 |-  ( ( Ord ( a +o b ) /\ Ord ( a +o B ) ) -> ( ( a +o b ) e. ( a +o B ) <-> ( a +o b ) C. ( a +o B ) ) )
59 58 biimpd 
 |-  ( ( Ord ( a +o b ) /\ Ord ( a +o B ) ) -> ( ( a +o b ) e. ( a +o B ) -> ( a +o b ) C. ( a +o B ) ) )
60 53 57 59 sylc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> ( a +o b ) C. ( a +o B ) )
61 60 pssssd 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> ( a +o b ) C_ ( a +o B ) )
62 61 sselda 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ z e. ( a +o b ) ) -> z e. ( a +o B ) )
63 62 anim1ci 
 |-  ( ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ z e. ( a +o b ) ) /\ a C_ z ) -> ( a C_ z /\ z e. ( a +o B ) ) )
64 oawordex2 
 |-  ( ( ( a e. On /\ B e. On ) /\ ( a C_ z /\ z e. ( a +o B ) ) ) -> E. y e. B ( a +o y ) = z )
65 47 63 64 syl2an2r 
 |-  ( ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ z e. ( a +o b ) ) /\ a C_ z ) -> E. y e. B ( a +o y ) = z )
66 oveq1 
 |-  ( w = a -> ( w +o y ) = ( a +o y ) )
67 66 eqeq2d 
 |-  ( w = a -> ( z = ( w +o y ) <-> z = ( a +o y ) ) )
68 eqcom 
 |-  ( z = ( a +o y ) <-> ( a +o y ) = z )
69 67 68 bitrdi 
 |-  ( w = a -> ( z = ( w +o y ) <-> ( a +o y ) = z ) )
70 69 rexbidv 
 |-  ( w = a -> ( E. y e. B z = ( w +o y ) <-> E. y e. B ( a +o y ) = z ) )
71 70 rspcev 
 |-  ( ( a e. A /\ E. y e. B ( a +o y ) = z ) -> E. w e. A E. y e. B z = ( w +o y ) )
72 14 65 71 syl2an2r 
 |-  ( ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ z e. ( a +o b ) ) /\ a C_ z ) -> E. w e. A E. y e. B z = ( w +o y ) )
73 eloni 
 |-  ( z e. On -> Ord z )
74 32 73 syl 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ z e. ( a +o b ) ) -> Ord z )
75 eloni 
 |-  ( a e. On -> Ord a )
76 25 75 syl 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> Ord a )
77 76 adantr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ z e. ( a +o b ) ) -> Ord a )
78 ordtri2or 
 |-  ( ( Ord z /\ Ord a ) -> ( z e. a \/ a C_ z ) )
79 74 77 78 syl2anc 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ z e. ( a +o b ) ) -> ( z e. a \/ a C_ z ) )
80 44 72 79 mpjaodan 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ z e. ( a +o b ) ) -> E. w e. A E. y e. B z = ( w +o y ) )
81 vex 
 |-  z e. _V
82 eqeq1 
 |-  ( x = z -> ( x = ( a +o b ) <-> z = ( a +o b ) ) )
83 82 2rexbidv 
 |-  ( x = z -> ( E. a e. A E. b e. B x = ( a +o b ) <-> E. a e. A E. b e. B z = ( a +o b ) ) )
84 oveq1 
 |-  ( a = w -> ( a +o b ) = ( w +o b ) )
85 84 eqeq2d 
 |-  ( a = w -> ( z = ( a +o b ) <-> z = ( w +o b ) ) )
86 oveq2 
 |-  ( b = y -> ( w +o b ) = ( w +o y ) )
87 86 eqeq2d 
 |-  ( b = y -> ( z = ( w +o b ) <-> z = ( w +o y ) ) )
88 85 87 cbvrex2vw 
 |-  ( E. a e. A E. b e. B z = ( a +o b ) <-> E. w e. A E. y e. B z = ( w +o y ) )
89 83 88 bitrdi 
 |-  ( x = z -> ( E. a e. A E. b e. B x = ( a +o b ) <-> E. w e. A E. y e. B z = ( w +o y ) ) )
90 81 89 elab 
 |-  ( z e. { x | E. a e. A E. b e. B x = ( a +o b ) } <-> E. w e. A E. y e. B z = ( w +o y ) )
91 80 90 sylibr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ z e. ( a +o b ) ) -> z e. { x | E. a e. A E. b e. B x = ( a +o b ) } )
92 91 ralrimiva 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> A. z e. ( a +o b ) z e. { x | E. a e. A E. b e. B x = ( a +o b ) } )
93 92 adantr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ y = ( a +o b ) ) -> A. z e. ( a +o b ) z e. { x | E. a e. A E. b e. B x = ( a +o b ) } )
94 simpr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ y = ( a +o b ) ) -> y = ( a +o b ) )
95 94 raleqdv 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ y = ( a +o b ) ) -> ( A. z e. y z e. { x | E. a e. A E. b e. B x = ( a +o b ) } <-> A. z e. ( a +o b ) z e. { x | E. a e. A E. b e. B x = ( a +o b ) } ) )
96 93 95 mpbird 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ y = ( a +o b ) ) -> A. z e. y z e. { x | E. a e. A E. b e. B x = ( a +o b ) } )
97 96 exp31 
 |-  ( ( A e. On /\ B e. On ) -> ( ( a e. A /\ b e. B ) -> ( y = ( a +o b ) -> A. z e. y z e. { x | E. a e. A E. b e. B x = ( a +o b ) } ) ) )
98 97 expdimp 
 |-  ( ( ( A e. On /\ B e. On ) /\ a e. A ) -> ( b e. B -> ( y = ( a +o b ) -> A. z e. y z e. { x | E. a e. A E. b e. B x = ( a +o b ) } ) ) )
99 6 12 98 rexlimd 
 |-  ( ( ( A e. On /\ B e. On ) /\ a e. A ) -> ( E. b e. B y = ( a +o b ) -> A. z e. y z e. { x | E. a e. A E. b e. B x = ( a +o b ) } ) )
100 99 ex 
 |-  ( ( A e. On /\ B e. On ) -> ( a e. A -> ( E. b e. B y = ( a +o b ) -> A. z e. y z e. { x | E. a e. A E. b e. B x = ( a +o b ) } ) ) )
101 1 5 100 rexlimd 
 |-  ( ( A e. On /\ B e. On ) -> ( E. a e. A E. b e. B y = ( a +o b ) -> A. z e. y z e. { x | E. a e. A E. b e. B x = ( a +o b ) } ) )
102 101 alrimiv 
 |-  ( ( A e. On /\ B e. On ) -> A. y ( E. a e. A E. b e. B y = ( a +o b ) -> A. z e. y z e. { x | E. a e. A E. b e. B x = ( a +o b ) } ) )
103 eqeq1 
 |-  ( x = y -> ( x = ( a +o b ) <-> y = ( a +o b ) ) )
104 103 2rexbidv 
 |-  ( x = y -> ( E. a e. A E. b e. B x = ( a +o b ) <-> E. a e. A E. b e. B y = ( a +o b ) ) )
105 104 ralab 
 |-  ( A. y e. { x | E. a e. A E. b e. B x = ( a +o b ) } A. z e. y z e. { x | E. a e. A E. b e. B x = ( a +o b ) } <-> A. y ( E. a e. A E. b e. B y = ( a +o b ) -> A. z e. y z e. { x | E. a e. A E. b e. B x = ( a +o b ) } ) )
106 102 105 sylibr 
 |-  ( ( A e. On /\ B e. On ) -> A. y e. { x | E. a e. A E. b e. B x = ( a +o b ) } A. z e. y z e. { x | E. a e. A E. b e. B x = ( a +o b ) } )
107 dftr5 
 |-  ( Tr { x | E. a e. A E. b e. B x = ( a +o b ) } <-> A. y e. { x | E. a e. A E. b e. B x = ( a +o b ) } A. z e. y z e. { x | E. a e. A E. b e. B x = ( a +o b ) } )
108 106 107 sylibr 
 |-  ( ( A e. On /\ B e. On ) -> Tr { x | E. a e. A E. b e. B x = ( a +o b ) } )
109 simpr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ x = ( a +o b ) ) -> x = ( a +o b ) )
110 30 adantr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ x = ( a +o b ) ) -> ( a +o b ) e. On )
111 109 110 eqeltrd 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ x = ( a +o b ) ) -> x e. On )
112 111 exp31 
 |-  ( ( A e. On /\ B e. On ) -> ( ( a e. A /\ b e. B ) -> ( x = ( a +o b ) -> x e. On ) ) )
113 112 rexlimdvv 
 |-  ( ( A e. On /\ B e. On ) -> ( E. a e. A E. b e. B x = ( a +o b ) -> x e. On ) )
114 113 abssdv 
 |-  ( ( A e. On /\ B e. On ) -> { x | E. a e. A E. b e. B x = ( a +o b ) } C_ On )
115 epweon 
 |-  _E We On
116 wess 
 |-  ( { x | E. a e. A E. b e. B x = ( a +o b ) } C_ On -> ( _E We On -> _E We { x | E. a e. A E. b e. B x = ( a +o b ) } ) )
117 114 115 116 mpisyl 
 |-  ( ( A e. On /\ B e. On ) -> _E We { x | E. a e. A E. b e. B x = ( a +o b ) } )
118 df-ord 
 |-  ( Ord { x | E. a e. A E. b e. B x = ( a +o b ) } <-> ( Tr { x | E. a e. A E. b e. B x = ( a +o b ) } /\ _E We { x | E. a e. A E. b e. B x = ( a +o b ) } ) )
119 108 117 118 sylanbrc 
 |-  ( ( A e. On /\ B e. On ) -> Ord { x | E. a e. A E. b e. B x = ( a +o b ) } )