Metamath Proof Explorer

Theorem omeulem1

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

Ref Expression
Assertion omeulem1 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 )

Proof

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