Metamath Proof Explorer

Theorem naddgeoa

Description: Natural addition results in a value greater than or equal than that of ordinal addition. (Contributed by RP, 1-Jan-2025)

Ref Expression
Assertion naddgeoa ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) ⊆ ( 𝐴 +no 𝐵 ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 +o 𝑏 ) = ( 𝑐 +o 𝑏 ) )
2 oveq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 +no 𝑏 ) = ( 𝑐 +no 𝑏 ) )
3 1 2 sseq12d ⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 +o 𝑏 ) ⊆ ( 𝑎 +no 𝑏 ) ↔ ( 𝑐 +o 𝑏 ) ⊆ ( 𝑐 +no 𝑏 ) ) )
4 oveq2 ⊢ ( 𝑏 = 𝑑 → ( 𝑐 +o 𝑏 ) = ( 𝑐 +o 𝑑 ) )
5 oveq2 ⊢ ( 𝑏 = 𝑑 → ( 𝑐 +no 𝑏 ) = ( 𝑐 +no 𝑑 ) )
6 4 5 sseq12d ⊢ ( 𝑏 = 𝑑 → ( ( 𝑐 +o 𝑏 ) ⊆ ( 𝑐 +no 𝑏 ) ↔ ( 𝑐 +o 𝑑 ) ⊆ ( 𝑐 +no 𝑑 ) ) )
7 oveq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 +o 𝑑 ) = ( 𝑐 +o 𝑑 ) )
8 oveq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 +no 𝑑 ) = ( 𝑐 +no 𝑑 ) )
9 7 8 sseq12d ⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ↔ ( 𝑐 +o 𝑑 ) ⊆ ( 𝑐 +no 𝑑 ) ) )
10 oveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 +o 𝑏 ) = ( 𝐴 +o 𝑏 ) )
11 oveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 +no 𝑏 ) = ( 𝐴 +no 𝑏 ) )
12 10 11 sseq12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 +o 𝑏 ) ⊆ ( 𝑎 +no 𝑏 ) ↔ ( 𝐴 +o 𝑏 ) ⊆ ( 𝐴 +no 𝑏 ) ) )
13 oveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐴 +o 𝑏 ) = ( 𝐴 +o 𝐵 ) )
14 oveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐴 +no 𝑏 ) = ( 𝐴 +no 𝐵 ) )
15 13 14 sseq12d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 +o 𝑏 ) ⊆ ( 𝐴 +no 𝑏 ) ↔ ( 𝐴 +o 𝐵 ) ⊆ ( 𝐴 +no 𝐵 ) ) )
16 simplll ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ Lim 𝑏 ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +o 𝑑 ) ⊆ ( 𝑐 +no 𝑑 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +o 𝑏 ) ⊆ ( 𝑐 +no 𝑏 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → 𝑎 ∈ On )
17 simpllr ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ Lim 𝑏 ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +o 𝑑 ) ⊆ ( 𝑐 +no 𝑑 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +o 𝑏 ) ⊆ ( 𝑐 +no 𝑏 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → 𝑏 ∈ On )
18 simplr ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ Lim 𝑏 ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +o 𝑑 ) ⊆ ( 𝑐 +no 𝑑 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +o 𝑏 ) ⊆ ( 𝑐 +no 𝑏 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → Lim 𝑏 )
19 17 18 jca ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ Lim 𝑏 ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +o 𝑑 ) ⊆ ( 𝑐 +no 𝑑 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +o 𝑏 ) ⊆ ( 𝑐 +no 𝑏 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → ( 𝑏 ∈ On ∧ Lim 𝑏 ) )
20 oalim ⊢ ( ( 𝑎 ∈ On ∧ ( 𝑏 ∈ On ∧ Lim 𝑏 ) ) → ( 𝑎 +o 𝑏 ) = ∪ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) )
21 16 19 20 syl2anc ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ Lim 𝑏 ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +o 𝑑 ) ⊆ ( 𝑐 +no 𝑑 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +o 𝑏 ) ⊆ ( 𝑐 +no 𝑏 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → ( 𝑎 +o 𝑏 ) = ∪ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) )
22 simpl ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ Lim 𝑏 ) → ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) )
23 simp3 ⊢ ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +o 𝑑 ) ⊆ ( 𝑐 +no 𝑑 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +o 𝑏 ) ⊆ ( 𝑐 +no 𝑏 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) → ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) )
24 simpr ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) ∧ ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) → ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) )
25 simpr ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → 𝑏 ∈ On )
26 onelss ⊢ ( 𝑏 ∈ On → ( 𝑑 ∈ 𝑏 → 𝑑 ⊆ 𝑏 ) )
27 25 26 syl ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( 𝑑 ∈ 𝑏 → 𝑑 ⊆ 𝑏 ) )
28 27 imp ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) → 𝑑 ⊆ 𝑏 )
29 simplr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) → 𝑏 ∈ On )
30 simpr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) → 𝑑 ∈ 𝑏 )
31 onelon ⊢ ( ( 𝑏 ∈ On ∧ 𝑑 ∈ 𝑏 ) → 𝑑 ∈ On )
32 29 30 31 syl2anc ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) → 𝑑 ∈ On )
33 simpll ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) → 𝑎 ∈ On )
34 naddss2 ⊢ ( ( 𝑑 ∈ On ∧ 𝑏 ∈ On ∧ 𝑎 ∈ On ) → ( 𝑑 ⊆ 𝑏 ↔ ( 𝑎 +no 𝑑 ) ⊆ ( 𝑎 +no 𝑏 ) ) )
35 32 29 33 34 syl3anc ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) → ( 𝑑 ⊆ 𝑏 ↔ ( 𝑎 +no 𝑑 ) ⊆ ( 𝑎 +no 𝑏 ) ) )
36 28 35 mpbid ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) → ( 𝑎 +no 𝑑 ) ⊆ ( 𝑎 +no 𝑏 ) )
37 36 adantr ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) ∧ ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) → ( 𝑎 +no 𝑑 ) ⊆ ( 𝑎 +no 𝑏 ) )
38 24 37 sstrd ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) ∧ ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) → ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑏 ) )
39 38 ex ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) → ( ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) → ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑏 ) ) )
40 39 ralimdva ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) → ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑏 ) ) )
41 40 imp ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) → ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑏 ) )
42 iunss ⊢ ( ∪ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑏 ) ↔ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑏 ) )
43 41 42 sylibr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) → ∪ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑏 ) )
44 22 23 43 syl2an ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ Lim 𝑏 ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +o 𝑑 ) ⊆ ( 𝑐 +no 𝑑 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +o 𝑏 ) ⊆ ( 𝑐 +no 𝑏 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → ∪ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑏 ) )
45 21 44 eqsstrd ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ Lim 𝑏 ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +o 𝑑 ) ⊆ ( 𝑐 +no 𝑑 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +o 𝑏 ) ⊆ ( 𝑐 +no 𝑏 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → ( 𝑎 +o 𝑏 ) ⊆ ( 𝑎 +no 𝑏 ) )
46 45 exp31 ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( Lim 𝑏 → ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +o 𝑑 ) ⊆ ( 𝑐 +no 𝑑 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +o 𝑏 ) ⊆ ( 𝑐 +no 𝑏 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) → ( 𝑎 +o 𝑏 ) ⊆ ( 𝑎 +no 𝑏 ) ) ) )
47 dflim3 ⊢ ( Lim 𝑏 ↔ ( Ord 𝑏 ∧ ¬ ( 𝑏 = ∅ ∨ ∃ 𝑑 ∈ On 𝑏 = suc 𝑑 ) ) )
48 47 notbii ⊢ ( ¬ Lim 𝑏 ↔ ¬ ( Ord 𝑏 ∧ ¬ ( 𝑏 = ∅ ∨ ∃ 𝑑 ∈ On 𝑏 = suc 𝑑 ) ) )
49 iman ⊢ ( ( Ord 𝑏 → ( 𝑏 = ∅ ∨ ∃ 𝑑 ∈ On 𝑏 = suc 𝑑 ) ) ↔ ¬ ( Ord 𝑏 ∧ ¬ ( 𝑏 = ∅ ∨ ∃ 𝑑 ∈ On 𝑏 = suc 𝑑 ) ) )
50 48 49 bitr4i ⊢ ( ¬ Lim 𝑏 ↔ ( Ord 𝑏 → ( 𝑏 = ∅ ∨ ∃ 𝑑 ∈ On 𝑏 = suc 𝑑 ) ) )
51 eloni ⊢ ( 𝑏 ∈ On → Ord 𝑏 )
52 pm5.5 ⊢ ( Ord 𝑏 → ( ( Ord 𝑏 → ( 𝑏 = ∅ ∨ ∃ 𝑑 ∈ On 𝑏 = suc 𝑑 ) ) ↔ ( 𝑏 = ∅ ∨ ∃ 𝑑 ∈ On 𝑏 = suc 𝑑 ) ) )
53 25 51 52 3syl ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( Ord 𝑏 → ( 𝑏 = ∅ ∨ ∃ 𝑑 ∈ On 𝑏 = suc 𝑑 ) ) ↔ ( 𝑏 = ∅ ∨ ∃ 𝑑 ∈ On 𝑏 = suc 𝑑 ) ) )
54 50 53 bitrid ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ¬ Lim 𝑏 ↔ ( 𝑏 = ∅ ∨ ∃ 𝑑 ∈ On 𝑏 = suc 𝑑 ) ) )
55 ssidd ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑏 = ∅ ) → 𝑎 ⊆ 𝑎 )
56 simpr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑏 = ∅ ) → 𝑏 = ∅ )
57 56 oveq2d ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑏 = ∅ ) → ( 𝑎 +o 𝑏 ) = ( 𝑎 +o ∅ ) )
58 simpll ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑏 = ∅ ) → 𝑎 ∈ On )
59 oa0 ⊢ ( 𝑎 ∈ On → ( 𝑎 +o ∅ ) = 𝑎 )
60 58 59 syl ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑏 = ∅ ) → ( 𝑎 +o ∅ ) = 𝑎 )
61 57 60 eqtrd ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑏 = ∅ ) → ( 𝑎 +o 𝑏 ) = 𝑎 )
62 56 oveq2d ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑏 = ∅ ) → ( 𝑎 +no 𝑏 ) = ( 𝑎 +no ∅ ) )
63 naddrid ⊢ ( 𝑎 ∈ On → ( 𝑎 +no ∅ ) = 𝑎 )
64 58 63 syl ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑏 = ∅ ) → ( 𝑎 +no ∅ ) = 𝑎 )
65 62 64 eqtrd ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑏 = ∅ ) → ( 𝑎 +no 𝑏 ) = 𝑎 )
66 55 61 65 3sstr4d ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑏 = ∅ ) → ( 𝑎 +o 𝑏 ) ⊆ ( 𝑎 +no 𝑏 ) )
67 66 a1d ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑏 = ∅ ) → ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +o 𝑑 ) ⊆ ( 𝑐 +no 𝑑 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +o 𝑏 ) ⊆ ( 𝑐 +no 𝑏 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) → ( 𝑎 +o 𝑏 ) ⊆ ( 𝑎 +no 𝑏 ) ) )
68 67 ex ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( 𝑏 = ∅ → ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +o 𝑑 ) ⊆ ( 𝑐 +no 𝑑 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +o 𝑏 ) ⊆ ( 𝑐 +no 𝑏 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) → ( 𝑎 +o 𝑏 ) ⊆ ( 𝑎 +no 𝑏 ) ) ) )
69 vex ⊢ 𝑑 ∈ V
70 69 sucid ⊢ 𝑑 ∈ suc 𝑑
71 simpr ⊢ ( ( 𝑑 ∈ On ∧ 𝑏 = suc 𝑑 ) → 𝑏 = suc 𝑑 )
72 70 71 eleqtrrid ⊢ ( ( 𝑑 ∈ On ∧ 𝑏 = suc 𝑑 ) → 𝑑 ∈ 𝑏 )
73 72 71 jca ⊢ ( ( 𝑑 ∈ On ∧ 𝑏 = suc 𝑑 ) → ( 𝑑 ∈ 𝑏 ∧ 𝑏 = suc 𝑑 ) )
74 73 a1i ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( 𝑑 ∈ On ∧ 𝑏 = suc 𝑑 ) → ( 𝑑 ∈ 𝑏 ∧ 𝑏 = suc 𝑑 ) ) )
75 74 reximdv2 ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ∃ 𝑑 ∈ On 𝑏 = suc 𝑑 → ∃ 𝑑 ∈ 𝑏 𝑏 = suc 𝑑 ) )
76 r19.29r ⊢ ( ( ∃ 𝑑 ∈ 𝑏 𝑏 = suc 𝑑 ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) → ∃ 𝑑 ∈ 𝑏 ( 𝑏 = suc 𝑑 ∧ ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) )
77 simprr ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) ∧ ( 𝑏 = suc 𝑑 ∧ ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) )
78 33 32 jca ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) → ( 𝑎 ∈ On ∧ 𝑑 ∈ On ) )
79 oacl ⊢ ( ( 𝑎 ∈ On ∧ 𝑑 ∈ On ) → ( 𝑎 +o 𝑑 ) ∈ On )
80 eloni ⊢ ( ( 𝑎 +o 𝑑 ) ∈ On → Ord ( 𝑎 +o 𝑑 ) )
81 79 80 syl ⊢ ( ( 𝑎 ∈ On ∧ 𝑑 ∈ On ) → Ord ( 𝑎 +o 𝑑 ) )
82 naddcl ⊢ ( ( 𝑎 ∈ On ∧ 𝑑 ∈ On ) → ( 𝑎 +no 𝑑 ) ∈ On )
83 eloni ⊢ ( ( 𝑎 +no 𝑑 ) ∈ On → Ord ( 𝑎 +no 𝑑 ) )
84 82 83 syl ⊢ ( ( 𝑎 ∈ On ∧ 𝑑 ∈ On ) → Ord ( 𝑎 +no 𝑑 ) )
85 81 84 jca ⊢ ( ( 𝑎 ∈ On ∧ 𝑑 ∈ On ) → ( Ord ( 𝑎 +o 𝑑 ) ∧ Ord ( 𝑎 +no 𝑑 ) ) )
86 ordsucsssuc ⊢ ( ( Ord ( 𝑎 +o 𝑑 ) ∧ Ord ( 𝑎 +no 𝑑 ) ) → ( ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ↔ suc ( 𝑎 +o 𝑑 ) ⊆ suc ( 𝑎 +no 𝑑 ) ) )
87 78 85 86 3syl ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) → ( ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ↔ suc ( 𝑎 +o 𝑑 ) ⊆ suc ( 𝑎 +no 𝑑 ) ) )
88 87 adantr ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) ∧ ( 𝑏 = suc 𝑑 ∧ ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → ( ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ↔ suc ( 𝑎 +o 𝑑 ) ⊆ suc ( 𝑎 +no 𝑑 ) ) )
89 77 88 mpbid ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) ∧ ( 𝑏 = suc 𝑑 ∧ ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → suc ( 𝑎 +o 𝑑 ) ⊆ suc ( 𝑎 +no 𝑑 ) )
90 simprl ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) ∧ ( 𝑏 = suc 𝑑 ∧ ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → 𝑏 = suc 𝑑 )
91 90 oveq2d ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) ∧ ( 𝑏 = suc 𝑑 ∧ ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → ( 𝑎 +o 𝑏 ) = ( 𝑎 +o suc 𝑑 ) )
92 78 adantr ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) ∧ ( 𝑏 = suc 𝑑 ∧ ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → ( 𝑎 ∈ On ∧ 𝑑 ∈ On ) )
93 oasuc ⊢ ( ( 𝑎 ∈ On ∧ 𝑑 ∈ On ) → ( 𝑎 +o suc 𝑑 ) = suc ( 𝑎 +o 𝑑 ) )
94 92 93 syl ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) ∧ ( 𝑏 = suc 𝑑 ∧ ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → ( 𝑎 +o suc 𝑑 ) = suc ( 𝑎 +o 𝑑 ) )
95 91 94 eqtrd ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) ∧ ( 𝑏 = suc 𝑑 ∧ ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → ( 𝑎 +o 𝑏 ) = suc ( 𝑎 +o 𝑑 ) )
96 90 oveq2d ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) ∧ ( 𝑏 = suc 𝑑 ∧ ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → ( 𝑎 +no 𝑏 ) = ( 𝑎 +no suc 𝑑 ) )
97 simplll ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) ∧ ( 𝑏 = suc 𝑑 ∧ ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → 𝑎 ∈ On )
98 31 ad4ant23 ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) ∧ ( 𝑏 = suc 𝑑 ∧ ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → 𝑑 ∈ On )
99 naddsuc2 ⊢ ( ( 𝑎 ∈ On ∧ 𝑑 ∈ On ) → ( 𝑎 +no suc 𝑑 ) = suc ( 𝑎 +no 𝑑 ) )
100 97 98 99 syl2anc ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) ∧ ( 𝑏 = suc 𝑑 ∧ ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → ( 𝑎 +no suc 𝑑 ) = suc ( 𝑎 +no 𝑑 ) )
101 96 100 eqtrd ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) ∧ ( 𝑏 = suc 𝑑 ∧ ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → ( 𝑎 +no 𝑏 ) = suc ( 𝑎 +no 𝑑 ) )
102 89 95 101 3sstr4d ⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝑑 ∈ 𝑏 ) ∧ ( 𝑏 = suc 𝑑 ∧ ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) ) → ( 𝑎 +o 𝑏 ) ⊆ ( 𝑎 +no 𝑏 ) )
103 102 rexlimdva2 ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ∃ 𝑑 ∈ 𝑏 ( 𝑏 = suc 𝑑 ∧ ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) → ( 𝑎 +o 𝑏 ) ⊆ ( 𝑎 +no 𝑏 ) ) )
104 76 103 syl5 ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( ∃ 𝑑 ∈ 𝑏 𝑏 = suc 𝑑 ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) → ( 𝑎 +o 𝑏 ) ⊆ ( 𝑎 +no 𝑏 ) ) )
105 104 expd ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ∃ 𝑑 ∈ 𝑏 𝑏 = suc 𝑑 → ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) → ( 𝑎 +o 𝑏 ) ⊆ ( 𝑎 +no 𝑏 ) ) ) )
106 23 105 syl7 ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ∃ 𝑑 ∈ 𝑏 𝑏 = suc 𝑑 → ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +o 𝑑 ) ⊆ ( 𝑐 +no 𝑑 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +o 𝑏 ) ⊆ ( 𝑐 +no 𝑏 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) → ( 𝑎 +o 𝑏 ) ⊆ ( 𝑎 +no 𝑏 ) ) ) )
107 75 106 syld ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ∃ 𝑑 ∈ On 𝑏 = suc 𝑑 → ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +o 𝑑 ) ⊆ ( 𝑐 +no 𝑑 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +o 𝑏 ) ⊆ ( 𝑐 +no 𝑏 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) → ( 𝑎 +o 𝑏 ) ⊆ ( 𝑎 +no 𝑏 ) ) ) )
108 68 107 jaod ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( 𝑏 = ∅ ∨ ∃ 𝑑 ∈ On 𝑏 = suc 𝑑 ) → ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +o 𝑑 ) ⊆ ( 𝑐 +no 𝑑 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +o 𝑏 ) ⊆ ( 𝑐 +no 𝑏 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) → ( 𝑎 +o 𝑏 ) ⊆ ( 𝑎 +no 𝑏 ) ) ) )
109 54 108 sylbid ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ¬ Lim 𝑏 → ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +o 𝑑 ) ⊆ ( 𝑐 +no 𝑑 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +o 𝑏 ) ⊆ ( 𝑐 +no 𝑏 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) → ( 𝑎 +o 𝑏 ) ⊆ ( 𝑎 +no 𝑏 ) ) ) )
110 46 109 pm2.61d ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +o 𝑑 ) ⊆ ( 𝑐 +no 𝑑 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +o 𝑏 ) ⊆ ( 𝑐 +no 𝑏 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +o 𝑑 ) ⊆ ( 𝑎 +no 𝑑 ) ) → ( 𝑎 +o 𝑏 ) ⊆ ( 𝑎 +no 𝑏 ) ) )
111 3 6 9 12 15 110 on2ind ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) ⊆ ( 𝐴 +no 𝐵 ) )