Metamath Proof Explorer

Theorem omeulem1

Description: Lemma for omeu : existence part. (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Assertion omeulem1 ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ → ∃ x ∈ On ∃ y ∈ A A ⋅ 𝑜 x + 𝑜 y = B

Proof

Step Hyp Ref Expression
1 simp2 ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ → B ∈ On
2 sucelon ⊢ B ∈ On ↔ suc ⁡ B ∈ On
3 1 2 sylib ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ → suc ⁡ B ∈ On
4 simp1 ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ → A ∈ On
5 on0eln0 ⊢ A ∈ On → ∅ ∈ A ↔ A ≠ ∅
6 5 biimpar ⊢ A ∈ On ∧ A ≠ ∅ → ∅ ∈ A
7 6 3adant2 ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ → ∅ ∈ A
8 omword2 ⊢ suc ⁡ B ∈ On ∧ A ∈ On ∧ ∅ ∈ A → suc ⁡ B ⊆ A ⋅ 𝑜 suc ⁡ B
9 3 4 7 8 syl21anc ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ → suc ⁡ B ⊆ A ⋅ 𝑜 suc ⁡ B
10 sucidg ⊢ B ∈ On → B ∈ suc ⁡ B
11 ssel ⊢ suc ⁡ B ⊆ A ⋅ 𝑜 suc ⁡ B → B ∈ suc ⁡ B → B ∈ A ⋅ 𝑜 suc ⁡ B
12 10 11 syl5 ⊢ suc ⁡ B ⊆ A ⋅ 𝑜 suc ⁡ B → B ∈ On → B ∈ A ⋅ 𝑜 suc ⁡ B
13 9 1 12 sylc ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ → B ∈ A ⋅ 𝑜 suc ⁡ B
14 suceq ⊢ x = B → suc ⁡ x = suc ⁡ B
15 14 oveq2d ⊢ x = B → A ⋅ 𝑜 suc ⁡ x = A ⋅ 𝑜 suc ⁡ B
16 15 eleq2d ⊢ x = B → B ∈ A ⋅ 𝑜 suc ⁡ x ↔ B ∈ A ⋅ 𝑜 suc ⁡ B
17 16 rspcev ⊢ B ∈ On ∧ B ∈ A ⋅ 𝑜 suc ⁡ B → ∃ x ∈ On B ∈ A ⋅ 𝑜 suc ⁡ x
18 1 13 17 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ → ∃ x ∈ On B ∈ A ⋅ 𝑜 suc ⁡ x
19 suceq ⊢ x = z → suc ⁡ x = suc ⁡ z
20 19 oveq2d ⊢ x = z → A ⋅ 𝑜 suc ⁡ x = A ⋅ 𝑜 suc ⁡ z
21 20 eleq2d ⊢ x = z → B ∈ A ⋅ 𝑜 suc ⁡ x ↔ B ∈ A ⋅ 𝑜 suc ⁡ z
22 21 onminex ⊢ ∃ x ∈ On B ∈ A ⋅ 𝑜 suc ⁡ x → ∃ x ∈ On B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z
23 vex ⊢ x ∈ V
24 23 elon ⊢ x ∈ On ↔ Ord ⁡ x
25 ordzsl ⊢ Ord ⁡ x ↔ x = ∅ ∨ ∃ w ∈ On x = suc ⁡ w ∨ Lim ⁡ x
26 24 25 bitri ⊢ x ∈ On ↔ x = ∅ ∨ ∃ w ∈ On x = suc ⁡ w ∨ Lim ⁡ x
27 oveq2 ⊢ x = ∅ → A ⋅ 𝑜 x = A ⋅ 𝑜 ∅
28 om0 ⊢ A ∈ On → A ⋅ 𝑜 ∅ = ∅
29 27 28 sylan9eqr ⊢ A ∈ On ∧ x = ∅ → A ⋅ 𝑜 x = ∅
30 ne0i ⊢ B ∈ A ⋅ 𝑜 x → A ⋅ 𝑜 x ≠ ∅
31 30 necon2bi ⊢ A ⋅ 𝑜 x = ∅ → ¬ B ∈ A ⋅ 𝑜 x
32 29 31 syl ⊢ A ∈ On ∧ x = ∅ → ¬ B ∈ A ⋅ 𝑜 x
33 32 ex ⊢ A ∈ On → x = ∅ → ¬ B ∈ A ⋅ 𝑜 x
34 33 a1d ⊢ A ∈ On → ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z → x = ∅ → ¬ B ∈ A ⋅ 𝑜 x
35 34 3ad2ant1 ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ → ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z → x = ∅ → ¬ B ∈ A ⋅ 𝑜 x
36 35 imp ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z → x = ∅ → ¬ B ∈ A ⋅ 𝑜 x
37 simp3 ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x = suc ⁡ w → x = suc ⁡ w
38 simp2 ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x = suc ⁡ w → ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z
39 raleq ⊢ x = suc ⁡ w → ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ↔ ∀ z ∈ suc ⁡ w ¬ B ∈ A ⋅ 𝑜 suc ⁡ z
40 vex ⊢ w ∈ V
41 40 sucid ⊢ w ∈ suc ⁡ w
42 suceq ⊢ z = w → suc ⁡ z = suc ⁡ w
43 42 oveq2d ⊢ z = w → A ⋅ 𝑜 suc ⁡ z = A ⋅ 𝑜 suc ⁡ w
44 43 eleq2d ⊢ z = w → B ∈ A ⋅ 𝑜 suc ⁡ z ↔ B ∈ A ⋅ 𝑜 suc ⁡ w
45 44 notbid ⊢ z = w → ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ↔ ¬ B ∈ A ⋅ 𝑜 suc ⁡ w
46 45 rspcv ⊢ w ∈ suc ⁡ w → ∀ z ∈ suc ⁡ w ¬ B ∈ A ⋅ 𝑜 suc ⁡ z → ¬ B ∈ A ⋅ 𝑜 suc ⁡ w
47 41 46 ax-mp ⊢ ∀ z ∈ suc ⁡ w ¬ B ∈ A ⋅ 𝑜 suc ⁡ z → ¬ B ∈ A ⋅ 𝑜 suc ⁡ w
48 39 47 syl6bi ⊢ x = suc ⁡ w → ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z → ¬ B ∈ A ⋅ 𝑜 suc ⁡ w
49 37 38 48 sylc ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x = suc ⁡ w → ¬ B ∈ A ⋅ 𝑜 suc ⁡ w
50 oveq2 ⊢ x = suc ⁡ w → A ⋅ 𝑜 x = A ⋅ 𝑜 suc ⁡ w
51 50 eleq2d ⊢ x = suc ⁡ w → B ∈ A ⋅ 𝑜 x ↔ B ∈ A ⋅ 𝑜 suc ⁡ w
52 51 notbid ⊢ x = suc ⁡ w → ¬ B ∈ A ⋅ 𝑜 x ↔ ¬ B ∈ A ⋅ 𝑜 suc ⁡ w
53 52 biimpar ⊢ x = suc ⁡ w ∧ ¬ B ∈ A ⋅ 𝑜 suc ⁡ w → ¬ B ∈ A ⋅ 𝑜 x
54 37 49 53 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x = suc ⁡ w → ¬ B ∈ A ⋅ 𝑜 x
55 54 3expia ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z → x = suc ⁡ w → ¬ B ∈ A ⋅ 𝑜 x
56 55 rexlimdvw ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z → ∃ w ∈ On x = suc ⁡ w → ¬ B ∈ A ⋅ 𝑜 x
57 ralnex ⊢ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ↔ ¬ ∃ z ∈ x B ∈ A ⋅ 𝑜 suc ⁡ z
58 simpr ⊢ Lim ⁡ x ∧ A ∈ On → A ∈ On
59 23 a1i ⊢ Lim ⁡ x ∧ A ∈ On → x ∈ V
60 simpl ⊢ Lim ⁡ x ∧ A ∈ On → Lim ⁡ x
61 omlim ⊢ A ∈ On ∧ x ∈ V ∧ Lim ⁡ x → A ⋅ 𝑜 x = ⋃ z ∈ x A ⋅ 𝑜 z
62 58 59 60 61 syl12anc ⊢ Lim ⁡ x ∧ A ∈ On → A ⋅ 𝑜 x = ⋃ z ∈ x A ⋅ 𝑜 z
63 62 eleq2d ⊢ Lim ⁡ x ∧ A ∈ On → B ∈ A ⋅ 𝑜 x ↔ B ∈ ⋃ z ∈ x A ⋅ 𝑜 z
64 eliun ⊢ B ∈ ⋃ z ∈ x A ⋅ 𝑜 z ↔ ∃ z ∈ x B ∈ A ⋅ 𝑜 z
65 limord ⊢ Lim ⁡ x → Ord ⁡ x
66 65 3ad2ant1 ⊢ Lim ⁡ x ∧ A ∈ On ∧ z ∈ x → Ord ⁡ x
67 66 24 sylibr ⊢ Lim ⁡ x ∧ A ∈ On ∧ z ∈ x → x ∈ On
68 simp3 ⊢ Lim ⁡ x ∧ A ∈ On ∧ z ∈ x → z ∈ x
69 onelon ⊢ x ∈ On ∧ z ∈ x → z ∈ On
70 67 68 69 syl2anc ⊢ Lim ⁡ x ∧ A ∈ On ∧ z ∈ x → z ∈ On
71 suceloni ⊢ z ∈ On → suc ⁡ z ∈ On
72 70 71 syl ⊢ Lim ⁡ x ∧ A ∈ On ∧ z ∈ x → suc ⁡ z ∈ On
73 simp2 ⊢ Lim ⁡ x ∧ A ∈ On ∧ z ∈ x → A ∈ On
74 sssucid ⊢ z ⊆ suc ⁡ z
75 omwordi ⊢ z ∈ On ∧ suc ⁡ z ∈ On ∧ A ∈ On → z ⊆ suc ⁡ z → A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 suc ⁡ z
76 74 75 mpi ⊢ z ∈ On ∧ suc ⁡ z ∈ On ∧ A ∈ On → A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 suc ⁡ z
77 70 72 73 76 syl3anc ⊢ Lim ⁡ x ∧ A ∈ On ∧ z ∈ x → A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 suc ⁡ z
78 77 sseld ⊢ Lim ⁡ x ∧ A ∈ On ∧ z ∈ x → B ∈ A ⋅ 𝑜 z → B ∈ A ⋅ 𝑜 suc ⁡ z
79 78 3expia ⊢ Lim ⁡ x ∧ A ∈ On → z ∈ x → B ∈ A ⋅ 𝑜 z → B ∈ A ⋅ 𝑜 suc ⁡ z
80 79 reximdvai ⊢ Lim ⁡ x ∧ A ∈ On → ∃ z ∈ x B ∈ A ⋅ 𝑜 z → ∃ z ∈ x B ∈ A ⋅ 𝑜 suc ⁡ z
81 64 80 syl5bi ⊢ Lim ⁡ x ∧ A ∈ On → B ∈ ⋃ z ∈ x A ⋅ 𝑜 z → ∃ z ∈ x B ∈ A ⋅ 𝑜 suc ⁡ z
82 63 81 sylbid ⊢ Lim ⁡ x ∧ A ∈ On → B ∈ A ⋅ 𝑜 x → ∃ z ∈ x B ∈ A ⋅ 𝑜 suc ⁡ z
83 82 con3d ⊢ Lim ⁡ x ∧ A ∈ On → ¬ ∃ z ∈ x B ∈ A ⋅ 𝑜 suc ⁡ z → ¬ B ∈ A ⋅ 𝑜 x
84 57 83 syl5bi ⊢ Lim ⁡ x ∧ A ∈ On → ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z → ¬ B ∈ A ⋅ 𝑜 x
85 84 expimpd ⊢ Lim ⁡ x → A ∈ On ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z → ¬ B ∈ A ⋅ 𝑜 x
86 85 com12 ⊢ A ∈ On ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z → Lim ⁡ x → ¬ B ∈ A ⋅ 𝑜 x
87 86 3ad2antl1 ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z → Lim ⁡ x → ¬ B ∈ A ⋅ 𝑜 x
88 36 56 87 3jaod ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z → x = ∅ ∨ ∃ w ∈ On x = suc ⁡ w ∨ Lim ⁡ x → ¬ B ∈ A ⋅ 𝑜 x
89 26 88 syl5bi ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z → x ∈ On → ¬ B ∈ A ⋅ 𝑜 x
90 89 impr ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On → ¬ B ∈ A ⋅ 𝑜 x
91 simpl1 ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On → A ∈ On
92 simprr ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On → x ∈ On
93 omcl ⊢ A ∈ On ∧ x ∈ On → A ⋅ 𝑜 x ∈ On
94 91 92 93 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On → A ⋅ 𝑜 x ∈ On
95 simpl2 ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On → B ∈ On
96 ontri1 ⊢ A ⋅ 𝑜 x ∈ On ∧ B ∈ On → A ⋅ 𝑜 x ⊆ B ↔ ¬ B ∈ A ⋅ 𝑜 x
97 94 95 96 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On → A ⋅ 𝑜 x ⊆ B ↔ ¬ B ∈ A ⋅ 𝑜 x
98 90 97 mpbird ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On → A ⋅ 𝑜 x ⊆ B
99 oawordex ⊢ A ⋅ 𝑜 x ∈ On ∧ B ∈ On → A ⋅ 𝑜 x ⊆ B ↔ ∃ y ∈ On A ⋅ 𝑜 x + 𝑜 y = B
100 94 95 99 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On → A ⋅ 𝑜 x ⊆ B ↔ ∃ y ∈ On A ⋅ 𝑜 x + 𝑜 y = B
101 98 100 mpbid ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On → ∃ y ∈ On A ⋅ 𝑜 x + 𝑜 y = B
102 101 3adantr1 ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On → ∃ y ∈ On A ⋅ 𝑜 x + 𝑜 y = B
103 simp3r ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On ∧ y ∈ On ∧ A ⋅ 𝑜 x + 𝑜 y = B → A ⋅ 𝑜 x + 𝑜 y = B
104 simp21 ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On ∧ y ∈ On ∧ A ⋅ 𝑜 x + 𝑜 y = B → B ∈ A ⋅ 𝑜 suc ⁡ x
105 simp11 ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On ∧ y ∈ On ∧ A ⋅ 𝑜 x + 𝑜 y = B → A ∈ On
106 simp23 ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On ∧ y ∈ On ∧ A ⋅ 𝑜 x + 𝑜 y = B → x ∈ On
107 omsuc ⊢ A ∈ On ∧ x ∈ On → A ⋅ 𝑜 suc ⁡ x = A ⋅ 𝑜 x + 𝑜 A
108 105 106 107 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On ∧ y ∈ On ∧ A ⋅ 𝑜 x + 𝑜 y = B → A ⋅ 𝑜 suc ⁡ x = A ⋅ 𝑜 x + 𝑜 A
109 104 108 eleqtrd ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On ∧ y ∈ On ∧ A ⋅ 𝑜 x + 𝑜 y = B → B ∈ A ⋅ 𝑜 x + 𝑜 A
110 103 109 eqeltrd ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On ∧ y ∈ On ∧ A ⋅ 𝑜 x + 𝑜 y = B → A ⋅ 𝑜 x + 𝑜 y ∈ A ⋅ 𝑜 x + 𝑜 A
111 simp3l ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On ∧ y ∈ On ∧ A ⋅ 𝑜 x + 𝑜 y = B → y ∈ On
112 105 106 93 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On ∧ y ∈ On ∧ A ⋅ 𝑜 x + 𝑜 y = B → A ⋅ 𝑜 x ∈ On
113 oaord ⊢ y ∈ On ∧ A ∈ On ∧ A ⋅ 𝑜 x ∈ On → y ∈ A ↔ A ⋅ 𝑜 x + 𝑜 y ∈ A ⋅ 𝑜 x + 𝑜 A
114 111 105 112 113 syl3anc ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On ∧ y ∈ On ∧ A ⋅ 𝑜 x + 𝑜 y = B → y ∈ A ↔ A ⋅ 𝑜 x + 𝑜 y ∈ A ⋅ 𝑜 x + 𝑜 A
115 110 114 mpbird ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On ∧ y ∈ On ∧ A ⋅ 𝑜 x + 𝑜 y = B → y ∈ A
116 115 103 jca ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On ∧ y ∈ On ∧ A ⋅ 𝑜 x + 𝑜 y = B → y ∈ A ∧ A ⋅ 𝑜 x + 𝑜 y = B
117 116 3expia ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On → y ∈ On ∧ A ⋅ 𝑜 x + 𝑜 y = B → y ∈ A ∧ A ⋅ 𝑜 x + 𝑜 y = B
118 117 reximdv2 ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On → ∃ y ∈ On A ⋅ 𝑜 x + 𝑜 y = B → ∃ y ∈ A A ⋅ 𝑜 x + 𝑜 y = B
119 102 118 mpd ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ∧ B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On → ∃ y ∈ A A ⋅ 𝑜 x + 𝑜 y = B
120 119 expcom ⊢ B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z ∧ x ∈ On → A ∈ On ∧ B ∈ On ∧ A ≠ ∅ → ∃ y ∈ A A ⋅ 𝑜 x + 𝑜 y = B
121 120 3expia ⊢ B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z → x ∈ On → A ∈ On ∧ B ∈ On ∧ A ≠ ∅ → ∃ y ∈ A A ⋅ 𝑜 x + 𝑜 y = B
122 121 com13 ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ → x ∈ On → B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z → ∃ y ∈ A A ⋅ 𝑜 x + 𝑜 y = B
123 122 reximdvai ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ → ∃ x ∈ On B ∈ A ⋅ 𝑜 suc ⁡ x ∧ ∀ z ∈ x ¬ B ∈ A ⋅ 𝑜 suc ⁡ z → ∃ x ∈ On ∃ y ∈ A A ⋅ 𝑜 x + 𝑜 y = B
124 22 123 syl5 ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ → ∃ x ∈ On B ∈ A ⋅ 𝑜 suc ⁡ x → ∃ x ∈ On ∃ y ∈ A A ⋅ 𝑜 x + 𝑜 y = B
125 18 124 mpd ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ → ∃ x ∈ On ∃ y ∈ A A ⋅ 𝑜 x + 𝑜 y = B