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

Theorem omeulem1 7816
Description: Lemma for omeu 7819: existence part. (Contributed by Mario Carneiro, 28-Feb-2013.)
Assertion
Ref Expression
omeulem1 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On ∃𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦

Proof of Theorem omeulem1
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp2 1131 . . 3 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → 𝐵 ∈ On)
2 sucelon 7164 . . . . . 6 (𝐵 ∈ On ↔ suc 𝐵 ∈ On)
31, 2sylib 208 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → suc 𝐵 ∈ On)
4 simp1 1130 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → 𝐴 ∈ On)
5 on0eln0 5923 . . . . . . 7 (𝐴 ∈ On → (∅ ∈ 𝐴𝐴 ≠ ∅))
65biimpar 463 . . . . . 6 ((𝐴 ∈ On ∧ 𝐴 ≠ ∅) → ∅ ∈ 𝐴)
763adant2 1125 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∅ ∈ 𝐴)
8 omword2 7808 . . . . 5 (((suc 𝐵 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → suc 𝐵 ⊆ (𝐴 ·𝑜 suc 𝐵))
93, 4, 7, 8syl21anc 1475 . . . 4 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → suc 𝐵 ⊆ (𝐴 ·𝑜 suc 𝐵))
10 sucidg 5946 . . . . 5 (𝐵 ∈ On → 𝐵 ∈ suc 𝐵)
11 ssel 3746 . . . . 5 (suc 𝐵 ⊆ (𝐴 ·𝑜 suc 𝐵) → (𝐵 ∈ suc 𝐵𝐵 ∈ (𝐴 ·𝑜 suc 𝐵)))
1210, 11syl5 34 . . . 4 (suc 𝐵 ⊆ (𝐴 ·𝑜 suc 𝐵) → (𝐵 ∈ On → 𝐵 ∈ (𝐴 ·𝑜 suc 𝐵)))
139, 1, 12sylc 65 . . 3 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → 𝐵 ∈ (𝐴 ·𝑜 suc 𝐵))
14 suceq 5933 . . . . . 6 (𝑥 = 𝐵 → suc 𝑥 = suc 𝐵)
1514oveq2d 6809 . . . . 5 (𝑥 = 𝐵 → (𝐴 ·𝑜 suc 𝑥) = (𝐴 ·𝑜 suc 𝐵))
1615eleq2d 2836 . . . 4 (𝑥 = 𝐵 → (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ↔ 𝐵 ∈ (𝐴 ·𝑜 suc 𝐵)))
1716rspcev 3460 . . 3 ((𝐵 ∈ On ∧ 𝐵 ∈ (𝐴 ·𝑜 suc 𝐵)) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴 ·𝑜 suc 𝑥))
181, 13, 17syl2anc 573 . 2 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴 ·𝑜 suc 𝑥))
19 suceq 5933 . . . . . 6 (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧)
2019oveq2d 6809 . . . . 5 (𝑥 = 𝑧 → (𝐴 ·𝑜 suc 𝑥) = (𝐴 ·𝑜 suc 𝑧))
2120eleq2d 2836 . . . 4 (𝑥 = 𝑧 → (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ↔ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
2221onminex 7154 . . 3 (∃𝑥 ∈ On 𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) → ∃𝑥 ∈ On (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
23 vex 3354 . . . . . . . . . . . . . . 15 𝑥 ∈ V
2423elon 5875 . . . . . . . . . . . . . 14 (𝑥 ∈ On ↔ Ord 𝑥)
25 ordzsl 7192 . . . . . . . . . . . . . 14 (Ord 𝑥 ↔ (𝑥 = ∅ ∨ ∃𝑤 ∈ On 𝑥 = suc 𝑤 ∨ Lim 𝑥))
2624, 25bitri 264 . . . . . . . . . . . . 13 (𝑥 ∈ On ↔ (𝑥 = ∅ ∨ ∃𝑤 ∈ On 𝑥 = suc 𝑤 ∨ Lim 𝑥))
27 noel 4067 . . . . . . . . . . . . . . . 16 ¬ 𝐵 ∈ ∅
28 oveq2 6801 . . . . . . . . . . . . . . . . . 18 (𝑥 = ∅ → (𝐴 ·𝑜 𝑥) = (𝐴 ·𝑜 ∅))
29 om0x 7753 . . . . . . . . . . . . . . . . . 18 (𝐴 ·𝑜 ∅) = ∅
3028, 29syl6eq 2821 . . . . . . . . . . . . . . . . 17 (𝑥 = ∅ → (𝐴 ·𝑜 𝑥) = ∅)
3130eleq2d 2836 . . . . . . . . . . . . . . . 16 (𝑥 = ∅ → (𝐵 ∈ (𝐴 ·𝑜 𝑥) ↔ 𝐵 ∈ ∅))
3227, 31mtbiri 316 . . . . . . . . . . . . . . 15 (𝑥 = ∅ → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥))
3332a1i 11 . . . . . . . . . . . . . 14 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (𝑥 = ∅ → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
34 simp3 1132 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 = suc 𝑤) → 𝑥 = suc 𝑤)
35 simp2 1131 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 = suc 𝑤) → ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧))
36 raleq 3287 . . . . . . . . . . . . . . . . . . 19 (𝑥 = suc 𝑤 → (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ↔ ∀𝑧 ∈ suc 𝑤 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
37 vex 3354 . . . . . . . . . . . . . . . . . . . . 21 𝑤 ∈ V
3837sucid 5947 . . . . . . . . . . . . . . . . . . . 20 𝑤 ∈ suc 𝑤
39 suceq 5933 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑤 → suc 𝑧 = suc 𝑤)
4039oveq2d 6809 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑤 → (𝐴 ·𝑜 suc 𝑧) = (𝐴 ·𝑜 suc 𝑤))
4140eleq2d 2836 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑤 → (𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ↔ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤)))
4241notbid 307 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑤 → (¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ↔ ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤)))
4342rspcv 3456 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ suc 𝑤 → (∀𝑧 ∈ suc 𝑤 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) → ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤)))
4438, 43ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (∀𝑧 ∈ suc 𝑤 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) → ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤))
4536, 44syl6bi 243 . . . . . . . . . . . . . . . . . 18 (𝑥 = suc 𝑤 → (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) → ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤)))
4634, 35, 45sylc 65 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 = suc 𝑤) → ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤))
47 oveq2 6801 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = suc 𝑤 → (𝐴 ·𝑜 𝑥) = (𝐴 ·𝑜 suc 𝑤))
4847eleq2d 2836 . . . . . . . . . . . . . . . . . . 19 (𝑥 = suc 𝑤 → (𝐵 ∈ (𝐴 ·𝑜 𝑥) ↔ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤)))
4948notbid 307 . . . . . . . . . . . . . . . . . 18 (𝑥 = suc 𝑤 → (¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥) ↔ ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤)))
5049biimpar 463 . . . . . . . . . . . . . . . . 17 ((𝑥 = suc 𝑤 ∧ ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤)) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥))
5134, 46, 50syl2anc 573 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 = suc 𝑤) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥))
52513expia 1114 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (𝑥 = suc 𝑤 → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
5352rexlimdvw 3182 . . . . . . . . . . . . . 14 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (∃𝑤 ∈ On 𝑥 = suc 𝑤 → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
54 ralnex 3141 . . . . . . . . . . . . . . . . . 18 (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ↔ ¬ ∃𝑧𝑥 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧))
55 simpr 471 . . . . . . . . . . . . . . . . . . . . . 22 ((Lim 𝑥𝐴 ∈ On) → 𝐴 ∈ On)
5623a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((Lim 𝑥𝐴 ∈ On) → 𝑥 ∈ V)
57 simpl 468 . . . . . . . . . . . . . . . . . . . . . 22 ((Lim 𝑥𝐴 ∈ On) → Lim 𝑥)
58 omlim 7767 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝐴 ·𝑜 𝑥) = 𝑧𝑥 (𝐴 ·𝑜 𝑧))
5955, 56, 57, 58syl12anc 1474 . . . . . . . . . . . . . . . . . . . . 21 ((Lim 𝑥𝐴 ∈ On) → (𝐴 ·𝑜 𝑥) = 𝑧𝑥 (𝐴 ·𝑜 𝑧))
6059eleq2d 2836 . . . . . . . . . . . . . . . . . . . 20 ((Lim 𝑥𝐴 ∈ On) → (𝐵 ∈ (𝐴 ·𝑜 𝑥) ↔ 𝐵 𝑧𝑥 (𝐴 ·𝑜 𝑧)))
61 eliun 4658 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 𝑧𝑥 (𝐴 ·𝑜 𝑧) ↔ ∃𝑧𝑥 𝐵 ∈ (𝐴 ·𝑜 𝑧))
62 limord 5927 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Lim 𝑥 → Ord 𝑥)
63623ad2ant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Lim 𝑥𝐴 ∈ On ∧ 𝑧𝑥) → Ord 𝑥)
6463, 24sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Lim 𝑥𝐴 ∈ On ∧ 𝑧𝑥) → 𝑥 ∈ On)
65 simp3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Lim 𝑥𝐴 ∈ On ∧ 𝑧𝑥) → 𝑧𝑥)
66 onelon 5891 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ On ∧ 𝑧𝑥) → 𝑧 ∈ On)
6764, 65, 66syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Lim 𝑥𝐴 ∈ On ∧ 𝑧𝑥) → 𝑧 ∈ On)
68 suceloni 7160 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ On → suc 𝑧 ∈ On)
6967, 68syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Lim 𝑥𝐴 ∈ On ∧ 𝑧𝑥) → suc 𝑧 ∈ On)
70 simp2 1131 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Lim 𝑥𝐴 ∈ On ∧ 𝑧𝑥) → 𝐴 ∈ On)
71 sssucid 5945 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑧 ⊆ suc 𝑧
72 omwordi 7805 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧 ∈ On ∧ suc 𝑧 ∈ On ∧ 𝐴 ∈ On) → (𝑧 ⊆ suc 𝑧 → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 suc 𝑧)))
7371, 72mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑧 ∈ On ∧ suc 𝑧 ∈ On ∧ 𝐴 ∈ On) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 suc 𝑧))
7467, 69, 70, 73syl3anc 1476 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Lim 𝑥𝐴 ∈ On ∧ 𝑧𝑥) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 suc 𝑧))
7574sseld 3751 . . . . . . . . . . . . . . . . . . . . . . 23 ((Lim 𝑥𝐴 ∈ On ∧ 𝑧𝑥) → (𝐵 ∈ (𝐴 ·𝑜 𝑧) → 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
76753expia 1114 . . . . . . . . . . . . . . . . . . . . . 22 ((Lim 𝑥𝐴 ∈ On) → (𝑧𝑥 → (𝐵 ∈ (𝐴 ·𝑜 𝑧) → 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧))))
7776reximdvai 3163 . . . . . . . . . . . . . . . . . . . . 21 ((Lim 𝑥𝐴 ∈ On) → (∃𝑧𝑥 𝐵 ∈ (𝐴 ·𝑜 𝑧) → ∃𝑧𝑥 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
7861, 77syl5bi 232 . . . . . . . . . . . . . . . . . . . 20 ((Lim 𝑥𝐴 ∈ On) → (𝐵 𝑧𝑥 (𝐴 ·𝑜 𝑧) → ∃𝑧𝑥 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
7960, 78sylbid 230 . . . . . . . . . . . . . . . . . . 19 ((Lim 𝑥𝐴 ∈ On) → (𝐵 ∈ (𝐴 ·𝑜 𝑥) → ∃𝑧𝑥 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
8079con3d 149 . . . . . . . . . . . . . . . . . 18 ((Lim 𝑥𝐴 ∈ On) → (¬ ∃𝑧𝑥 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
8154, 80syl5bi 232 . . . . . . . . . . . . . . . . 17 ((Lim 𝑥𝐴 ∈ On) → (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
8281expimpd 441 . . . . . . . . . . . . . . . 16 (Lim 𝑥 → ((𝐴 ∈ On ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
8382com12 32 . . . . . . . . . . . . . . 15 ((𝐴 ∈ On ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (Lim 𝑥 → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
84833ad2antl1 1200 . . . . . . . . . . . . . 14 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (Lim 𝑥 → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
8533, 53, 843jaod 1540 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → ((𝑥 = ∅ ∨ ∃𝑤 ∈ On 𝑥 = suc 𝑤 ∨ Lim 𝑥) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
8626, 85syl5bi 232 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (𝑥 ∈ On → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
8786impr 442 . . . . . . . . . . 11 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥))
88 simpl1 1227 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → 𝐴 ∈ On)
89 simprr 756 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → 𝑥 ∈ On)
90 omcl 7770 . . . . . . . . . . . . 13 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 𝑥) ∈ On)
9188, 89, 90syl2anc 573 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → (𝐴 ·𝑜 𝑥) ∈ On)
92 simpl2 1229 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → 𝐵 ∈ On)
93 ontri1 5900 . . . . . . . . . . . 12 (((𝐴 ·𝑜 𝑥) ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜 𝑥) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
9491, 92, 93syl2anc 573 . . . . . . . . . . 11 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ((𝐴 ·𝑜 𝑥) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
9587, 94mpbird 247 . . . . . . . . . 10 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → (𝐴 ·𝑜 𝑥) ⊆ 𝐵)
96 oawordex 7791 . . . . . . . . . . 11 (((𝐴 ·𝑜 𝑥) ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜 𝑥) ⊆ 𝐵 ↔ ∃𝑦 ∈ On ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
9791, 92, 96syl2anc 573 . . . . . . . . . 10 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ((𝐴 ·𝑜 𝑥) ⊆ 𝐵 ↔ ∃𝑦 ∈ On ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
9895, 97mpbid 222 . . . . . . . . 9 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ∃𝑦 ∈ On ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)
99983adantr1 1174 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ∃𝑦 ∈ On ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)
100 simp3r 1244 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)
101 simp21 1248 . . . . . . . . . . . . . 14 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → 𝐵 ∈ (𝐴 ·𝑜 suc 𝑥))
102 simp11 1245 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → 𝐴 ∈ On)
103 simp23 1250 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → 𝑥 ∈ On)
104 omsuc 7760 . . . . . . . . . . . . . . 15 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 suc 𝑥) = ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))
105102, 103, 104syl2anc 573 . . . . . . . . . . . . . 14 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → (𝐴 ·𝑜 suc 𝑥) = ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))
106101, 105eleqtrd 2852 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → 𝐵 ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))
107100, 106eqeltrd 2850 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))
108 simp3l 1243 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → 𝑦 ∈ On)
109102, 103, 90syl2anc 573 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → (𝐴 ·𝑜 𝑥) ∈ On)
110 oaord 7781 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴 ·𝑜 𝑥) ∈ On) → (𝑦𝐴 ↔ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴)))
111108, 102, 109, 110syl3anc 1476 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → (𝑦𝐴 ↔ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴)))
112107, 111mpbird 247 . . . . . . . . . . 11 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → 𝑦𝐴)
113112, 100jca 501 . . . . . . . . . 10 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → (𝑦𝐴 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
1141133expia 1114 . . . . . . . . 9 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ((𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵) → (𝑦𝐴 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)))
115114reximdv2 3162 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → (∃𝑦 ∈ On ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵 → ∃𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
11699, 115mpd 15 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ∃𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)
117116expcom 398 . . . . . 6 ((𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) → ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
1181173expia 1114 . . . . 5 ((𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (𝑥 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)))
119118com13 88 . . . 4 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → (𝑥 ∈ On → ((𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → ∃𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)))
120119reximdvai 3163 . . 3 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → (∃𝑥 ∈ On (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → ∃𝑥 ∈ On ∃𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
12122, 120syl5 34 . 2 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → (∃𝑥 ∈ On 𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) → ∃𝑥 ∈ On ∃𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
12218, 121mpd 15 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On ∃𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  w3o 1070  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  Vcvv 3351  wss 3723  c0 4063   ciun 4654  Ord word 5865  Oncon0 5866  Lim wlim 5867  suc csuc 5868  (class class class)co 6793   +𝑜 coa 7710   ·𝑜 comu 7711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-omul 7718
This theorem is referenced by:  omeu  7819
  Copyright terms: Public domain W3C validator