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 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝑎 +o 𝑏 ) } ⊆ ( 𝐴 +o 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑥 = ( 𝑎 +o 𝑏 ) ) → 𝑥 = ( 𝑎 +o 𝑏 ) )
2 onelon ⊢ ( ( 𝐴 ∈ On ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ On )
3 2 ad2ant2r ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ∈ On )
4 onelon ⊢ ( ( 𝐵 ∈ On ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ On )
5 4 ad2ant2l ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 ∈ On )
6 oacl ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( 𝑎 +o 𝑏 ) ∈ On )
7 3 5 6 syl2anc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 +o 𝑏 ) ∈ On )
8 oacl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) ∈ On )
9 8 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐴 +o 𝐵 ) ∈ On )
10 7 9 jca ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑎 +o 𝑏 ) ∈ On ∧ ( 𝐴 +o 𝐵 ) ∈ On ) )
11 simpl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐴 ∈ On )
12 11 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝐴 ∈ On )
13 3 12 5 3jca ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ∈ On ∧ 𝐴 ∈ On ∧ 𝑏 ∈ On ) )
14 simpl ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → 𝑎 ∈ 𝐴 )
15 14 adantl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ∈ 𝐴 )
16 eloni ⊢ ( 𝑎 ∈ On → Ord 𝑎 )
17 eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
18 16 17 anim12i ⊢ ( ( 𝑎 ∈ On ∧ 𝐴 ∈ On ) → ( Ord 𝑎 ∧ Ord 𝐴 ) )
19 3 12 18 syl2anc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( Ord 𝑎 ∧ Ord 𝐴 ) )
20 ordelpss ⊢ ( ( Ord 𝑎 ∧ Ord 𝐴 ) → ( 𝑎 ∈ 𝐴 ↔ 𝑎 ⊊ 𝐴 ) )
21 19 20 syl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ∈ 𝐴 ↔ 𝑎 ⊊ 𝐴 ) )
22 15 21 mpbid ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ⊊ 𝐴 )
23 22 pssssd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ⊆ 𝐴 )
24 oawordri ⊢ ( ( 𝑎 ∈ On ∧ 𝐴 ∈ On ∧ 𝑏 ∈ On ) → ( 𝑎 ⊆ 𝐴 → ( 𝑎 +o 𝑏 ) ⊆ ( 𝐴 +o 𝑏 ) ) )
25 13 23 24 sylc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 +o 𝑏 ) ⊆ ( 𝐴 +o 𝑏 ) )
26 pm3.22 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) )
27 26 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) )
28 simpr ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
29 28 adantl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 ∈ 𝐵 )
30 oaordi ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 𝑏 ∈ 𝐵 → ( 𝐴 +o 𝑏 ) ∈ ( 𝐴 +o 𝐵 ) ) )
31 27 29 30 sylc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐴 +o 𝑏 ) ∈ ( 𝐴 +o 𝐵 ) )
32 25 31 jca ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑎 +o 𝑏 ) ⊆ ( 𝐴 +o 𝑏 ) ∧ ( 𝐴 +o 𝑏 ) ∈ ( 𝐴 +o 𝐵 ) ) )
33 ontr2 ⊢ ( ( ( 𝑎 +o 𝑏 ) ∈ On ∧ ( 𝐴 +o 𝐵 ) ∈ On ) → ( ( ( 𝑎 +o 𝑏 ) ⊆ ( 𝐴 +o 𝑏 ) ∧ ( 𝐴 +o 𝑏 ) ∈ ( 𝐴 +o 𝐵 ) ) → ( 𝑎 +o 𝑏 ) ∈ ( 𝐴 +o 𝐵 ) ) )
34 10 32 33 sylc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 +o 𝑏 ) ∈ ( 𝐴 +o 𝐵 ) )
35 34 adantr ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑥 = ( 𝑎 +o 𝑏 ) ) → ( 𝑎 +o 𝑏 ) ∈ ( 𝐴 +o 𝐵 ) )
36 1 35 eqeltrd ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑥 = ( 𝑎 +o 𝑏 ) ) → 𝑥 ∈ ( 𝐴 +o 𝐵 ) )
37 36 exp31 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑥 = ( 𝑎 +o 𝑏 ) → 𝑥 ∈ ( 𝐴 +o 𝐵 ) ) ) )
38 37 rexlimdvv ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝑎 +o 𝑏 ) → 𝑥 ∈ ( 𝐴 +o 𝐵 ) ) )
39 38 abssdv ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝑎 +o 𝑏 ) } ⊆ ( 𝐴 +o 𝐵 ) )