Metamath Proof Explorer

Theorem omlimcl

Description: The product of any nonzero ordinal with a limit ordinal is a limit ordinal. Proposition 8.24 of TakeutiZaring p. 64. (Contributed by NM, 25-Dec-2004)

Ref Expression
Assertion omlimcl ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → Lim ( 𝐴 ·o 𝐵 ) )

Proof

Step Hyp Ref Expression
1 limelon ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → 𝐵 ∈ On )
2 omcl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) ∈ On )
3 eloni ⊢ ( ( 𝐴 ·o 𝐵 ) ∈ On → Ord ( 𝐴 ·o 𝐵 ) )
4 2 3 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → Ord ( 𝐴 ·o 𝐵 ) )
5 1 4 sylan2 ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → Ord ( 𝐴 ·o 𝐵 ) )
6 5 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → Ord ( 𝐴 ·o 𝐵 ) )
7 0ellim ⊢ ( Lim 𝐵 → ∅ ∈ 𝐵 )
8 n0i ⊢ ( ∅ ∈ 𝐵 → ¬ 𝐵 = ∅ )
9 7 8 syl ⊢ ( Lim 𝐵 → ¬ 𝐵 = ∅ )
10 n0i ⊢ ( ∅ ∈ 𝐴 → ¬ 𝐴 = ∅ )
11 9 10 anim12ci ⊢ ( ( Lim 𝐵 ∧ ∅ ∈ 𝐴 ) → ( ¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅ ) )
12 11 adantll ⊢ ( ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ( ¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅ ) )
13 12 adantll ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( ¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅ ) )
14 om00 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ·o 𝐵 ) = ∅ ↔ ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) ) )
15 14 notbid ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ¬ ( 𝐴 ·o 𝐵 ) = ∅ ↔ ¬ ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) ) )
16 ioran ⊢ ( ¬ ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) ↔ ( ¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅ ) )
17 15 16 bitrdi ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ¬ ( 𝐴 ·o 𝐵 ) = ∅ ↔ ( ¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅ ) ) )
18 1 17 sylan2 ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( ¬ ( 𝐴 ·o 𝐵 ) = ∅ ↔ ( ¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅ ) ) )
19 18 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( ¬ ( 𝐴 ·o 𝐵 ) = ∅ ↔ ( ¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅ ) ) )
20 13 19 mpbird ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ¬ ( 𝐴 ·o 𝐵 ) = ∅ )
21 vex ⊢ 𝑦 ∈ V
22 21 sucid ⊢ 𝑦 ∈ suc 𝑦
23 omlim ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( 𝐴 ·o 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ·o 𝑥 ) )
24 eqeq1 ⊢ ( ( 𝐴 ·o 𝐵 ) = suc 𝑦 → ( ( 𝐴 ·o 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ·o 𝑥 ) ↔ suc 𝑦 = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ·o 𝑥 ) ) )
25 24 biimpac ⊢ ( ( ( 𝐴 ·o 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ·o 𝑥 ) ∧ ( 𝐴 ·o 𝐵 ) = suc 𝑦 ) → suc 𝑦 = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ·o 𝑥 ) )
26 23 25 sylan ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ( 𝐴 ·o 𝐵 ) = suc 𝑦 ) → suc 𝑦 = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ·o 𝑥 ) )
27 22 26 eleqtrid ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ( 𝐴 ·o 𝐵 ) = suc 𝑦 ) → 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 ( 𝐴 ·o 𝑥 ) )
28 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 ( 𝐴 ·o 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐵 𝑦 ∈ ( 𝐴 ·o 𝑥 ) )
29 27 28 sylib ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ( 𝐴 ·o 𝐵 ) = suc 𝑦 ) → ∃ 𝑥 ∈ 𝐵 𝑦 ∈ ( 𝐴 ·o 𝑥 ) )
30 29 adantlr ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐴 ·o 𝐵 ) = suc 𝑦 ) → ∃ 𝑥 ∈ 𝐵 𝑦 ∈ ( 𝐴 ·o 𝑥 ) )
31 onelon ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ On )
32 1 31 sylan ⊢ ( ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ On )
33 onnbtwn ⊢ ( 𝑥 ∈ On → ¬ ( 𝑥 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝑥 ) )
34 imnan ⊢ ( ( 𝑥 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝑥 ) ↔ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝑥 ) )
35 33 34 sylibr ⊢ ( 𝑥 ∈ On → ( 𝑥 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝑥 ) )
36 35 com12 ⊢ ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ On → ¬ 𝐵 ∈ suc 𝑥 ) )
37 36 adantl ⊢ ( ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ On → ¬ 𝐵 ∈ suc 𝑥 ) )
38 32 37 mpd ⊢ ( ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ¬ 𝐵 ∈ suc 𝑥 )
39 38 ad5ant24 ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 ·o 𝑥 ) ) → ¬ 𝐵 ∈ suc 𝑥 )
40 simpl ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ 𝐵 ) → 𝐵 ∈ On )
41 40 31 jca ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ 𝐵 ) → ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) )
42 1 41 sylan ⊢ ( ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) )
43 42 anim2i ⊢ ( ( 𝐴 ∈ On ∧ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) ) )
44 43 anassrs ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) ) )
45 omcl ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( 𝐴 ·o 𝑥 ) ∈ On )
46 eloni ⊢ ( ( 𝐴 ·o 𝑥 ) ∈ On → Ord ( 𝐴 ·o 𝑥 ) )
47 ordsucelsuc ⊢ ( Ord ( 𝐴 ·o 𝑥 ) → ( 𝑦 ∈ ( 𝐴 ·o 𝑥 ) ↔ suc 𝑦 ∈ suc ( 𝐴 ·o 𝑥 ) ) )
48 46 47 syl ⊢ ( ( 𝐴 ·o 𝑥 ) ∈ On → ( 𝑦 ∈ ( 𝐴 ·o 𝑥 ) ↔ suc 𝑦 ∈ suc ( 𝐴 ·o 𝑥 ) ) )
49 oa1suc ⊢ ( ( 𝐴 ·o 𝑥 ) ∈ On → ( ( 𝐴 ·o 𝑥 ) +o 1o ) = suc ( 𝐴 ·o 𝑥 ) )
50 49 eleq2d ⊢ ( ( 𝐴 ·o 𝑥 ) ∈ On → ( suc 𝑦 ∈ ( ( 𝐴 ·o 𝑥 ) +o 1o ) ↔ suc 𝑦 ∈ suc ( 𝐴 ·o 𝑥 ) ) )
51 48 50 bitr4d ⊢ ( ( 𝐴 ·o 𝑥 ) ∈ On → ( 𝑦 ∈ ( 𝐴 ·o 𝑥 ) ↔ suc 𝑦 ∈ ( ( 𝐴 ·o 𝑥 ) +o 1o ) ) )
52 45 51 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑦 ∈ ( 𝐴 ·o 𝑥 ) ↔ suc 𝑦 ∈ ( ( 𝐴 ·o 𝑥 ) +o 1o ) ) )
53 52 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝐴 ·o 𝑥 ) ↔ suc 𝑦 ∈ ( ( 𝐴 ·o 𝑥 ) +o 1o ) ) )
54 eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
55 ordgt0ge1 ⊢ ( Ord 𝐴 → ( ∅ ∈ 𝐴 ↔ 1o ⊆ 𝐴 ) )
56 54 55 syl ⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ 1o ⊆ 𝐴 ) )
57 56 adantr ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( ∅ ∈ 𝐴 ↔ 1o ⊆ 𝐴 ) )
58 1on ⊢ 1o ∈ On
59 oaword ⊢ ( ( 1o ∈ On ∧ 𝐴 ∈ On ∧ ( 𝐴 ·o 𝑥 ) ∈ On ) → ( 1o ⊆ 𝐴 ↔ ( ( 𝐴 ·o 𝑥 ) +o 1o ) ⊆ ( ( 𝐴 ·o 𝑥 ) +o 𝐴 ) ) )
60 58 59 mp3an1 ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐴 ·o 𝑥 ) ∈ On ) → ( 1o ⊆ 𝐴 ↔ ( ( 𝐴 ·o 𝑥 ) +o 1o ) ⊆ ( ( 𝐴 ·o 𝑥 ) +o 𝐴 ) ) )
61 45 60 syldan ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( 1o ⊆ 𝐴 ↔ ( ( 𝐴 ·o 𝑥 ) +o 1o ) ⊆ ( ( 𝐴 ·o 𝑥 ) +o 𝐴 ) ) )
62 57 61 bitrd ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( ∅ ∈ 𝐴 ↔ ( ( 𝐴 ·o 𝑥 ) +o 1o ) ⊆ ( ( 𝐴 ·o 𝑥 ) +o 𝐴 ) ) )
63 62 biimpa ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝐴 ·o 𝑥 ) +o 1o ) ⊆ ( ( 𝐴 ·o 𝑥 ) +o 𝐴 ) )
64 omsuc ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( 𝐴 ·o suc 𝑥 ) = ( ( 𝐴 ·o 𝑥 ) +o 𝐴 ) )
65 64 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ·o suc 𝑥 ) = ( ( 𝐴 ·o 𝑥 ) +o 𝐴 ) )
66 63 65 sseqtrrd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝐴 ·o 𝑥 ) +o 1o ) ⊆ ( 𝐴 ·o suc 𝑥 ) )
67 66 sseld ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( suc 𝑦 ∈ ( ( 𝐴 ·o 𝑥 ) +o 1o ) → suc 𝑦 ∈ ( 𝐴 ·o suc 𝑥 ) ) )
68 53 67 sylbid ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝐴 ·o 𝑥 ) → suc 𝑦 ∈ ( 𝐴 ·o suc 𝑥 ) ) )
69 eleq1 ⊢ ( ( 𝐴 ·o 𝐵 ) = suc 𝑦 → ( ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o suc 𝑥 ) ↔ suc 𝑦 ∈ ( 𝐴 ·o suc 𝑥 ) ) )
70 69 biimprd ⊢ ( ( 𝐴 ·o 𝐵 ) = suc 𝑦 → ( suc 𝑦 ∈ ( 𝐴 ·o suc 𝑥 ) → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o suc 𝑥 ) ) )
71 68 70 syl9 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝐴 ·o 𝐵 ) = suc 𝑦 → ( 𝑦 ∈ ( 𝐴 ·o 𝑥 ) → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o suc 𝑥 ) ) ) )
72 71 com23 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝐴 ·o 𝑥 ) → ( ( 𝐴 ·o 𝐵 ) = suc 𝑦 → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o suc 𝑥 ) ) ) )
73 72 adantlrl ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝐴 ·o 𝑥 ) → ( ( 𝐴 ·o 𝐵 ) = suc 𝑦 → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o suc 𝑥 ) ) ) )
74 sucelon ⊢ ( 𝑥 ∈ On ↔ suc 𝑥 ∈ On )
75 omord ⊢ ( ( 𝐵 ∈ On ∧ suc 𝑥 ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝐵 ∈ suc 𝑥 ∧ ∅ ∈ 𝐴 ) ↔ ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o suc 𝑥 ) ) )
76 simpl ⊢ ( ( 𝐵 ∈ suc 𝑥 ∧ ∅ ∈ 𝐴 ) → 𝐵 ∈ suc 𝑥 )
77 75 76 syl6bir ⊢ ( ( 𝐵 ∈ On ∧ suc 𝑥 ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o suc 𝑥 ) → 𝐵 ∈ suc 𝑥 ) )
78 74 77 syl3an2b ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o suc 𝑥 ) → 𝐵 ∈ suc 𝑥 ) )
79 78 3comr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑥 ∈ On ) → ( ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o suc 𝑥 ) → 𝐵 ∈ suc 𝑥 ) )
80 79 3expb ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) ) → ( ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o suc 𝑥 ) → 𝐵 ∈ suc 𝑥 ) )
81 80 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o suc 𝑥 ) → 𝐵 ∈ suc 𝑥 ) )
82 73 81 syl6d ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝐴 ·o 𝑥 ) → ( ( 𝐴 ·o 𝐵 ) = suc 𝑦 → 𝐵 ∈ suc 𝑥 ) ) )
83 44 82 sylan ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝐴 ·o 𝑥 ) → ( ( 𝐴 ·o 𝐵 ) = suc 𝑦 → 𝐵 ∈ suc 𝑥 ) ) )
84 83 an32s ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑦 ∈ ( 𝐴 ·o 𝑥 ) → ( ( 𝐴 ·o 𝐵 ) = suc 𝑦 → 𝐵 ∈ suc 𝑥 ) ) )
85 84 imp ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 ·o 𝑥 ) ) → ( ( 𝐴 ·o 𝐵 ) = suc 𝑦 → 𝐵 ∈ suc 𝑥 ) )
86 39 85 mtod ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 ·o 𝑥 ) ) → ¬ ( 𝐴 ·o 𝐵 ) = suc 𝑦 )
87 86 rexlimdva2 ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( ∃ 𝑥 ∈ 𝐵 𝑦 ∈ ( 𝐴 ·o 𝑥 ) → ¬ ( 𝐴 ·o 𝐵 ) = suc 𝑦 ) )
88 87 adantr ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐴 ·o 𝐵 ) = suc 𝑦 ) → ( ∃ 𝑥 ∈ 𝐵 𝑦 ∈ ( 𝐴 ·o 𝑥 ) → ¬ ( 𝐴 ·o 𝐵 ) = suc 𝑦 ) )
89 30 88 mpd ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐴 ·o 𝐵 ) = suc 𝑦 ) → ¬ ( 𝐴 ·o 𝐵 ) = suc 𝑦 )
90 89 pm2.01da ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ¬ ( 𝐴 ·o 𝐵 ) = suc 𝑦 )
91 90 adantr ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ 𝑦 ∈ On ) → ¬ ( 𝐴 ·o 𝐵 ) = suc 𝑦 )
92 91 nrexdv ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ¬ ∃ 𝑦 ∈ On ( 𝐴 ·o 𝐵 ) = suc 𝑦 )
93 ioran ⊢ ( ¬ ( ( 𝐴 ·o 𝐵 ) = ∅ ∨ ∃ 𝑦 ∈ On ( 𝐴 ·o 𝐵 ) = suc 𝑦 ) ↔ ( ¬ ( 𝐴 ·o 𝐵 ) = ∅ ∧ ¬ ∃ 𝑦 ∈ On ( 𝐴 ·o 𝐵 ) = suc 𝑦 ) )
94 20 92 93 sylanbrc ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ¬ ( ( 𝐴 ·o 𝐵 ) = ∅ ∨ ∃ 𝑦 ∈ On ( 𝐴 ·o 𝐵 ) = suc 𝑦 ) )
95 dflim3 ⊢ ( Lim ( 𝐴 ·o 𝐵 ) ↔ ( Ord ( 𝐴 ·o 𝐵 ) ∧ ¬ ( ( 𝐴 ·o 𝐵 ) = ∅ ∨ ∃ 𝑦 ∈ On ( 𝐴 ·o 𝐵 ) = suc 𝑦 ) ) )
96 6 94 95 sylanbrc ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → Lim ( 𝐴 ·o 𝐵 ) )