| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp2 1138 | . . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → 𝐵 ∈ On) | 
| 2 |  | onsucb 7837 | . . . . . 6
⊢ (𝐵 ∈ On ↔ suc 𝐵 ∈ On) | 
| 3 | 1, 2 | sylib 218 | . . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → suc 𝐵 ∈ On) | 
| 4 |  | simp1 1137 | . . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → 𝐴 ∈ On) | 
| 5 |  | on0eln0 6440 | . . . . . . 7
⊢ (𝐴 ∈ On → (∅
∈ 𝐴 ↔ 𝐴 ≠ ∅)) | 
| 6 | 5 | biimpar 477 | . . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐴 ≠ ∅) → ∅
∈ 𝐴) | 
| 7 | 6 | 3adant2 1132 | . . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∅
∈ 𝐴) | 
| 8 |  | omword2 8612 | . . . . 5
⊢ (((suc
𝐵 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐴) → suc 𝐵 ⊆ (𝐴 ·o suc 𝐵)) | 
| 9 | 3, 4, 7, 8 | syl21anc 838 | . . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → suc 𝐵 ⊆ (𝐴 ·o suc 𝐵)) | 
| 10 |  | sucidg 6465 | . . . . 5
⊢ (𝐵 ∈ On → 𝐵 ∈ suc 𝐵) | 
| 11 |  | ssel 3977 | . . . . 5
⊢ (suc
𝐵 ⊆ (𝐴 ·o suc 𝐵) → (𝐵 ∈ suc 𝐵 → 𝐵 ∈ (𝐴 ·o suc 𝐵))) | 
| 12 | 10, 11 | syl5 34 | . . . 4
⊢ (suc
𝐵 ⊆ (𝐴 ·o suc 𝐵) → (𝐵 ∈ On → 𝐵 ∈ (𝐴 ·o suc 𝐵))) | 
| 13 | 9, 1, 12 | sylc 65 | . . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → 𝐵 ∈ (𝐴 ·o suc 𝐵)) | 
| 14 |  | suceq 6450 | . . . . . 6
⊢ (𝑥 = 𝐵 → suc 𝑥 = suc 𝐵) | 
| 15 | 14 | oveq2d 7447 | . . . . 5
⊢ (𝑥 = 𝐵 → (𝐴 ·o suc 𝑥) = (𝐴 ·o suc 𝐵)) | 
| 16 | 15 | eleq2d 2827 | . . . 4
⊢ (𝑥 = 𝐵 → (𝐵 ∈ (𝐴 ·o suc 𝑥) ↔ 𝐵 ∈ (𝐴 ·o suc 𝐵))) | 
| 17 | 16 | rspcev 3622 | . . 3
⊢ ((𝐵 ∈ On ∧ 𝐵 ∈ (𝐴 ·o suc 𝐵)) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴 ·o suc 𝑥)) | 
| 18 | 1, 13, 17 | syl2anc 584 | . 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) →
∃𝑥 ∈ On 𝐵 ∈ (𝐴 ·o suc 𝑥)) | 
| 19 |  | suceq 6450 | . . . . . 6
⊢ (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧) | 
| 20 | 19 | oveq2d 7447 | . . . . 5
⊢ (𝑥 = 𝑧 → (𝐴 ·o suc 𝑥) = (𝐴 ·o suc 𝑧)) | 
| 21 | 20 | eleq2d 2827 | . . . 4
⊢ (𝑥 = 𝑧 → (𝐵 ∈ (𝐴 ·o suc 𝑥) ↔ 𝐵 ∈ (𝐴 ·o suc 𝑧))) | 
| 22 | 21 | onminex 7822 | . . 3
⊢
(∃𝑥 ∈ On
𝐵 ∈ (𝐴 ·o suc 𝑥) → ∃𝑥 ∈ On (𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧))) | 
| 23 |  | vex 3484 | . . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V | 
| 24 | 23 | elon 6393 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ On ↔ Ord 𝑥) | 
| 25 |  | ordzsl 7866 | . . . . . . . . . . . . . 14
⊢ (Ord
𝑥 ↔ (𝑥 = ∅ ∨ ∃𝑤 ∈ On 𝑥 = suc 𝑤 ∨ Lim 𝑥)) | 
| 26 | 24, 25 | bitri 275 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ On ↔ (𝑥 = ∅ ∨ ∃𝑤 ∈ On 𝑥 = suc 𝑤 ∨ Lim 𝑥)) | 
| 27 |  | oveq2 7439 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = ∅ → (𝐴 ·o 𝑥) = (𝐴 ·o
∅)) | 
| 28 |  | om0 8555 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ On → (𝐴 ·o ∅) =
∅) | 
| 29 | 27, 28 | sylan9eqr 2799 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ On ∧ 𝑥 = ∅) → (𝐴 ·o 𝑥) = ∅) | 
| 30 |  | ne0i 4341 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 ∈ (𝐴 ·o 𝑥) → (𝐴 ·o 𝑥) ≠ ∅) | 
| 31 | 30 | necon2bi 2971 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ·o 𝑥) = ∅ → ¬ 𝐵 ∈ (𝐴 ·o 𝑥)) | 
| 32 | 29, 31 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ On ∧ 𝑥 = ∅) → ¬ 𝐵 ∈ (𝐴 ·o 𝑥)) | 
| 33 | 32 | ex 412 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ On → (𝑥 = ∅ → ¬ 𝐵 ∈ (𝐴 ·o 𝑥))) | 
| 34 | 33 | a1d 25 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ On → (∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) → (𝑥 = ∅ → ¬ 𝐵 ∈ (𝐴 ·o 𝑥)))) | 
| 35 | 34 | 3ad2ant1 1134 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) →
(∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) → (𝑥 = ∅ → ¬ 𝐵 ∈ (𝐴 ·o 𝑥)))) | 
| 36 | 35 | imp 406 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧
∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧)) → (𝑥 = ∅ → ¬ 𝐵 ∈ (𝐴 ·o 𝑥))) | 
| 37 |  | simp3 1139 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧
∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 = suc 𝑤) → 𝑥 = suc 𝑤) | 
| 38 |  | simp2 1138 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧
∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 = suc 𝑤) → ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧)) | 
| 39 |  | raleq 3323 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = suc 𝑤 → (∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ↔ ∀𝑧 ∈ suc 𝑤 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧))) | 
| 40 |  | vex 3484 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑤 ∈ V | 
| 41 | 40 | sucid 6466 | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝑤 ∈ suc 𝑤 | 
| 42 |  | suceq 6450 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = 𝑤 → suc 𝑧 = suc 𝑤) | 
| 43 | 42 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = 𝑤 → (𝐴 ·o suc 𝑧) = (𝐴 ·o suc 𝑤)) | 
| 44 | 43 | eleq2d 2827 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = 𝑤 → (𝐵 ∈ (𝐴 ·o suc 𝑧) ↔ 𝐵 ∈ (𝐴 ·o suc 𝑤))) | 
| 45 | 44 | notbid 318 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑤 → (¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ↔ ¬ 𝐵 ∈ (𝐴 ·o suc 𝑤))) | 
| 46 | 45 | rspcv 3618 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ suc 𝑤 → (∀𝑧 ∈ suc 𝑤 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) → ¬ 𝐵 ∈ (𝐴 ·o suc 𝑤))) | 
| 47 | 41, 46 | ax-mp 5 | . . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑧 ∈
suc 𝑤 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) → ¬ 𝐵 ∈ (𝐴 ·o suc 𝑤)) | 
| 48 | 39, 47 | biimtrdi 253 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = suc 𝑤 → (∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) → ¬ 𝐵 ∈ (𝐴 ·o suc 𝑤))) | 
| 49 | 37, 38, 48 | sylc 65 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧
∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 = suc 𝑤) → ¬ 𝐵 ∈ (𝐴 ·o suc 𝑤)) | 
| 50 |  | oveq2 7439 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = suc 𝑤 → (𝐴 ·o 𝑥) = (𝐴 ·o suc 𝑤)) | 
| 51 | 50 | eleq2d 2827 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = suc 𝑤 → (𝐵 ∈ (𝐴 ·o 𝑥) ↔ 𝐵 ∈ (𝐴 ·o suc 𝑤))) | 
| 52 | 51 | notbid 318 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = suc 𝑤 → (¬ 𝐵 ∈ (𝐴 ·o 𝑥) ↔ ¬ 𝐵 ∈ (𝐴 ·o suc 𝑤))) | 
| 53 | 52 | biimpar 477 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = suc 𝑤 ∧ ¬ 𝐵 ∈ (𝐴 ·o suc 𝑤)) → ¬ 𝐵 ∈ (𝐴 ·o 𝑥)) | 
| 54 | 37, 49, 53 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧
∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 = suc 𝑤) → ¬ 𝐵 ∈ (𝐴 ·o 𝑥)) | 
| 55 | 54 | 3expia 1122 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧
∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧)) → (𝑥 = suc 𝑤 → ¬ 𝐵 ∈ (𝐴 ·o 𝑥))) | 
| 56 | 55 | rexlimdvw 3160 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧
∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧)) → (∃𝑤 ∈ On 𝑥 = suc 𝑤 → ¬ 𝐵 ∈ (𝐴 ·o 𝑥))) | 
| 57 |  | ralnex 3072 | . . . . . . . . . . . . . . . . . 18
⊢
(∀𝑧 ∈
𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ↔ ¬ ∃𝑧 ∈ 𝑥 𝐵 ∈ (𝐴 ·o suc 𝑧)) | 
| 58 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → 𝐴 ∈ On) | 
| 59 | 23 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → 𝑥 ∈ V) | 
| 60 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → Lim 𝑥) | 
| 61 |  | omlim 8571 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝐴 ·o 𝑥) = ∪ 𝑧 ∈ 𝑥 (𝐴 ·o 𝑧)) | 
| 62 | 58, 59, 60, 61 | syl12anc 837 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → (𝐴 ·o 𝑥) = ∪ 𝑧 ∈ 𝑥 (𝐴 ·o 𝑧)) | 
| 63 | 62 | eleq2d 2827 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → (𝐵 ∈ (𝐴 ·o 𝑥) ↔ 𝐵 ∈ ∪
𝑧 ∈ 𝑥 (𝐴 ·o 𝑧))) | 
| 64 |  | eliun 4995 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 ∈ ∪ 𝑧 ∈ 𝑥 (𝐴 ·o 𝑧) ↔ ∃𝑧 ∈ 𝑥 𝐵 ∈ (𝐴 ·o 𝑧)) | 
| 65 |  | limord 6444 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (Lim
𝑥 → Ord 𝑥) | 
| 66 | 65 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On ∧ 𝑧 ∈ 𝑥) → Ord 𝑥) | 
| 67 | 66, 24 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On ∧ 𝑧 ∈ 𝑥) → 𝑥 ∈ On) | 
| 68 |  | simp3 1139 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ 𝑥) | 
| 69 |  | onelon 6409 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ On ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ On) | 
| 70 | 67, 68, 69 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ On) | 
| 71 |  | onsuc 7831 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ On → suc 𝑧 ∈ On) | 
| 72 | 70, 71 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On ∧ 𝑧 ∈ 𝑥) → suc 𝑧 ∈ On) | 
| 73 |  | simp2 1138 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On ∧ 𝑧 ∈ 𝑥) → 𝐴 ∈ On) | 
| 74 |  | sssucid 6464 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑧 ⊆ suc 𝑧 | 
| 75 |  | omwordi 8609 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑧 ∈ On ∧ suc 𝑧 ∈ On ∧ 𝐴 ∈ On) → (𝑧 ⊆ suc 𝑧 → (𝐴 ·o 𝑧) ⊆ (𝐴 ·o suc 𝑧))) | 
| 76 | 74, 75 | mpi 20 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ On ∧ suc 𝑧 ∈ On ∧ 𝐴 ∈ On) → (𝐴 ·o 𝑧) ⊆ (𝐴 ·o suc 𝑧)) | 
| 77 | 70, 72, 73, 76 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On ∧ 𝑧 ∈ 𝑥) → (𝐴 ·o 𝑧) ⊆ (𝐴 ·o suc 𝑧)) | 
| 78 | 77 | sseld 3982 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On ∧ 𝑧 ∈ 𝑥) → (𝐵 ∈ (𝐴 ·o 𝑧) → 𝐵 ∈ (𝐴 ·o suc 𝑧))) | 
| 79 | 78 | 3expia 1122 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → (𝑧 ∈ 𝑥 → (𝐵 ∈ (𝐴 ·o 𝑧) → 𝐵 ∈ (𝐴 ·o suc 𝑧)))) | 
| 80 | 79 | reximdvai 3165 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → (∃𝑧 ∈ 𝑥 𝐵 ∈ (𝐴 ·o 𝑧) → ∃𝑧 ∈ 𝑥 𝐵 ∈ (𝐴 ·o suc 𝑧))) | 
| 81 | 64, 80 | biimtrid 242 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → (𝐵 ∈ ∪
𝑧 ∈ 𝑥 (𝐴 ·o 𝑧) → ∃𝑧 ∈ 𝑥 𝐵 ∈ (𝐴 ·o suc 𝑧))) | 
| 82 | 63, 81 | sylbid 240 | . . . . . . . . . . . . . . . . . . 19
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → (𝐵 ∈ (𝐴 ·o 𝑥) → ∃𝑧 ∈ 𝑥 𝐵 ∈ (𝐴 ·o suc 𝑧))) | 
| 83 | 82 | con3d 152 | . . . . . . . . . . . . . . . . . 18
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → (¬ ∃𝑧 ∈ 𝑥 𝐵 ∈ (𝐴 ·o suc 𝑧) → ¬ 𝐵 ∈ (𝐴 ·o 𝑥))) | 
| 84 | 57, 83 | biimtrid 242 | . . . . . . . . . . . . . . . . 17
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → (∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) → ¬ 𝐵 ∈ (𝐴 ·o 𝑥))) | 
| 85 | 84 | expimpd 453 | . . . . . . . . . . . . . . . 16
⊢ (Lim
𝑥 → ((𝐴 ∈ On ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧)) → ¬ 𝐵 ∈ (𝐴 ·o 𝑥))) | 
| 86 | 85 | com12 32 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ On ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧)) → (Lim 𝑥 → ¬ 𝐵 ∈ (𝐴 ·o 𝑥))) | 
| 87 | 86 | 3ad2antl1 1186 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧
∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧)) → (Lim 𝑥 → ¬ 𝐵 ∈ (𝐴 ·o 𝑥))) | 
| 88 | 36, 56, 87 | 3jaod 1431 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧
∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧)) → ((𝑥 = ∅ ∨ ∃𝑤 ∈ On 𝑥 = suc 𝑤 ∨ Lim 𝑥) → ¬ 𝐵 ∈ (𝐴 ·o 𝑥))) | 
| 89 | 26, 88 | biimtrid 242 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧
∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧)) → (𝑥 ∈ On → ¬ 𝐵 ∈ (𝐴 ·o 𝑥))) | 
| 90 | 89 | impr 454 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧
(∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On)) → ¬ 𝐵 ∈ (𝐴 ·o 𝑥)) | 
| 91 |  | simpl1 1192 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧
(∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On)) → 𝐴 ∈ On) | 
| 92 |  | simprr 773 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧
(∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On)) → 𝑥 ∈ On) | 
| 93 |  | omcl 8574 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·o 𝑥) ∈ On) | 
| 94 | 91, 92, 93 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧
(∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On)) → (𝐴 ·o 𝑥) ∈ On) | 
| 95 |  | simpl2 1193 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧
(∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On)) → 𝐵 ∈ On) | 
| 96 |  | ontri1 6418 | . . . . . . . . . . . 12
⊢ (((𝐴 ·o 𝑥) ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o 𝑥) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴 ·o 𝑥))) | 
| 97 | 94, 95, 96 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧
(∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On)) → ((𝐴 ·o 𝑥) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴 ·o 𝑥))) | 
| 98 | 90, 97 | mpbird 257 | . . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧
(∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On)) → (𝐴 ·o 𝑥) ⊆ 𝐵) | 
| 99 |  | oawordex 8595 | . . . . . . . . . . 11
⊢ (((𝐴 ·o 𝑥) ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o 𝑥) ⊆ 𝐵 ↔ ∃𝑦 ∈ On ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵)) | 
| 100 | 94, 95, 99 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧
(∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On)) → ((𝐴 ·o 𝑥) ⊆ 𝐵 ↔ ∃𝑦 ∈ On ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵)) | 
| 101 | 98, 100 | mpbid 232 | . . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧
(∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On)) → ∃𝑦 ∈ On ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵) | 
| 102 | 101 | 3adantr1 1170 | . . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On)) → ∃𝑦 ∈ On ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵) | 
| 103 |  | simp3r 1203 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵)) → ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵) | 
| 104 |  | simp21 1207 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵)) → 𝐵 ∈ (𝐴 ·o suc 𝑥)) | 
| 105 |  | simp11 1204 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵)) → 𝐴 ∈ On) | 
| 106 |  | simp23 1209 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵)) → 𝑥 ∈ On) | 
| 107 |  | omsuc 8564 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·o suc 𝑥) = ((𝐴 ·o 𝑥) +o 𝐴)) | 
| 108 | 105, 106,
107 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵)) → (𝐴 ·o suc 𝑥) = ((𝐴 ·o 𝑥) +o 𝐴)) | 
| 109 | 104, 108 | eleqtrd 2843 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵)) → 𝐵 ∈ ((𝐴 ·o 𝑥) +o 𝐴)) | 
| 110 | 103, 109 | eqeltrd 2841 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵)) → ((𝐴 ·o 𝑥) +o 𝑦) ∈ ((𝐴 ·o 𝑥) +o 𝐴)) | 
| 111 |  | simp3l 1202 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵)) → 𝑦 ∈ On) | 
| 112 | 105, 106,
93 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵)) → (𝐴 ·o 𝑥) ∈ On) | 
| 113 |  | oaord 8585 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴 ·o 𝑥) ∈ On) → (𝑦 ∈ 𝐴 ↔ ((𝐴 ·o 𝑥) +o 𝑦) ∈ ((𝐴 ·o 𝑥) +o 𝐴))) | 
| 114 | 111, 105,
112, 113 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵)) → (𝑦 ∈ 𝐴 ↔ ((𝐴 ·o 𝑥) +o 𝑦) ∈ ((𝐴 ·o 𝑥) +o 𝐴))) | 
| 115 | 110, 114 | mpbird 257 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵)) → 𝑦 ∈ 𝐴) | 
| 116 | 115, 103 | jca 511 | . . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵)) → (𝑦 ∈ 𝐴 ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵)) | 
| 117 | 116 | 3expia 1122 | . . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On)) → ((𝑦 ∈ On ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵) → (𝑦 ∈ 𝐴 ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵))) | 
| 118 | 117 | reximdv2 3164 | . . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On)) → (∃𝑦 ∈ On ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵 → ∃𝑦 ∈ 𝐴 ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵)) | 
| 119 | 102, 118 | mpd 15 | . . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On)) → ∃𝑦 ∈ 𝐴 ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵) | 
| 120 | 119 | expcom 413 | . . . . . 6
⊢ ((𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧) ∧ 𝑥 ∈ On) → ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃𝑦 ∈ 𝐴 ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵)) | 
| 121 | 120 | 3expia 1122 | . . . . 5
⊢ ((𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧)) → (𝑥 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃𝑦 ∈ 𝐴 ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵))) | 
| 122 | 121 | com13 88 | . . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → (𝑥 ∈ On → ((𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧)) → ∃𝑦 ∈ 𝐴 ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵))) | 
| 123 | 122 | reximdvai 3165 | . . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) →
(∃𝑥 ∈ On (𝐵 ∈ (𝐴 ·o suc 𝑥) ∧ ∀𝑧 ∈ 𝑥 ¬ 𝐵 ∈ (𝐴 ·o suc 𝑧)) → ∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵)) | 
| 124 | 22, 123 | syl5 34 | . 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) →
(∃𝑥 ∈ On 𝐵 ∈ (𝐴 ·o suc 𝑥) → ∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵)) | 
| 125 | 18, 124 | mpd 15 | 1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) →
∃𝑥 ∈ On
∃𝑦 ∈ 𝐴 ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵) |