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