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

Theorem omeulem1 7707
Description: Lemma for omeu 7710: 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 1082 . . 3 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → 𝐵 ∈ On)
2 sucelon 7059 . . . . . 6 (𝐵 ∈ On ↔ suc 𝐵 ∈ On)
31, 2sylib 208 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → suc 𝐵 ∈ On)
4 simp1 1081 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → 𝐴 ∈ On)
5 on0eln0 5818 . . . . . . 7 (𝐴 ∈ On → (∅ ∈ 𝐴𝐴 ≠ ∅))
65biimpar 501 . . . . . 6 ((𝐴 ∈ On ∧ 𝐴 ≠ ∅) → ∅ ∈ 𝐴)
763adant2 1100 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∅ ∈ 𝐴)
8 omword2 7699 . . . . 5 (((suc 𝐵 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → suc 𝐵 ⊆ (𝐴 ·𝑜 suc 𝐵))
93, 4, 7, 8syl21anc 1365 . . . 4 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → suc 𝐵 ⊆ (𝐴 ·𝑜 suc 𝐵))
10 sucidg 5841 . . . . 5 (𝐵 ∈ On → 𝐵 ∈ suc 𝐵)
11 ssel 3630 . . . . 5 (suc 𝐵 ⊆ (𝐴 ·𝑜 suc 𝐵) → (𝐵 ∈ suc 𝐵𝐵 ∈ (𝐴 ·𝑜 suc 𝐵)))
1210, 11syl5 34 . . . 4 (suc 𝐵 ⊆ (𝐴 ·𝑜 suc 𝐵) → (𝐵 ∈ On → 𝐵 ∈ (𝐴 ·𝑜 suc 𝐵)))
139, 1, 12sylc 65 . . 3 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → 𝐵 ∈ (𝐴 ·𝑜 suc 𝐵))
14 suceq 5828 . . . . . 6 (𝑥 = 𝐵 → suc 𝑥 = suc 𝐵)
1514oveq2d 6706 . . . . 5 (𝑥 = 𝐵 → (𝐴 ·𝑜 suc 𝑥) = (𝐴 ·𝑜 suc 𝐵))
1615eleq2d 2716 . . . 4 (𝑥 = 𝐵 → (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ↔ 𝐵 ∈ (𝐴 ·𝑜 suc 𝐵)))
1716rspcev 3340 . . 3 ((𝐵 ∈ On ∧ 𝐵 ∈ (𝐴 ·𝑜 suc 𝐵)) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴 ·𝑜 suc 𝑥))
181, 13, 17syl2anc 694 . 2 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴 ·𝑜 suc 𝑥))
19 suceq 5828 . . . . . 6 (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧)
2019oveq2d 6706 . . . . 5 (𝑥 = 𝑧 → (𝐴 ·𝑜 suc 𝑥) = (𝐴 ·𝑜 suc 𝑧))
2120eleq2d 2716 . . . 4 (𝑥 = 𝑧 → (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ↔ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
2221onminex 7049 . . 3 (∃𝑥 ∈ On 𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) → ∃𝑥 ∈ On (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
23 vex 3234 . . . . . . . . . . . . . . 15 𝑥 ∈ V
2423elon 5770 . . . . . . . . . . . . . 14 (𝑥 ∈ On ↔ Ord 𝑥)
25 ordzsl 7087 . . . . . . . . . . . . . 14 (Ord 𝑥 ↔ (𝑥 = ∅ ∨ ∃𝑤 ∈ On 𝑥 = suc 𝑤 ∨ Lim 𝑥))
2624, 25bitri 264 . . . . . . . . . . . . 13 (𝑥 ∈ On ↔ (𝑥 = ∅ ∨ ∃𝑤 ∈ On 𝑥 = suc 𝑤 ∨ Lim 𝑥))
27 noel 3952 . . . . . . . . . . . . . . . 16 ¬ 𝐵 ∈ ∅
28 oveq2 6698 . . . . . . . . . . . . . . . . . 18 (𝑥 = ∅ → (𝐴 ·𝑜 𝑥) = (𝐴 ·𝑜 ∅))
29 om0x 7644 . . . . . . . . . . . . . . . . . 18 (𝐴 ·𝑜 ∅) = ∅
3028, 29syl6eq 2701 . . . . . . . . . . . . . . . . 17 (𝑥 = ∅ → (𝐴 ·𝑜 𝑥) = ∅)
3130eleq2d 2716 . . . . . . . . . . . . . . . 16 (𝑥 = ∅ → (𝐵 ∈ (𝐴 ·𝑜 𝑥) ↔ 𝐵 ∈ ∅))
3227, 31mtbiri 316 . . . . . . . . . . . . . . 15 (𝑥 = ∅ → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥))
3332a1i 11 . . . . . . . . . . . . . 14 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (𝑥 = ∅ → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
34 simp3 1083 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 = suc 𝑤) → 𝑥 = suc 𝑤)
35 simp2 1082 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 = suc 𝑤) → ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧))
36 raleq 3168 . . . . . . . . . . . . . . . . . . 19 (𝑥 = suc 𝑤 → (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ↔ ∀𝑧 ∈ suc 𝑤 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
37 vex 3234 . . . . . . . . . . . . . . . . . . . . 21 𝑤 ∈ V
3837sucid 5842 . . . . . . . . . . . . . . . . . . . 20 𝑤 ∈ suc 𝑤
39 suceq 5828 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑤 → suc 𝑧 = suc 𝑤)
4039oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑤 → (𝐴 ·𝑜 suc 𝑧) = (𝐴 ·𝑜 suc 𝑤))
4140eleq2d 2716 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑤 → (𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ↔ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤)))
4241notbid 307 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑤 → (¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ↔ ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤)))
4342rspcv 3336 . . . . . . . . . . . . . . . . . . . 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 6698 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = suc 𝑤 → (𝐴 ·𝑜 𝑥) = (𝐴 ·𝑜 suc 𝑤))
4847eleq2d 2716 . . . . . . . . . . . . . . . . . . 19 (𝑥 = suc 𝑤 → (𝐵 ∈ (𝐴 ·𝑜 𝑥) ↔ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤)))
4948notbid 307 . . . . . . . . . . . . . . . . . 18 (𝑥 = suc 𝑤 → (¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥) ↔ ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤)))
5049biimpar 501 . . . . . . . . . . . . . . . . 17 ((𝑥 = suc 𝑤 ∧ ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑤)) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥))
5134, 46, 50syl2anc 694 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 = suc 𝑤) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥))
52513expia 1286 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (𝑥 = suc 𝑤 → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
5352rexlimdvw 3063 . . . . . . . . . . . . . 14 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (∃𝑤 ∈ On 𝑥 = suc 𝑤 → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
54 ralnex 3021 . . . . . . . . . . . . . . . . . 18 (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ↔ ¬ ∃𝑧𝑥 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧))
55 simpr 476 . . . . . . . . . . . . . . . . . . . . . 22 ((Lim 𝑥𝐴 ∈ On) → 𝐴 ∈ On)
5623a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((Lim 𝑥𝐴 ∈ On) → 𝑥 ∈ V)
57 simpl 472 . . . . . . . . . . . . . . . . . . . . . 22 ((Lim 𝑥𝐴 ∈ On) → Lim 𝑥)
58 omlim 7658 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝐴 ·𝑜 𝑥) = 𝑧𝑥 (𝐴 ·𝑜 𝑧))
5955, 56, 57, 58syl12anc 1364 . . . . . . . . . . . . . . . . . . . . 21 ((Lim 𝑥𝐴 ∈ On) → (𝐴 ·𝑜 𝑥) = 𝑧𝑥 (𝐴 ·𝑜 𝑧))
6059eleq2d 2716 . . . . . . . . . . . . . . . . . . . 20 ((Lim 𝑥𝐴 ∈ On) → (𝐵 ∈ (𝐴 ·𝑜 𝑥) ↔ 𝐵 𝑧𝑥 (𝐴 ·𝑜 𝑧)))
61 eliun 4556 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 𝑧𝑥 (𝐴 ·𝑜 𝑧) ↔ ∃𝑧𝑥 𝐵 ∈ (𝐴 ·𝑜 𝑧))
62 limord 5822 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Lim 𝑥 → Ord 𝑥)
63623ad2ant1 1102 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Lim 𝑥𝐴 ∈ On ∧ 𝑧𝑥) → Ord 𝑥)
6463, 24sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Lim 𝑥𝐴 ∈ On ∧ 𝑧𝑥) → 𝑥 ∈ On)
65 simp3 1083 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Lim 𝑥𝐴 ∈ On ∧ 𝑧𝑥) → 𝑧𝑥)
66 onelon 5786 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ On ∧ 𝑧𝑥) → 𝑧 ∈ On)
6764, 65, 66syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Lim 𝑥𝐴 ∈ On ∧ 𝑧𝑥) → 𝑧 ∈ On)
68 suceloni 7055 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ On → suc 𝑧 ∈ On)
6967, 68syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Lim 𝑥𝐴 ∈ On ∧ 𝑧𝑥) → suc 𝑧 ∈ On)
70 simp2 1082 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Lim 𝑥𝐴 ∈ On ∧ 𝑧𝑥) → 𝐴 ∈ On)
71 sssucid 5840 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑧 ⊆ suc 𝑧
72 omwordi 7696 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧 ∈ On ∧ suc 𝑧 ∈ On ∧ 𝐴 ∈ On) → (𝑧 ⊆ suc 𝑧 → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 suc 𝑧)))
7371, 72mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑧 ∈ On ∧ suc 𝑧 ∈ On ∧ 𝐴 ∈ On) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 suc 𝑧))
7467, 69, 70, 73syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Lim 𝑥𝐴 ∈ On ∧ 𝑧𝑥) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 suc 𝑧))
7574sseld 3635 . . . . . . . . . . . . . . . . . . . . . . 23 ((Lim 𝑥𝐴 ∈ On ∧ 𝑧𝑥) → (𝐵 ∈ (𝐴 ·𝑜 𝑧) → 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
76753expia 1286 . . . . . . . . . . . . . . . . . . . . . 22 ((Lim 𝑥𝐴 ∈ On) → (𝑧𝑥 → (𝐵 ∈ (𝐴 ·𝑜 𝑧) → 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧))))
7776reximdvai 3044 . . . . . . . . . . . . . . . . . . . . 21 ((Lim 𝑥𝐴 ∈ On) → (∃𝑧𝑥 𝐵 ∈ (𝐴 ·𝑜 𝑧) → ∃𝑧𝑥 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
7861, 77syl5bi 232 . . . . . . . . . . . . . . . . . . . 20 ((Lim 𝑥𝐴 ∈ On) → (𝐵 𝑧𝑥 (𝐴 ·𝑜 𝑧) → ∃𝑧𝑥 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
7960, 78sylbid 230 . . . . . . . . . . . . . . . . . . 19 ((Lim 𝑥𝐴 ∈ On) → (𝐵 ∈ (𝐴 ·𝑜 𝑥) → ∃𝑧𝑥 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)))
8079con3d 148 . . . . . . . . . . . . . . . . . 18 ((Lim 𝑥𝐴 ∈ On) → (¬ ∃𝑧𝑥 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
8154, 80syl5bi 232 . . . . . . . . . . . . . . . . 17 ((Lim 𝑥𝐴 ∈ On) → (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
8281expimpd 628 . . . . . . . . . . . . . . . 16 (Lim 𝑥 → ((𝐴 ∈ On ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
8382com12 32 . . . . . . . . . . . . . . 15 ((𝐴 ∈ On ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (Lim 𝑥 → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
84833ad2antl1 1243 . . . . . . . . . . . . . 14 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (Lim 𝑥 → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
8533, 53, 843jaod 1432 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → ((𝑥 = ∅ ∨ ∃𝑤 ∈ On 𝑥 = suc 𝑤 ∨ Lim 𝑥) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
8626, 85syl5bi 232 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (𝑥 ∈ On → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
8786impr 648 . . . . . . . . . . 11 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥))
88 simpl1 1084 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → 𝐴 ∈ On)
89 simprr 811 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → 𝑥 ∈ On)
90 omcl 7661 . . . . . . . . . . . . 13 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 𝑥) ∈ On)
9188, 89, 90syl2anc 694 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → (𝐴 ·𝑜 𝑥) ∈ On)
92 simpl2 1085 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → 𝐵 ∈ On)
93 ontri1 5795 . . . . . . . . . . . 12 (((𝐴 ·𝑜 𝑥) ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜 𝑥) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
9491, 92, 93syl2anc 694 . . . . . . . . . . 11 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ((𝐴 ·𝑜 𝑥) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴 ·𝑜 𝑥)))
9587, 94mpbird 247 . . . . . . . . . 10 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → (𝐴 ·𝑜 𝑥) ⊆ 𝐵)
96 oawordex 7682 . . . . . . . . . . 11 (((𝐴 ·𝑜 𝑥) ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜 𝑥) ⊆ 𝐵 ↔ ∃𝑦 ∈ On ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
9791, 92, 96syl2anc 694 . . . . . . . . . 10 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ((𝐴 ·𝑜 𝑥) ⊆ 𝐵 ↔ ∃𝑦 ∈ On ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
9895, 97mpbid 222 . . . . . . . . 9 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ∃𝑦 ∈ On ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)
99983adantr1 1240 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ∃𝑦 ∈ On ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)
100 simp3r 1110 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)
101 simp21 1114 . . . . . . . . . . . . . 14 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → 𝐵 ∈ (𝐴 ·𝑜 suc 𝑥))
102 simp11 1111 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → 𝐴 ∈ On)
103 simp23 1116 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → 𝑥 ∈ On)
104 omsuc 7651 . . . . . . . . . . . . . . 15 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 suc 𝑥) = ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))
105102, 103, 104syl2anc 694 . . . . . . . . . . . . . 14 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → (𝐴 ·𝑜 suc 𝑥) = ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))
106101, 105eleqtrd 2732 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → 𝐵 ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))
107100, 106eqeltrd 2730 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))
108 simp3l 1109 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → 𝑦 ∈ On)
109102, 103, 90syl2anc 694 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → (𝐴 ·𝑜 𝑥) ∈ On)
110 oaord 7672 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴 ·𝑜 𝑥) ∈ On) → (𝑦𝐴 ↔ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴)))
111108, 102, 109, 110syl3anc 1366 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → (𝑦𝐴 ↔ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴)))
112107, 111mpbird 247 . . . . . . . . . . 11 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → 𝑦𝐴)
113112, 100jca 553 . . . . . . . . . 10 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) ∧ (𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → (𝑦𝐴 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
1141133expia 1286 . . . . . . . . 9 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ((𝑦 ∈ On ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵) → (𝑦𝐴 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)))
115114reximdv2 3043 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → (∃𝑦 ∈ On ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵 → ∃𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
11699, 115mpd 15 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On)) → ∃𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)
117116expcom 450 . . . . . 6 ((𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧) ∧ 𝑥 ∈ On) → ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
1181173expia 1286 . . . . 5 ((𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → (𝑥 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)))
119118com13 88 . . . 4 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → (𝑥 ∈ On → ((𝐵 ∈ (𝐴 ·𝑜 suc 𝑥) ∧ ∀𝑧𝑥 ¬ 𝐵 ∈ (𝐴 ·𝑜 suc 𝑧)) → ∃𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)))
120119reximdvai 3044 . . 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 383  w3o 1053  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  Vcvv 3231  wss 3607  c0 3948   ciun 4552  Ord word 5760  Oncon0 5761  Lim wlim 5762  suc csuc 5763  (class class class)co 6690   +𝑜 coa 7602   ·𝑜 comu 7603
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-omul 7610
This theorem is referenced by:  omeu  7710
  Copyright terms: Public domain W3C validator