Metamath Proof Explorer

Theorem onov0suclim

Description: Compactly express rules for binary operations on ordinals. (Contributed by RP, 18-Jan-2025)

Ref Expression
Hypotheses onov0suclim.0 ⊢ ( 𝐴 ∈ On → ( 𝐴 ⊗ ∅ ) = 𝐷 )
onov0suclim.suc ⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ⊗ suc 𝐶 ) = 𝐸 )
onov0suclim.lim ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ Lim 𝐵 ) → ( 𝐴 ⊗ 𝐵 ) = 𝐹 )
Assertion onov0suclim ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐵 = ∅ → ( 𝐴 ⊗ 𝐵 ) = 𝐷 ) ∧ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐴 ⊗ 𝐵 ) = 𝐸 ) ∧ ( Lim 𝐵 → ( 𝐴 ⊗ 𝐵 ) = 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 onov0suclim.0 ⊢ ( 𝐴 ∈ On → ( 𝐴 ⊗ ∅ ) = 𝐷 )
2 onov0suclim.suc ⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ⊗ suc 𝐶 ) = 𝐸 )
3 onov0suclim.lim ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ Lim 𝐵 ) → ( 𝐴 ⊗ 𝐵 ) = 𝐹 )
4 eloni ⊢ ( 𝐵 ∈ On → Ord 𝐵 )
5 orduniorsuc ⊢ ( Ord 𝐵 → ( 𝐵 = ∪ 𝐵 ∨ 𝐵 = suc ∪ 𝐵 ) )
6 unizlim ⊢ ( Ord 𝐵 → ( 𝐵 = ∪ 𝐵 ↔ ( 𝐵 = ∅ ∨ Lim 𝐵 ) ) )
7 6 biimpd ⊢ ( Ord 𝐵 → ( 𝐵 = ∪ 𝐵 → ( 𝐵 = ∅ ∨ Lim 𝐵 ) ) )
8 7 orim1d ⊢ ( Ord 𝐵 → ( ( 𝐵 = ∪ 𝐵 ∨ 𝐵 = suc ∪ 𝐵 ) → ( ( 𝐵 = ∅ ∨ Lim 𝐵 ) ∨ 𝐵 = suc ∪ 𝐵 ) ) )
9 5 8 mpd ⊢ ( Ord 𝐵 → ( ( 𝐵 = ∅ ∨ Lim 𝐵 ) ∨ 𝐵 = suc ∪ 𝐵 ) )
10 4 9 syl ⊢ ( 𝐵 ∈ On → ( ( 𝐵 = ∅ ∨ Lim 𝐵 ) ∨ 𝐵 = suc ∪ 𝐵 ) )
11 10 adantl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐵 = ∅ ∨ Lim 𝐵 ) ∨ 𝐵 = suc ∪ 𝐵 ) )
12 oveq2 ⊢ ( 𝐵 = ∅ → ( 𝐴 ⊗ 𝐵 ) = ( 𝐴 ⊗ ∅ ) )
13 12 1 sylan9eqr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 = ∅ ) → ( 𝐴 ⊗ 𝐵 ) = 𝐷 )
14 13 ex ⊢ ( 𝐴 ∈ On → ( 𝐵 = ∅ → ( 𝐴 ⊗ 𝐵 ) = 𝐷 ) )
15 14 ad2antrr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐵 = ∅ ) → ( 𝐵 = ∅ → ( 𝐴 ⊗ 𝐵 ) = 𝐷 ) )
16 eloni ⊢ ( 𝐶 ∈ On → Ord 𝐶 )
17 0elsuc ⊢ ( Ord 𝐶 → ∅ ∈ suc 𝐶 )
18 16 17 syl ⊢ ( 𝐶 ∈ On → ∅ ∈ suc 𝐶 )
19 18 adantl ⊢ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ∅ ∈ suc 𝐶 )
20 simpl ⊢ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → 𝐵 = suc 𝐶 )
21 19 20 eleqtrrd ⊢ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ∅ ∈ 𝐵 )
22 n0i ⊢ ( ∅ ∈ 𝐵 → ¬ 𝐵 = ∅ )
23 21 22 syl ⊢ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ¬ 𝐵 = ∅ )
24 23 pm2.21d ⊢ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐵 = ∅ → ( 𝐴 ⊗ 𝐵 ) = 𝐸 ) )
25 24 adantl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) ) → ( 𝐵 = ∅ → ( 𝐴 ⊗ 𝐵 ) = 𝐸 ) )
26 25 impancom ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐵 = ∅ ) → ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐴 ⊗ 𝐵 ) = 𝐸 ) )
27 nlim0 ⊢ ¬ Lim ∅
28 limeq ⊢ ( 𝐵 = ∅ → ( Lim 𝐵 ↔ Lim ∅ ) )
29 27 28 mtbiri ⊢ ( 𝐵 = ∅ → ¬ Lim 𝐵 )
30 29 adantl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐵 = ∅ ) → ¬ Lim 𝐵 )
31 30 pm2.21d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐵 = ∅ ) → ( Lim 𝐵 → ( 𝐴 ⊗ 𝐵 ) = 𝐹 ) )
32 15 26 31 3jca ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐵 = ∅ ) → ( ( 𝐵 = ∅ → ( 𝐴 ⊗ 𝐵 ) = 𝐷 ) ∧ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐴 ⊗ 𝐵 ) = 𝐸 ) ∧ ( Lim 𝐵 → ( 𝐴 ⊗ 𝐵 ) = 𝐹 ) ) )
33 32 ex ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 = ∅ → ( ( 𝐵 = ∅ → ( 𝐴 ⊗ 𝐵 ) = 𝐷 ) ∧ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐴 ⊗ 𝐵 ) = 𝐸 ) ∧ ( Lim 𝐵 → ( 𝐴 ⊗ 𝐵 ) = 𝐹 ) ) ) )
34 29 con2i ⊢ ( Lim 𝐵 → ¬ 𝐵 = ∅ )
35 34 adantl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ Lim 𝐵 ) → ¬ 𝐵 = ∅ )
36 35 pm2.21d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ Lim 𝐵 ) → ( 𝐵 = ∅ → ( 𝐴 ⊗ 𝐵 ) = 𝐷 ) )
37 limeq ⊢ ( 𝐵 = suc 𝐶 → ( Lim 𝐵 ↔ Lim suc 𝐶 ) )
38 37 notbid ⊢ ( 𝐵 = suc 𝐶 → ( ¬ Lim 𝐵 ↔ ¬ Lim suc 𝐶 ) )
39 38 biimprd ⊢ ( 𝐵 = suc 𝐶 → ( ¬ Lim suc 𝐶 → ¬ Lim 𝐵 ) )
40 nlimsucg ⊢ ( 𝐶 ∈ On → ¬ Lim suc 𝐶 )
41 39 40 impel ⊢ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ¬ Lim 𝐵 )
42 41 adantl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) ) → ¬ Lim 𝐵 )
43 42 pm2.21d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) ) → ( Lim 𝐵 → ( 𝐴 ⊗ 𝐵 ) = 𝐸 ) )
44 43 impancom ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ Lim 𝐵 ) → ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐴 ⊗ 𝐵 ) = 𝐸 ) )
45 3 a1d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ Lim 𝐵 ) → ( Lim 𝐵 → ( 𝐴 ⊗ 𝐵 ) = 𝐹 ) )
46 36 44 45 3jca ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ Lim 𝐵 ) → ( ( 𝐵 = ∅ → ( 𝐴 ⊗ 𝐵 ) = 𝐷 ) ∧ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐴 ⊗ 𝐵 ) = 𝐸 ) ∧ ( Lim 𝐵 → ( 𝐴 ⊗ 𝐵 ) = 𝐹 ) ) )
47 46 ex ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( Lim 𝐵 → ( ( 𝐵 = ∅ → ( 𝐴 ⊗ 𝐵 ) = 𝐷 ) ∧ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐴 ⊗ 𝐵 ) = 𝐸 ) ∧ ( Lim 𝐵 → ( 𝐴 ⊗ 𝐵 ) = 𝐹 ) ) ) )
48 33 47 jaod ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐵 = ∅ ∨ Lim 𝐵 ) → ( ( 𝐵 = ∅ → ( 𝐴 ⊗ 𝐵 ) = 𝐷 ) ∧ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐴 ⊗ 𝐵 ) = 𝐸 ) ∧ ( Lim 𝐵 → ( 𝐴 ⊗ 𝐵 ) = 𝐹 ) ) ) )
49 1n0 ⊢ 1o ≠ ∅
50 necom ⊢ ( 1o ≠ ∅ ↔ ∅ ≠ 1o )
51 df-1o ⊢ 1o = suc ∅
52 uni0 ⊢ ∪ ∅ = ∅
53 suceq ⊢ ( ∪ ∅ = ∅ → suc ∪ ∅ = suc ∅ )
54 52 53 ax-mp ⊢ suc ∪ ∅ = suc ∅
55 51 54 eqtr4i ⊢ 1o = suc ∪ ∅
56 55 neeq2i ⊢ ( ∅ ≠ 1o ↔ ∅ ≠ suc ∪ ∅ )
57 df-ne ⊢ ( ∅ ≠ suc ∪ ∅ ↔ ¬ ∅ = suc ∪ ∅ )
58 50 56 57 3bitri ⊢ ( 1o ≠ ∅ ↔ ¬ ∅ = suc ∪ ∅ )
59 id ⊢ ( 𝐵 = ∅ → 𝐵 = ∅ )
60 unieq ⊢ ( 𝐵 = ∅ → ∪ 𝐵 = ∪ ∅ )
61 suceq ⊢ ( ∪ 𝐵 = ∪ ∅ → suc ∪ 𝐵 = suc ∪ ∅ )
62 60 61 syl ⊢ ( 𝐵 = ∅ → suc ∪ 𝐵 = suc ∪ ∅ )
63 59 62 eqeq12d ⊢ ( 𝐵 = ∅ → ( 𝐵 = suc ∪ 𝐵 ↔ ∅ = suc ∪ ∅ ) )
64 63 notbid ⊢ ( 𝐵 = ∅ → ( ¬ 𝐵 = suc ∪ 𝐵 ↔ ¬ ∅ = suc ∪ ∅ ) )
65 58 64 bitr4id ⊢ ( 𝐵 = ∅ → ( 1o ≠ ∅ ↔ ¬ 𝐵 = suc ∪ 𝐵 ) )
66 49 65 mpbii ⊢ ( 𝐵 = ∅ → ¬ 𝐵 = suc ∪ 𝐵 )
67 66 con2i ⊢ ( 𝐵 = suc ∪ 𝐵 → ¬ 𝐵 = ∅ )
68 67 adantl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐵 = suc ∪ 𝐵 ) → ¬ 𝐵 = ∅ )
69 68 pm2.21d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐵 = suc ∪ 𝐵 ) → ( 𝐵 = ∅ → ( 𝐴 ⊗ 𝐵 ) = 𝐷 ) )
70 simprl ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) ) → 𝐵 = suc 𝐶 )
71 70 oveq2d ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) ) → ( 𝐴 ⊗ 𝐵 ) = ( 𝐴 ⊗ suc 𝐶 ) )
72 2 adantrl ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) ) → ( 𝐴 ⊗ suc 𝐶 ) = 𝐸 )
73 71 72 eqtrd ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) ) → ( 𝐴 ⊗ 𝐵 ) = 𝐸 )
74 73 ex ⊢ ( 𝐴 ∈ On → ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐴 ⊗ 𝐵 ) = 𝐸 ) )
75 74 ad2antrr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐵 = suc ∪ 𝐵 ) → ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐴 ⊗ 𝐵 ) = 𝐸 ) )
76 onuni ⊢ ( 𝐵 ∈ On → ∪ 𝐵 ∈ On )
77 nlimsucg ⊢ ( ∪ 𝐵 ∈ On → ¬ Lim suc ∪ 𝐵 )
78 76 77 syl ⊢ ( 𝐵 ∈ On → ¬ Lim suc ∪ 𝐵 )
79 limeq ⊢ ( 𝐵 = suc ∪ 𝐵 → ( Lim 𝐵 ↔ Lim suc ∪ 𝐵 ) )
80 79 notbid ⊢ ( 𝐵 = suc ∪ 𝐵 → ( ¬ Lim 𝐵 ↔ ¬ Lim suc ∪ 𝐵 ) )
81 80 biimprd ⊢ ( 𝐵 = suc ∪ 𝐵 → ( ¬ Lim suc ∪ 𝐵 → ¬ Lim 𝐵 ) )
82 78 81 mpan9 ⊢ ( ( 𝐵 ∈ On ∧ 𝐵 = suc ∪ 𝐵 ) → ¬ Lim 𝐵 )
83 82 adantll ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐵 = suc ∪ 𝐵 ) → ¬ Lim 𝐵 )
84 83 pm2.21d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐵 = suc ∪ 𝐵 ) → ( Lim 𝐵 → ( 𝐴 ⊗ 𝐵 ) = 𝐹 ) )
85 69 75 84 3jca ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐵 = suc ∪ 𝐵 ) → ( ( 𝐵 = ∅ → ( 𝐴 ⊗ 𝐵 ) = 𝐷 ) ∧ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐴 ⊗ 𝐵 ) = 𝐸 ) ∧ ( Lim 𝐵 → ( 𝐴 ⊗ 𝐵 ) = 𝐹 ) ) )
86 85 ex ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 = suc ∪ 𝐵 → ( ( 𝐵 = ∅ → ( 𝐴 ⊗ 𝐵 ) = 𝐷 ) ∧ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐴 ⊗ 𝐵 ) = 𝐸 ) ∧ ( Lim 𝐵 → ( 𝐴 ⊗ 𝐵 ) = 𝐹 ) ) ) )
87 48 86 jaod ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( ( 𝐵 = ∅ ∨ Lim 𝐵 ) ∨ 𝐵 = suc ∪ 𝐵 ) → ( ( 𝐵 = ∅ → ( 𝐴 ⊗ 𝐵 ) = 𝐷 ) ∧ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐴 ⊗ 𝐵 ) = 𝐸 ) ∧ ( Lim 𝐵 → ( 𝐴 ⊗ 𝐵 ) = 𝐹 ) ) ) )
88 11 87 mpd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐵 = ∅ → ( 𝐴 ⊗ 𝐵 ) = 𝐷 ) ∧ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐴 ⊗ 𝐵 ) = 𝐸 ) ∧ ( Lim 𝐵 → ( 𝐴 ⊗ 𝐵 ) = 𝐹 ) ) )