MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  omlimcl Structured version   Visualization version   GIF version

Theorem omlimcl 8525
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.)
Assertion
Ref Expression
omlimcl (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → Lim (𝐴 ·o 𝐵))

Proof of Theorem omlimcl
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 limelon 6381 . . . 4 ((𝐵𝐶 ∧ Lim 𝐵) → 𝐵 ∈ On)
2 omcl 8482 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) ∈ On)
3 eloni 6327 . . . . 5 ((𝐴 ·o 𝐵) ∈ On → Ord (𝐴 ·o 𝐵))
42, 3syl 17 . . . 4 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Ord (𝐴 ·o 𝐵))
51, 4sylan2 593 . . 3 ((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) → Ord (𝐴 ·o 𝐵))
65adantr 481 . 2 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → Ord (𝐴 ·o 𝐵))
7 0ellim 6380 . . . . . . . 8 (Lim 𝐵 → ∅ ∈ 𝐵)
8 n0i 4293 . . . . . . . 8 (∅ ∈ 𝐵 → ¬ 𝐵 = ∅)
97, 8syl 17 . . . . . . 7 (Lim 𝐵 → ¬ 𝐵 = ∅)
10 n0i 4293 . . . . . . 7 (∅ ∈ 𝐴 → ¬ 𝐴 = ∅)
119, 10anim12ci 614 . . . . . 6 ((Lim 𝐵 ∧ ∅ ∈ 𝐴) → (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅))
1211adantll 712 . . . . 5 (((𝐵𝐶 ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅))
1312adantll 712 . . . 4 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅))
14 om00 8522 . . . . . . . 8 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅)))
1514notbid 317 . . . . . . 7 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (¬ (𝐴 ·o 𝐵) = ∅ ↔ ¬ (𝐴 = ∅ ∨ 𝐵 = ∅)))
16 ioran 982 . . . . . . 7 (¬ (𝐴 = ∅ ∨ 𝐵 = ∅) ↔ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅))
1715, 16bitrdi 286 . . . . . 6 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (¬ (𝐴 ·o 𝐵) = ∅ ↔ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
181, 17sylan2 593 . . . . 5 ((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) → (¬ (𝐴 ·o 𝐵) = ∅ ↔ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
1918adantr 481 . . . 4 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (¬ (𝐴 ·o 𝐵) = ∅ ↔ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
2013, 19mpbird 256 . . 3 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → ¬ (𝐴 ·o 𝐵) = ∅)
21 vex 3449 . . . . . . . . . . 11 𝑦 ∈ V
2221sucid 6399 . . . . . . . . . 10 𝑦 ∈ suc 𝑦
23 omlim 8479 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) → (𝐴 ·o 𝐵) = 𝑥𝐵 (𝐴 ·o 𝑥))
24 eqeq1 2740 . . . . . . . . . . . 12 ((𝐴 ·o 𝐵) = suc 𝑦 → ((𝐴 ·o 𝐵) = 𝑥𝐵 (𝐴 ·o 𝑥) ↔ suc 𝑦 = 𝑥𝐵 (𝐴 ·o 𝑥)))
2524biimpac 479 . . . . . . . . . . 11 (((𝐴 ·o 𝐵) = 𝑥𝐵 (𝐴 ·o 𝑥) ∧ (𝐴 ·o 𝐵) = suc 𝑦) → suc 𝑦 = 𝑥𝐵 (𝐴 ·o 𝑥))
2623, 25sylan 580 . . . . . . . . . 10 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ (𝐴 ·o 𝐵) = suc 𝑦) → suc 𝑦 = 𝑥𝐵 (𝐴 ·o 𝑥))
2722, 26eleqtrid 2844 . . . . . . . . 9 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ (𝐴 ·o 𝐵) = suc 𝑦) → 𝑦 𝑥𝐵 (𝐴 ·o 𝑥))
28 eliun 4958 . . . . . . . . 9 (𝑦 𝑥𝐵 (𝐴 ·o 𝑥) ↔ ∃𝑥𝐵 𝑦 ∈ (𝐴 ·o 𝑥))
2927, 28sylib 217 . . . . . . . 8 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ (𝐴 ·o 𝐵) = suc 𝑦) → ∃𝑥𝐵 𝑦 ∈ (𝐴 ·o 𝑥))
3029adantlr 713 . . . . . . 7 ((((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ (𝐴 ·o 𝐵) = suc 𝑦) → ∃𝑥𝐵 𝑦 ∈ (𝐴 ·o 𝑥))
31 onelon 6342 . . . . . . . . . . . . 13 ((𝐵 ∈ On ∧ 𝑥𝐵) → 𝑥 ∈ On)
321, 31sylan 580 . . . . . . . . . . . 12 (((𝐵𝐶 ∧ Lim 𝐵) ∧ 𝑥𝐵) → 𝑥 ∈ On)
33 onnbtwn 6411 . . . . . . . . . . . . . . 15 (𝑥 ∈ On → ¬ (𝑥𝐵𝐵 ∈ suc 𝑥))
34 imnan 400 . . . . . . . . . . . . . . 15 ((𝑥𝐵 → ¬ 𝐵 ∈ suc 𝑥) ↔ ¬ (𝑥𝐵𝐵 ∈ suc 𝑥))
3533, 34sylibr 233 . . . . . . . . . . . . . 14 (𝑥 ∈ On → (𝑥𝐵 → ¬ 𝐵 ∈ suc 𝑥))
3635com12 32 . . . . . . . . . . . . 13 (𝑥𝐵 → (𝑥 ∈ On → ¬ 𝐵 ∈ suc 𝑥))
3736adantl 482 . . . . . . . . . . . 12 (((𝐵𝐶 ∧ Lim 𝐵) ∧ 𝑥𝐵) → (𝑥 ∈ On → ¬ 𝐵 ∈ suc 𝑥))
3832, 37mpd 15 . . . . . . . . . . 11 (((𝐵𝐶 ∧ Lim 𝐵) ∧ 𝑥𝐵) → ¬ 𝐵 ∈ suc 𝑥)
3938ad5ant24 759 . . . . . . . . . 10 (((((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝑥𝐵) ∧ 𝑦 ∈ (𝐴 ·o 𝑥)) → ¬ 𝐵 ∈ suc 𝑥)
40 simpl 483 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ On ∧ 𝑥𝐵) → 𝐵 ∈ On)
4140, 31jca 512 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ On ∧ 𝑥𝐵) → (𝐵 ∈ On ∧ 𝑥 ∈ On))
421, 41sylan 580 . . . . . . . . . . . . . . 15 (((𝐵𝐶 ∧ Lim 𝐵) ∧ 𝑥𝐵) → (𝐵 ∈ On ∧ 𝑥 ∈ On))
4342anim2i 617 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ ((𝐵𝐶 ∧ Lim 𝐵) ∧ 𝑥𝐵)) → (𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑥 ∈ On)))
4443anassrs 468 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ 𝑥𝐵) → (𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑥 ∈ On)))
45 omcl 8482 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·o 𝑥) ∈ On)
46 eloni 6327 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ·o 𝑥) ∈ On → Ord (𝐴 ·o 𝑥))
47 ordsucelsuc 7757 . . . . . . . . . . . . . . . . . . . . . 22 (Ord (𝐴 ·o 𝑥) → (𝑦 ∈ (𝐴 ·o 𝑥) ↔ suc 𝑦 ∈ suc (𝐴 ·o 𝑥)))
4846, 47syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ·o 𝑥) ∈ On → (𝑦 ∈ (𝐴 ·o 𝑥) ↔ suc 𝑦 ∈ suc (𝐴 ·o 𝑥)))
49 oa1suc 8477 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ·o 𝑥) ∈ On → ((𝐴 ·o 𝑥) +o 1o) = suc (𝐴 ·o 𝑥))
5049eleq2d 2823 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ·o 𝑥) ∈ On → (suc 𝑦 ∈ ((𝐴 ·o 𝑥) +o 1o) ↔ suc 𝑦 ∈ suc (𝐴 ·o 𝑥)))
5148, 50bitr4d 281 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ·o 𝑥) ∈ On → (𝑦 ∈ (𝐴 ·o 𝑥) ↔ suc 𝑦 ∈ ((𝐴 ·o 𝑥) +o 1o)))
5245, 51syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝑦 ∈ (𝐴 ·o 𝑥) ↔ suc 𝑦 ∈ ((𝐴 ·o 𝑥) +o 1o)))
5352adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑦 ∈ (𝐴 ·o 𝑥) ↔ suc 𝑦 ∈ ((𝐴 ·o 𝑥) +o 1o)))
54 eloni 6327 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ On → Ord 𝐴)
55 ordgt0ge1 8439 . . . . . . . . . . . . . . . . . . . . . . . 24 (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 1o𝐴))
5654, 55syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ 1o𝐴))
5756adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∅ ∈ 𝐴 ↔ 1o𝐴))
58 1on 8424 . . . . . . . . . . . . . . . . . . . . . . . 24 1o ∈ On
59 oaword 8496 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1o ∈ On ∧ 𝐴 ∈ On ∧ (𝐴 ·o 𝑥) ∈ On) → (1o𝐴 ↔ ((𝐴 ·o 𝑥) +o 1o) ⊆ ((𝐴 ·o 𝑥) +o 𝐴)))
6058, 59mp3an1 1448 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ On ∧ (𝐴 ·o 𝑥) ∈ On) → (1o𝐴 ↔ ((𝐴 ·o 𝑥) +o 1o) ⊆ ((𝐴 ·o 𝑥) +o 𝐴)))
6145, 60syldan 591 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (1o𝐴 ↔ ((𝐴 ·o 𝑥) +o 1o) ⊆ ((𝐴 ·o 𝑥) +o 𝐴)))
6257, 61bitrd 278 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∅ ∈ 𝐴 ↔ ((𝐴 ·o 𝑥) +o 1o) ⊆ ((𝐴 ·o 𝑥) +o 𝐴)))
6362biimpa 477 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∅ ∈ 𝐴) → ((𝐴 ·o 𝑥) +o 1o) ⊆ ((𝐴 ·o 𝑥) +o 𝐴))
64 omsuc 8472 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·o suc 𝑥) = ((𝐴 ·o 𝑥) +o 𝐴))
6564adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∅ ∈ 𝐴) → (𝐴 ·o suc 𝑥) = ((𝐴 ·o 𝑥) +o 𝐴))
6663, 65sseqtrrd 3985 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∅ ∈ 𝐴) → ((𝐴 ·o 𝑥) +o 1o) ⊆ (𝐴 ·o suc 𝑥))
6766sseld 3943 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∅ ∈ 𝐴) → (suc 𝑦 ∈ ((𝐴 ·o 𝑥) +o 1o) → suc 𝑦 ∈ (𝐴 ·o suc 𝑥)))
6853, 67sylbid 239 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑦 ∈ (𝐴 ·o 𝑥) → suc 𝑦 ∈ (𝐴 ·o suc 𝑥)))
69 eleq1 2825 . . . . . . . . . . . . . . . . . 18 ((𝐴 ·o 𝐵) = suc 𝑦 → ((𝐴 ·o 𝐵) ∈ (𝐴 ·o suc 𝑥) ↔ suc 𝑦 ∈ (𝐴 ·o suc 𝑥)))
7069biimprd 247 . . . . . . . . . . . . . . . . 17 ((𝐴 ·o 𝐵) = suc 𝑦 → (suc 𝑦 ∈ (𝐴 ·o suc 𝑥) → (𝐴 ·o 𝐵) ∈ (𝐴 ·o suc 𝑥)))
7168, 70syl9 77 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∅ ∈ 𝐴) → ((𝐴 ·o 𝐵) = suc 𝑦 → (𝑦 ∈ (𝐴 ·o 𝑥) → (𝐴 ·o 𝐵) ∈ (𝐴 ·o suc 𝑥))))
7271com23 86 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑦 ∈ (𝐴 ·o 𝑥) → ((𝐴 ·o 𝐵) = suc 𝑦 → (𝐴 ·o 𝐵) ∈ (𝐴 ·o suc 𝑥))))
7372adantlrl 718 . . . . . . . . . . . . . 14 (((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑥 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝑦 ∈ (𝐴 ·o 𝑥) → ((𝐴 ·o 𝐵) = suc 𝑦 → (𝐴 ·o 𝐵) ∈ (𝐴 ·o suc 𝑥))))
74 onsucb 7752 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ On ↔ suc 𝑥 ∈ On)
75 omord 8515 . . . . . . . . . . . . . . . . . . 19 ((𝐵 ∈ On ∧ suc 𝑥 ∈ On ∧ 𝐴 ∈ On) → ((𝐵 ∈ suc 𝑥 ∧ ∅ ∈ 𝐴) ↔ (𝐴 ·o 𝐵) ∈ (𝐴 ·o suc 𝑥)))
76 simpl 483 . . . . . . . . . . . . . . . . . . 19 ((𝐵 ∈ suc 𝑥 ∧ ∅ ∈ 𝐴) → 𝐵 ∈ suc 𝑥)
7775, 76syl6bir 253 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ On ∧ suc 𝑥 ∈ On ∧ 𝐴 ∈ On) → ((𝐴 ·o 𝐵) ∈ (𝐴 ·o suc 𝑥) → 𝐵 ∈ suc 𝑥))
7874, 77syl3an2b 1404 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ On ∧ 𝑥 ∈ On ∧ 𝐴 ∈ On) → ((𝐴 ·o 𝐵) ∈ (𝐴 ·o suc 𝑥) → 𝐵 ∈ suc 𝑥))
79783comr 1125 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑥 ∈ On) → ((𝐴 ·o 𝐵) ∈ (𝐴 ·o suc 𝑥) → 𝐵 ∈ suc 𝑥))
80793expb 1120 . . . . . . . . . . . . . . 15 ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑥 ∈ On)) → ((𝐴 ·o 𝐵) ∈ (𝐴 ·o suc 𝑥) → 𝐵 ∈ suc 𝑥))
8180adantr 481 . . . . . . . . . . . . . 14 (((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑥 ∈ On)) ∧ ∅ ∈ 𝐴) → ((𝐴 ·o 𝐵) ∈ (𝐴 ·o suc 𝑥) → 𝐵 ∈ suc 𝑥))
8273, 81syl6d 75 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑥 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝑦 ∈ (𝐴 ·o 𝑥) → ((𝐴 ·o 𝐵) = suc 𝑦𝐵 ∈ suc 𝑥)))
8344, 82sylan 580 . . . . . . . . . . . 12 ((((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ 𝑥𝐵) ∧ ∅ ∈ 𝐴) → (𝑦 ∈ (𝐴 ·o 𝑥) → ((𝐴 ·o 𝐵) = suc 𝑦𝐵 ∈ suc 𝑥)))
8483an32s 650 . . . . . . . . . . 11 ((((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝑥𝐵) → (𝑦 ∈ (𝐴 ·o 𝑥) → ((𝐴 ·o 𝐵) = suc 𝑦𝐵 ∈ suc 𝑥)))
8584imp 407 . . . . . . . . . 10 (((((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝑥𝐵) ∧ 𝑦 ∈ (𝐴 ·o 𝑥)) → ((𝐴 ·o 𝐵) = suc 𝑦𝐵 ∈ suc 𝑥))
8639, 85mtod 197 . . . . . . . . 9 (((((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝑥𝐵) ∧ 𝑦 ∈ (𝐴 ·o 𝑥)) → ¬ (𝐴 ·o 𝐵) = suc 𝑦)
8786rexlimdva2 3154 . . . . . . . 8 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (∃𝑥𝐵 𝑦 ∈ (𝐴 ·o 𝑥) → ¬ (𝐴 ·o 𝐵) = suc 𝑦))
8887adantr 481 . . . . . . 7 ((((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ (𝐴 ·o 𝐵) = suc 𝑦) → (∃𝑥𝐵 𝑦 ∈ (𝐴 ·o 𝑥) → ¬ (𝐴 ·o 𝐵) = suc 𝑦))
8930, 88mpd 15 . . . . . 6 ((((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ (𝐴 ·o 𝐵) = suc 𝑦) → ¬ (𝐴 ·o 𝐵) = suc 𝑦)
9089pm2.01da 797 . . . . 5 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → ¬ (𝐴 ·o 𝐵) = suc 𝑦)
9190adantr 481 . . . 4 ((((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝑦 ∈ On) → ¬ (𝐴 ·o 𝐵) = suc 𝑦)
9291nrexdv 3146 . . 3 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → ¬ ∃𝑦 ∈ On (𝐴 ·o 𝐵) = suc 𝑦)
93 ioran 982 . . 3 (¬ ((𝐴 ·o 𝐵) = ∅ ∨ ∃𝑦 ∈ On (𝐴 ·o 𝐵) = suc 𝑦) ↔ (¬ (𝐴 ·o 𝐵) = ∅ ∧ ¬ ∃𝑦 ∈ On (𝐴 ·o 𝐵) = suc 𝑦))
9420, 92, 93sylanbrc 583 . 2 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → ¬ ((𝐴 ·o 𝐵) = ∅ ∨ ∃𝑦 ∈ On (𝐴 ·o 𝐵) = suc 𝑦))
95 dflim3 7783 . 2 (Lim (𝐴 ·o 𝐵) ↔ (Ord (𝐴 ·o 𝐵) ∧ ¬ ((𝐴 ·o 𝐵) = ∅ ∨ ∃𝑦 ∈ On (𝐴 ·o 𝐵) = suc 𝑦)))
966, 94, 95sylanbrc 583 1 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → Lim (𝐴 ·o 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wrex 3073  wss 3910  c0 4282   ciun 4954  Ord word 6316  Oncon0 6317  Lim wlim 6318  suc csuc 6319  (class class class)co 7357  1oc1o 8405   +o coa 8409   ·o comu 8410
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-oadd 8416  df-omul 8417
This theorem is referenced by:  odi  8526  omass  8527  omlimcl2  41562  omlim2  41619
  Copyright terms: Public domain W3C validator