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

Proof

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