Step |
Hyp |
Ref |
Expression |
1 |
|
onelon |
⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ On ) |
2 |
1
|
ex |
⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → 𝐴 ∈ On ) ) |
3 |
2
|
adantr |
⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → 𝐴 ∈ On ) ) |
4 |
|
oewordri |
⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( 𝐴 ↑o 𝐶 ) ⊆ ( 𝐵 ↑o 𝐶 ) ) ) |
5 |
4
|
3adant1 |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( 𝐴 ↑o 𝐶 ) ⊆ ( 𝐵 ↑o 𝐶 ) ) ) |
6 |
|
oecl |
⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ↑o 𝐶 ) ∈ On ) |
7 |
6
|
3adant2 |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ↑o 𝐶 ) ∈ On ) |
8 |
|
oecl |
⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ↑o 𝐶 ) ∈ On ) |
9 |
8
|
3adant1 |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ↑o 𝐶 ) ∈ On ) |
10 |
|
simp1 |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → 𝐴 ∈ On ) |
11 |
|
omwordri |
⊢ ( ( ( 𝐴 ↑o 𝐶 ) ∈ On ∧ ( 𝐵 ↑o 𝐶 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝐴 ↑o 𝐶 ) ⊆ ( 𝐵 ↑o 𝐶 ) → ( ( 𝐴 ↑o 𝐶 ) ·o 𝐴 ) ⊆ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ) ) |
12 |
7 9 10 11
|
syl3anc |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ↑o 𝐶 ) ⊆ ( 𝐵 ↑o 𝐶 ) → ( ( 𝐴 ↑o 𝐶 ) ·o 𝐴 ) ⊆ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ) ) |
13 |
5 12
|
syld |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( ( 𝐴 ↑o 𝐶 ) ·o 𝐴 ) ⊆ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ) ) |
14 |
|
oesuc |
⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ↑o suc 𝐶 ) = ( ( 𝐴 ↑o 𝐶 ) ·o 𝐴 ) ) |
15 |
14
|
3adant2 |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ↑o suc 𝐶 ) = ( ( 𝐴 ↑o 𝐶 ) ·o 𝐴 ) ) |
16 |
15
|
sseq1d |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ↑o suc 𝐶 ) ⊆ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ↔ ( ( 𝐴 ↑o 𝐶 ) ·o 𝐴 ) ⊆ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ) ) |
17 |
13 16
|
sylibrd |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( 𝐴 ↑o suc 𝐶 ) ⊆ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ) ) |
18 |
|
ne0i |
⊢ ( 𝐴 ∈ 𝐵 → 𝐵 ≠ ∅ ) |
19 |
|
on0eln0 |
⊢ ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 ↔ 𝐵 ≠ ∅ ) ) |
20 |
18 19
|
syl5ibr |
⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → ∅ ∈ 𝐵 ) ) |
21 |
20
|
adantr |
⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ∅ ∈ 𝐵 ) ) |
22 |
|
oen0 |
⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐵 ) → ∅ ∈ ( 𝐵 ↑o 𝐶 ) ) |
23 |
22
|
ex |
⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ∅ ∈ 𝐵 → ∅ ∈ ( 𝐵 ↑o 𝐶 ) ) ) |
24 |
21 23
|
syld |
⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ∅ ∈ ( 𝐵 ↑o 𝐶 ) ) ) |
25 |
|
omordi |
⊢ ( ( ( 𝐵 ∈ On ∧ ( 𝐵 ↑o 𝐶 ) ∈ On ) ∧ ∅ ∈ ( 𝐵 ↑o 𝐶 ) ) → ( 𝐴 ∈ 𝐵 → ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∈ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐵 ) ) ) |
26 |
8 25
|
syldanl |
⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ ( 𝐵 ↑o 𝐶 ) ) → ( 𝐴 ∈ 𝐵 → ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∈ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐵 ) ) ) |
27 |
26
|
ex |
⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ∅ ∈ ( 𝐵 ↑o 𝐶 ) → ( 𝐴 ∈ 𝐵 → ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∈ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐵 ) ) ) ) |
28 |
27
|
com23 |
⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( ∅ ∈ ( 𝐵 ↑o 𝐶 ) → ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∈ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐵 ) ) ) ) |
29 |
24 28
|
mpdd |
⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∈ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐵 ) ) ) |
30 |
29
|
3adant1 |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∈ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐵 ) ) ) |
31 |
|
oesuc |
⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ↑o suc 𝐶 ) = ( ( 𝐵 ↑o 𝐶 ) ·o 𝐵 ) ) |
32 |
31
|
3adant1 |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ↑o suc 𝐶 ) = ( ( 𝐵 ↑o 𝐶 ) ·o 𝐵 ) ) |
33 |
32
|
eleq2d |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∈ ( 𝐵 ↑o suc 𝐶 ) ↔ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∈ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐵 ) ) ) |
34 |
30 33
|
sylibrd |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∈ ( 𝐵 ↑o suc 𝐶 ) ) ) |
35 |
17 34
|
jcad |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( ( 𝐴 ↑o suc 𝐶 ) ⊆ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∧ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∈ ( 𝐵 ↑o suc 𝐶 ) ) ) ) |
36 |
35
|
3expa |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( ( 𝐴 ↑o suc 𝐶 ) ⊆ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∧ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∈ ( 𝐵 ↑o suc 𝐶 ) ) ) ) |
37 |
|
sucelon |
⊢ ( 𝐶 ∈ On ↔ suc 𝐶 ∈ On ) |
38 |
|
oecl |
⊢ ( ( 𝐴 ∈ On ∧ suc 𝐶 ∈ On ) → ( 𝐴 ↑o suc 𝐶 ) ∈ On ) |
39 |
|
oecl |
⊢ ( ( 𝐵 ∈ On ∧ suc 𝐶 ∈ On ) → ( 𝐵 ↑o suc 𝐶 ) ∈ On ) |
40 |
|
ontr2 |
⊢ ( ( ( 𝐴 ↑o suc 𝐶 ) ∈ On ∧ ( 𝐵 ↑o suc 𝐶 ) ∈ On ) → ( ( ( 𝐴 ↑o suc 𝐶 ) ⊆ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∧ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∈ ( 𝐵 ↑o suc 𝐶 ) ) → ( 𝐴 ↑o suc 𝐶 ) ∈ ( 𝐵 ↑o suc 𝐶 ) ) ) |
41 |
38 39 40
|
syl2an |
⊢ ( ( ( 𝐴 ∈ On ∧ suc 𝐶 ∈ On ) ∧ ( 𝐵 ∈ On ∧ suc 𝐶 ∈ On ) ) → ( ( ( 𝐴 ↑o suc 𝐶 ) ⊆ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∧ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∈ ( 𝐵 ↑o suc 𝐶 ) ) → ( 𝐴 ↑o suc 𝐶 ) ∈ ( 𝐵 ↑o suc 𝐶 ) ) ) |
42 |
41
|
anandirs |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ suc 𝐶 ∈ On ) → ( ( ( 𝐴 ↑o suc 𝐶 ) ⊆ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∧ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∈ ( 𝐵 ↑o suc 𝐶 ) ) → ( 𝐴 ↑o suc 𝐶 ) ∈ ( 𝐵 ↑o suc 𝐶 ) ) ) |
43 |
37 42
|
sylan2b |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ( ( ( 𝐴 ↑o suc 𝐶 ) ⊆ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∧ ( ( 𝐵 ↑o 𝐶 ) ·o 𝐴 ) ∈ ( 𝐵 ↑o suc 𝐶 ) ) → ( 𝐴 ↑o suc 𝐶 ) ∈ ( 𝐵 ↑o suc 𝐶 ) ) ) |
44 |
36 43
|
syld |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( 𝐴 ↑o suc 𝐶 ) ∈ ( 𝐵 ↑o suc 𝐶 ) ) ) |
45 |
44
|
exp31 |
⊢ ( 𝐴 ∈ On → ( 𝐵 ∈ On → ( 𝐶 ∈ On → ( 𝐴 ∈ 𝐵 → ( 𝐴 ↑o suc 𝐶 ) ∈ ( 𝐵 ↑o suc 𝐶 ) ) ) ) ) |
46 |
45
|
com4l |
⊢ ( 𝐵 ∈ On → ( 𝐶 ∈ On → ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ On → ( 𝐴 ↑o suc 𝐶 ) ∈ ( 𝐵 ↑o suc 𝐶 ) ) ) ) ) |
47 |
46
|
imp |
⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ On → ( 𝐴 ↑o suc 𝐶 ) ∈ ( 𝐵 ↑o suc 𝐶 ) ) ) ) |
48 |
3 47
|
mpdd |
⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( 𝐴 ↑o suc 𝐶 ) ∈ ( 𝐵 ↑o suc 𝐶 ) ) ) |