Metamath Proof Explorer

Theorem oaun3lem2

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

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

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ x = ( a +o b ) ) -> x = ( a +o b ) )
2 onelon 
 |-  ( ( A e. On /\ a e. A ) -> a e. On )
3 2 ad2ant2r 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> a e. On )
4 onelon 
 |-  ( ( B e. On /\ b e. B ) -> b e. On )
5 4 ad2ant2l 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> b e. On )
6 oacl 
 |-  ( ( a e. On /\ b e. On ) -> ( a +o b ) e. On )
7 3 5 6 syl2anc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> ( a +o b ) e. On )
8 oacl 
 |-  ( ( A e. On /\ B e. On ) -> ( A +o B ) e. On )
9 8 adantr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> ( A +o B ) e. On )
10 7 9 jca 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> ( ( a +o b ) e. On /\ ( A +o B ) e. On ) )
11 simpl 
 |-  ( ( A e. On /\ B e. On ) -> A e. On )
12 11 adantr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> A e. On )
13 3 12 5 3jca 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> ( a e. On /\ A e. On /\ b e. On ) )
14 simpl 
 |-  ( ( a e. A /\ b e. B ) -> a e. A )
15 14 adantl 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> a e. A )
16 eloni 
 |-  ( a e. On -> Ord a )
17 eloni 
 |-  ( A e. On -> Ord A )
18 16 17 anim12i 
 |-  ( ( a e. On /\ A e. On ) -> ( Ord a /\ Ord A ) )
19 3 12 18 syl2anc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> ( Ord a /\ Ord A ) )
20 ordelpss 
 |-  ( ( Ord a /\ Ord A ) -> ( a e. A <-> a C. A ) )
21 19 20 syl 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> ( a e. A <-> a C. A ) )
22 15 21 mpbid 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> a C. A )
23 22 pssssd 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> a C_ A )
24 oawordri 
 |-  ( ( a e. On /\ A e. On /\ b e. On ) -> ( a C_ A -> ( a +o b ) C_ ( A +o b ) ) )
25 13 23 24 sylc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> ( a +o b ) C_ ( A +o b ) )
26 pm3.22 
 |-  ( ( A e. On /\ B e. On ) -> ( B e. On /\ A e. On ) )
27 26 adantr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> ( B e. On /\ A e. On ) )
28 simpr 
 |-  ( ( a e. A /\ b e. B ) -> b e. B )
29 28 adantl 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> b e. B )
30 oaordi 
 |-  ( ( B e. On /\ A e. On ) -> ( b e. B -> ( A +o b ) e. ( A +o B ) ) )
31 27 29 30 sylc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> ( A +o b ) e. ( A +o B ) )
32 25 31 jca 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> ( ( a +o b ) C_ ( A +o b ) /\ ( A +o b ) e. ( A +o B ) ) )
33 ontr2 
 |-  ( ( ( a +o b ) e. On /\ ( A +o B ) e. On ) -> ( ( ( a +o b ) C_ ( A +o b ) /\ ( A +o b ) e. ( A +o B ) ) -> ( a +o b ) e. ( A +o B ) ) )
34 10 32 33 sylc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) -> ( a +o b ) e. ( A +o B ) )
35 34 adantr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ x = ( a +o b ) ) -> ( a +o b ) e. ( A +o B ) )
36 1 35 eqeltrd 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( a e. A /\ b e. B ) ) /\ x = ( a +o b ) ) -> x e. ( A +o B ) )
37 36 exp31 
 |-  ( ( A e. On /\ B e. On ) -> ( ( a e. A /\ b e. B ) -> ( x = ( a +o b ) -> x e. ( A +o B ) ) ) )
38 37 rexlimdvv 
 |-  ( ( A e. On /\ B e. On ) -> ( E. a e. A E. b e. B x = ( a +o b ) -> x e. ( A +o B ) ) )
39 38 abssdv 
 |-  ( ( A e. On /\ B e. On ) -> { x | E. a e. A E. b e. B x = ( a +o b ) } C_ ( A +o B ) )