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 
|- ( A e. On -> ( A .(x) (/) ) = D )
onov0suclim.suc 
|- ( ( A e. On /\ C e. On ) -> ( A .(x) suc C ) = E )
onov0suclim.lim 
|- ( ( ( A e. On /\ B e. On ) /\ Lim B ) -> ( A .(x) B ) = F )
Assertion onov0suclim 
|- ( ( A e. On /\ B e. On ) -> ( ( B = (/) -> ( A .(x) B ) = D ) /\ ( ( B = suc C /\ C e. On ) -> ( A .(x) B ) = E ) /\ ( Lim B -> ( A .(x) B ) = F ) ) )

Proof

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