Metamath Proof Explorer

Theorem oeordi

Description: Ordering law for ordinal exponentiation. Proposition 8.33 of TakeutiZaring p. 67. (Contributed by NM, 5-Jan-2005) (Revised by Mario Carneiro, 24-May-2015)

Ref Expression
Assertion oeordi ( ( 𝐵 ∈ On ∧ 𝐶 ∈ ( On ∖ 2o ) ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑥 = suc 𝐴 → ( 𝐶 ↑o 𝑥 ) = ( 𝐶 ↑o suc 𝐴 ) )
2 1 eleq2d ⊢ ( 𝑥 = suc 𝐴 → ( ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑥 ) ↔ ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o suc 𝐴 ) ) )
3 2 imbi2d ⊢ ( 𝑥 = suc 𝐴 → ( ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑥 ) ) ↔ ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o suc 𝐴 ) ) ) )
4 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐶 ↑o 𝑥 ) = ( 𝐶 ↑o 𝑦 ) )
5 4 eleq2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑥 ) ↔ ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) )
6 5 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑥 ) ) ↔ ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) ) )
7 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐶 ↑o 𝑥 ) = ( 𝐶 ↑o suc 𝑦 ) )
8 7 eleq2d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑥 ) ↔ ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o suc 𝑦 ) ) )
9 8 imbi2d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑥 ) ) ↔ ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o suc 𝑦 ) ) ) )
10 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐶 ↑o 𝑥 ) = ( 𝐶 ↑o 𝐵 ) )
11 10 eleq2d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑥 ) ↔ ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝐵 ) ) )
12 11 imbi2d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑥 ) ) ↔ ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝐵 ) ) ) )
13 eldifi ⊢ ( 𝐶 ∈ ( On ∖ 2o ) → 𝐶 ∈ On )
14 oecl ⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐶 ↑o 𝐴 ) ∈ On )
15 13 14 sylan ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝐴 ∈ On ) → ( 𝐶 ↑o 𝐴 ) ∈ On )
16 om1 ⊢ ( ( 𝐶 ↑o 𝐴 ) ∈ On → ( ( 𝐶 ↑o 𝐴 ) ·o 1o ) = ( 𝐶 ↑o 𝐴 ) )
17 15 16 syl ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝐴 ∈ On ) → ( ( 𝐶 ↑o 𝐴 ) ·o 1o ) = ( 𝐶 ↑o 𝐴 ) )
18 ondif2 ⊢ ( 𝐶 ∈ ( On ∖ 2o ) ↔ ( 𝐶 ∈ On ∧ 1o ∈ 𝐶 ) )
19 18 simprbi ⊢ ( 𝐶 ∈ ( On ∖ 2o ) → 1o ∈ 𝐶 )
20 19 adantr ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝐴 ∈ On ) → 1o ∈ 𝐶 )
21 13 adantr ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝐴 ∈ On ) → 𝐶 ∈ On )
22 simpr ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝐴 ∈ On ) → 𝐴 ∈ On )
23 dif20el ⊢ ( 𝐶 ∈ ( On ∖ 2o ) → ∅ ∈ 𝐶 )
24 23 adantr ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝐴 ∈ On ) → ∅ ∈ 𝐶 )
25 oen0 ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ∅ ∈ ( 𝐶 ↑o 𝐴 ) )
26 21 22 24 25 syl21anc ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝐴 ∈ On ) → ∅ ∈ ( 𝐶 ↑o 𝐴 ) )
27 omordi ⊢ ( ( ( 𝐶 ∈ On ∧ ( 𝐶 ↑o 𝐴 ) ∈ On ) ∧ ∅ ∈ ( 𝐶 ↑o 𝐴 ) ) → ( 1o ∈ 𝐶 → ( ( 𝐶 ↑o 𝐴 ) ·o 1o ) ∈ ( ( 𝐶 ↑o 𝐴 ) ·o 𝐶 ) ) )
28 21 15 26 27 syl21anc ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝐴 ∈ On ) → ( 1o ∈ 𝐶 → ( ( 𝐶 ↑o 𝐴 ) ·o 1o ) ∈ ( ( 𝐶 ↑o 𝐴 ) ·o 𝐶 ) ) )
29 20 28 mpd ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝐴 ∈ On ) → ( ( 𝐶 ↑o 𝐴 ) ·o 1o ) ∈ ( ( 𝐶 ↑o 𝐴 ) ·o 𝐶 ) )
30 17 29 eqeltrrd ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝐴 ∈ On ) → ( 𝐶 ↑o 𝐴 ) ∈ ( ( 𝐶 ↑o 𝐴 ) ·o 𝐶 ) )
31 oesuc ⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐶 ↑o suc 𝐴 ) = ( ( 𝐶 ↑o 𝐴 ) ·o 𝐶 ) )
32 13 31 sylan ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝐴 ∈ On ) → ( 𝐶 ↑o suc 𝐴 ) = ( ( 𝐶 ↑o 𝐴 ) ·o 𝐶 ) )
33 30 32 eleqtrrd ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝐴 ∈ On ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o suc 𝐴 ) )
34 33 expcom ⊢ ( 𝐴 ∈ On → ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o suc 𝐴 ) ) )
35 oecl ⊢ ( ( 𝐶 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐶 ↑o 𝑦 ) ∈ On )
36 13 35 sylan ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( 𝐶 ↑o 𝑦 ) ∈ On )
37 om1 ⊢ ( ( 𝐶 ↑o 𝑦 ) ∈ On → ( ( 𝐶 ↑o 𝑦 ) ·o 1o ) = ( 𝐶 ↑o 𝑦 ) )
38 36 37 syl ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( ( 𝐶 ↑o 𝑦 ) ·o 1o ) = ( 𝐶 ↑o 𝑦 ) )
39 19 adantr ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → 1o ∈ 𝐶 )
40 13 adantr ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → 𝐶 ∈ On )
41 simpr ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → 𝑦 ∈ On )
42 23 adantr ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ∅ ∈ 𝐶 )
43 oen0 ⊢ ( ( ( 𝐶 ∈ On ∧ 𝑦 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ∅ ∈ ( 𝐶 ↑o 𝑦 ) )
44 40 41 42 43 syl21anc ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ∅ ∈ ( 𝐶 ↑o 𝑦 ) )
45 omordi ⊢ ( ( ( 𝐶 ∈ On ∧ ( 𝐶 ↑o 𝑦 ) ∈ On ) ∧ ∅ ∈ ( 𝐶 ↑o 𝑦 ) ) → ( 1o ∈ 𝐶 → ( ( 𝐶 ↑o 𝑦 ) ·o 1o ) ∈ ( ( 𝐶 ↑o 𝑦 ) ·o 𝐶 ) ) )
46 40 36 44 45 syl21anc ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( 1o ∈ 𝐶 → ( ( 𝐶 ↑o 𝑦 ) ·o 1o ) ∈ ( ( 𝐶 ↑o 𝑦 ) ·o 𝐶 ) ) )
47 39 46 mpd ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( ( 𝐶 ↑o 𝑦 ) ·o 1o ) ∈ ( ( 𝐶 ↑o 𝑦 ) ·o 𝐶 ) )
48 38 47 eqeltrrd ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( 𝐶 ↑o 𝑦 ) ∈ ( ( 𝐶 ↑o 𝑦 ) ·o 𝐶 ) )
49 oesuc ⊢ ( ( 𝐶 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐶 ↑o suc 𝑦 ) = ( ( 𝐶 ↑o 𝑦 ) ·o 𝐶 ) )
50 13 49 sylan ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( 𝐶 ↑o suc 𝑦 ) = ( ( 𝐶 ↑o 𝑦 ) ·o 𝐶 ) )
51 48 50 eleqtrrd ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( 𝐶 ↑o 𝑦 ) ∈ ( 𝐶 ↑o suc 𝑦 ) )
52 suceloni ⊢ ( 𝑦 ∈ On → suc 𝑦 ∈ On )
53 oecl ⊢ ( ( 𝐶 ∈ On ∧ suc 𝑦 ∈ On ) → ( 𝐶 ↑o suc 𝑦 ) ∈ On )
54 13 52 53 syl2an ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( 𝐶 ↑o suc 𝑦 ) ∈ On )
55 ontr1 ⊢ ( ( 𝐶 ↑o suc 𝑦 ) ∈ On → ( ( ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ∧ ( 𝐶 ↑o 𝑦 ) ∈ ( 𝐶 ↑o suc 𝑦 ) ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o suc 𝑦 ) ) )
56 54 55 syl ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( ( ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ∧ ( 𝐶 ↑o 𝑦 ) ∈ ( 𝐶 ↑o suc 𝑦 ) ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o suc 𝑦 ) ) )
57 51 56 mpan2d ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o suc 𝑦 ) ) )
58 57 expcom ⊢ ( 𝑦 ∈ On → ( 𝐶 ∈ ( On ∖ 2o ) → ( ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o suc 𝑦 ) ) ) )
59 58 adantr ⊢ ( ( 𝑦 ∈ On ∧ 𝐴 ∈ 𝑦 ) → ( 𝐶 ∈ ( On ∖ 2o ) → ( ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o suc 𝑦 ) ) ) )
60 59 a2d ⊢ ( ( 𝑦 ∈ On ∧ 𝐴 ∈ 𝑦 ) → ( ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) → ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o suc 𝑦 ) ) ) )
61 bi2.04 ⊢ ( ( 𝐴 ∈ 𝑦 → ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) ) ↔ ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐴 ∈ 𝑦 → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) ) )
62 61 ralbii ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∈ 𝑦 → ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐴 ∈ 𝑦 → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) ) )
63 r19.21v ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐴 ∈ 𝑦 → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) ) ↔ ( 𝐶 ∈ ( On ∖ 2o ) → ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∈ 𝑦 → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) ) )
64 62 63 bitri ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∈ 𝑦 → ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) ) ↔ ( 𝐶 ∈ ( On ∖ 2o ) → ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∈ 𝑦 → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) ) )
65 limsuc ⊢ ( Lim 𝑥 → ( 𝐴 ∈ 𝑥 ↔ suc 𝐴 ∈ 𝑥 ) )
66 65 biimpa ⊢ ( ( Lim 𝑥 ∧ 𝐴 ∈ 𝑥 ) → suc 𝐴 ∈ 𝑥 )
67 elex ⊢ ( suc 𝐴 ∈ 𝑥 → suc 𝐴 ∈ V )
68 sucexb ⊢ ( 𝐴 ∈ V ↔ suc 𝐴 ∈ V )
69 sucidg ⊢ ( 𝐴 ∈ V → 𝐴 ∈ suc 𝐴 )
70 68 69 sylbir ⊢ ( suc 𝐴 ∈ V → 𝐴 ∈ suc 𝐴 )
71 67 70 syl ⊢ ( suc 𝐴 ∈ 𝑥 → 𝐴 ∈ suc 𝐴 )
72 eleq2 ⊢ ( 𝑦 = suc 𝐴 → ( 𝐴 ∈ 𝑦 ↔ 𝐴 ∈ suc 𝐴 ) )
73 oveq2 ⊢ ( 𝑦 = suc 𝐴 → ( 𝐶 ↑o 𝑦 ) = ( 𝐶 ↑o suc 𝐴 ) )
74 73 eleq2d ⊢ ( 𝑦 = suc 𝐴 → ( ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ↔ ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o suc 𝐴 ) ) )
75 72 74 imbi12d ⊢ ( 𝑦 = suc 𝐴 → ( ( 𝐴 ∈ 𝑦 → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) ↔ ( 𝐴 ∈ suc 𝐴 → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o suc 𝐴 ) ) ) )
76 75 rspcv ⊢ ( suc 𝐴 ∈ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∈ 𝑦 → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) → ( 𝐴 ∈ suc 𝐴 → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o suc 𝐴 ) ) ) )
77 71 76 mpid ⊢ ( suc 𝐴 ∈ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∈ 𝑦 → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o suc 𝐴 ) ) )
78 77 anc2li ⊢ ( suc 𝐴 ∈ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∈ 𝑦 → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) → ( suc 𝐴 ∈ 𝑥 ∧ ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o suc 𝐴 ) ) ) )
79 73 eliuni ⊢ ( ( suc 𝐴 ∈ 𝑥 ∧ ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o suc 𝐴 ) ) → ( 𝐶 ↑o 𝐴 ) ∈ ∪ 𝑦 ∈ 𝑥 ( 𝐶 ↑o 𝑦 ) )
80 78 79 syl6 ⊢ ( suc 𝐴 ∈ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∈ 𝑦 → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) → ( 𝐶 ↑o 𝐴 ) ∈ ∪ 𝑦 ∈ 𝑥 ( 𝐶 ↑o 𝑦 ) ) )
81 66 80 syl ⊢ ( ( Lim 𝑥 ∧ 𝐴 ∈ 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∈ 𝑦 → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) → ( 𝐶 ↑o 𝐴 ) ∈ ∪ 𝑦 ∈ 𝑥 ( 𝐶 ↑o 𝑦 ) ) )
82 81 adantr ⊢ ( ( ( Lim 𝑥 ∧ 𝐴 ∈ 𝑥 ) ∧ 𝐶 ∈ ( On ∖ 2o ) ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∈ 𝑦 → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) → ( 𝐶 ↑o 𝐴 ) ∈ ∪ 𝑦 ∈ 𝑥 ( 𝐶 ↑o 𝑦 ) ) )
83 13 adantl ⊢ ( ( Lim 𝑥 ∧ 𝐶 ∈ ( On ∖ 2o ) ) → 𝐶 ∈ On )
84 simpl ⊢ ( ( Lim 𝑥 ∧ 𝐶 ∈ ( On ∖ 2o ) ) → Lim 𝑥 )
85 23 adantl ⊢ ( ( Lim 𝑥 ∧ 𝐶 ∈ ( On ∖ 2o ) ) → ∅ ∈ 𝐶 )
86 vex ⊢ 𝑥 ∈ V
87 oelim ⊢ ( ( ( 𝐶 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ∧ ∅ ∈ 𝐶 ) → ( 𝐶 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐶 ↑o 𝑦 ) )
88 86 87 mpanlr1 ⊢ ( ( ( 𝐶 ∈ On ∧ Lim 𝑥 ) ∧ ∅ ∈ 𝐶 ) → ( 𝐶 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐶 ↑o 𝑦 ) )
89 83 84 85 88 syl21anc ⊢ ( ( Lim 𝑥 ∧ 𝐶 ∈ ( On ∖ 2o ) ) → ( 𝐶 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐶 ↑o 𝑦 ) )
90 89 adantlr ⊢ ( ( ( Lim 𝑥 ∧ 𝐴 ∈ 𝑥 ) ∧ 𝐶 ∈ ( On ∖ 2o ) ) → ( 𝐶 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐶 ↑o 𝑦 ) )
91 90 eleq2d ⊢ ( ( ( Lim 𝑥 ∧ 𝐴 ∈ 𝑥 ) ∧ 𝐶 ∈ ( On ∖ 2o ) ) → ( ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑥 ) ↔ ( 𝐶 ↑o 𝐴 ) ∈ ∪ 𝑦 ∈ 𝑥 ( 𝐶 ↑o 𝑦 ) ) )
92 82 91 sylibrd ⊢ ( ( ( Lim 𝑥 ∧ 𝐴 ∈ 𝑥 ) ∧ 𝐶 ∈ ( On ∖ 2o ) ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∈ 𝑦 → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑥 ) ) )
93 92 ex ⊢ ( ( Lim 𝑥 ∧ 𝐴 ∈ 𝑥 ) → ( 𝐶 ∈ ( On ∖ 2o ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∈ 𝑦 → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑥 ) ) ) )
94 93 a2d ⊢ ( ( Lim 𝑥 ∧ 𝐴 ∈ 𝑥 ) → ( ( 𝐶 ∈ ( On ∖ 2o ) → ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∈ 𝑦 → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) ) → ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑥 ) ) ) )
95 64 94 syl5bi ⊢ ( ( Lim 𝑥 ∧ 𝐴 ∈ 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∈ 𝑦 → ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑦 ) ) ) → ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝑥 ) ) ) )
96 3 6 9 12 34 60 95 tfindsg2 ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝐵 ) ) )
97 96 impancom ⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ ( On ∖ 2o ) ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝐵 ) ) )