This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oewordri

Description: Weak ordering property of ordinal exponentiation. Proposition 8.35 of TakeutiZaring p. 68. (Contributed by NM, 6-Jan-2005)

Ref Expression
Assertion oewordri ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( 𝐴 ↑o 𝐶 ) ⊆ ( 𝐵 ↑o 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o ∅ ) )
2 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝐵 ↑o 𝑥 ) = ( 𝐵 ↑o ∅ ) )
3 1 2 sseq12d ⊢ ( 𝑥 = ∅ → ( ( 𝐴 ↑o 𝑥 ) ⊆ ( 𝐵 ↑o 𝑥 ) ↔ ( 𝐴 ↑o ∅ ) ⊆ ( 𝐵 ↑o ∅ ) ) )
4 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o 𝑦 ) )
5 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ↑o 𝑥 ) = ( 𝐵 ↑o 𝑦 ) )
6 4 5 sseq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ↑o 𝑥 ) ⊆ ( 𝐵 ↑o 𝑥 ) ↔ ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐵 ↑o 𝑦 ) ) )
7 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o suc 𝑦 ) )
8 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐵 ↑o 𝑥 ) = ( 𝐵 ↑o suc 𝑦 ) )
9 7 8 sseq12d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ↑o 𝑥 ) ⊆ ( 𝐵 ↑o 𝑥 ) ↔ ( 𝐴 ↑o suc 𝑦 ) ⊆ ( 𝐵 ↑o suc 𝑦 ) ) )
10 oveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o 𝐶 ) )
11 oveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐵 ↑o 𝑥 ) = ( 𝐵 ↑o 𝐶 ) )
12 10 11 sseq12d ⊢ ( 𝑥 = 𝐶 → ( ( 𝐴 ↑o 𝑥 ) ⊆ ( 𝐵 ↑o 𝑥 ) ↔ ( 𝐴 ↑o 𝐶 ) ⊆ ( 𝐵 ↑o 𝐶 ) ) )
13 onelon ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ On )
14 oe0 ⊢ ( 𝐴 ∈ On → ( 𝐴 ↑o ∅ ) = 1o )
15 13 14 syl ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ↑o ∅ ) = 1o )
16 oe0 ⊢ ( 𝐵 ∈ On → ( 𝐵 ↑o ∅ ) = 1o )
17 16 adantr ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → ( 𝐵 ↑o ∅ ) = 1o )
18 15 17 eqtr4d ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ↑o ∅ ) = ( 𝐵 ↑o ∅ ) )
19 eqimss ⊢ ( ( 𝐴 ↑o ∅ ) = ( 𝐵 ↑o ∅ ) → ( 𝐴 ↑o ∅ ) ⊆ ( 𝐵 ↑o ∅ ) )
20 18 19 syl ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ↑o ∅ ) ⊆ ( 𝐵 ↑o ∅ ) )
21 simpl ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → 𝐵 ∈ On )
22 onelss ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → 𝐴 ⊆ 𝐵 ) )
23 22 imp ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ⊆ 𝐵 )
24 13 21 23 jca31 ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) )
25 oecl ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o 𝑦 ) ∈ On )
26 25 3adant2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o 𝑦 ) ∈ On )
27 oecl ⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 ↑o 𝑦 ) ∈ On )
28 27 3adant1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 ↑o 𝑦 ) ∈ On )
29 simp1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → 𝐴 ∈ On )
30 omwordri ⊢ ( ( ( 𝐴 ↑o 𝑦 ) ∈ On ∧ ( 𝐵 ↑o 𝑦 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐵 ↑o 𝑦 ) → ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ⊆ ( ( 𝐵 ↑o 𝑦 ) ·o 𝐴 ) ) )
31 26 28 29 30 syl3anc ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐵 ↑o 𝑦 ) → ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ⊆ ( ( 𝐵 ↑o 𝑦 ) ·o 𝐴 ) ) )
32 31 imp ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐵 ↑o 𝑦 ) ) → ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ⊆ ( ( 𝐵 ↑o 𝑦 ) ·o 𝐴 ) )
33 32 adantrl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐵 ↑o 𝑦 ) ) ) → ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ⊆ ( ( 𝐵 ↑o 𝑦 ) ·o 𝐴 ) )
34 omwordi ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ ( 𝐵 ↑o 𝑦 ) ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( ( 𝐵 ↑o 𝑦 ) ·o 𝐴 ) ⊆ ( ( 𝐵 ↑o 𝑦 ) ·o 𝐵 ) ) )
35 28 34 syld3an3 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( ( 𝐵 ↑o 𝑦 ) ·o 𝐴 ) ⊆ ( ( 𝐵 ↑o 𝑦 ) ·o 𝐵 ) ) )
36 35 imp ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝐵 ↑o 𝑦 ) ·o 𝐴 ) ⊆ ( ( 𝐵 ↑o 𝑦 ) ·o 𝐵 ) )
37 36 adantrr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐵 ↑o 𝑦 ) ) ) → ( ( 𝐵 ↑o 𝑦 ) ·o 𝐴 ) ⊆ ( ( 𝐵 ↑o 𝑦 ) ·o 𝐵 ) )
38 33 37 sstrd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐵 ↑o 𝑦 ) ) ) → ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ⊆ ( ( 𝐵 ↑o 𝑦 ) ·o 𝐵 ) )
39 oesuc ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o suc 𝑦 ) = ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) )
40 39 3adant2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o suc 𝑦 ) = ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) )
41 40 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐵 ↑o 𝑦 ) ) ) → ( 𝐴 ↑o suc 𝑦 ) = ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) )
42 oesuc ⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 ↑o suc 𝑦 ) = ( ( 𝐵 ↑o 𝑦 ) ·o 𝐵 ) )
43 42 3adant1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 ↑o suc 𝑦 ) = ( ( 𝐵 ↑o 𝑦 ) ·o 𝐵 ) )
44 43 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐵 ↑o 𝑦 ) ) ) → ( 𝐵 ↑o suc 𝑦 ) = ( ( 𝐵 ↑o 𝑦 ) ·o 𝐵 ) )
45 38 41 44 3sstr4d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐵 ↑o 𝑦 ) ) ) → ( 𝐴 ↑o suc 𝑦 ) ⊆ ( 𝐵 ↑o suc 𝑦 ) )
46 45 exp520 ⊢ ( 𝐴 ∈ On → ( 𝐵 ∈ On → ( 𝑦 ∈ On → ( 𝐴 ⊆ 𝐵 → ( ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐵 ↑o 𝑦 ) → ( 𝐴 ↑o suc 𝑦 ) ⊆ ( 𝐵 ↑o suc 𝑦 ) ) ) ) ) )
47 46 com3r ⊢ ( 𝑦 ∈ On → ( 𝐴 ∈ On → ( 𝐵 ∈ On → ( 𝐴 ⊆ 𝐵 → ( ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐵 ↑o 𝑦 ) → ( 𝐴 ↑o suc 𝑦 ) ⊆ ( 𝐵 ↑o suc 𝑦 ) ) ) ) ) )
48 47 imp4c ⊢ ( 𝑦 ∈ On → ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐵 ↑o 𝑦 ) → ( 𝐴 ↑o suc 𝑦 ) ⊆ ( 𝐵 ↑o suc 𝑦 ) ) ) )
49 24 48 syl5 ⊢ ( 𝑦 ∈ On → ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐵 ↑o 𝑦 ) → ( 𝐴 ↑o suc 𝑦 ) ⊆ ( 𝐵 ↑o suc 𝑦 ) ) ) )
50 vex ⊢ 𝑥 ∈ V
51 limelon ⊢ ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → 𝑥 ∈ On )
52 50 51 mpan ⊢ ( Lim 𝑥 → 𝑥 ∈ On )
53 0ellim ⊢ ( Lim 𝑥 → ∅ ∈ 𝑥 )
54 oe0m1 ⊢ ( 𝑥 ∈ On → ( ∅ ∈ 𝑥 ↔ ( ∅ ↑o 𝑥 ) = ∅ ) )
55 54 biimpa ⊢ ( ( 𝑥 ∈ On ∧ ∅ ∈ 𝑥 ) → ( ∅ ↑o 𝑥 ) = ∅ )
56 52 53 55 syl2anc ⊢ ( Lim 𝑥 → ( ∅ ↑o 𝑥 ) = ∅ )
57 0ss ⊢ ∅ ⊆ ( 𝐵 ↑o 𝑥 )
58 56 57 eqsstrdi ⊢ ( Lim 𝑥 → ( ∅ ↑o 𝑥 ) ⊆ ( 𝐵 ↑o 𝑥 ) )
59 oveq1 ⊢ ( 𝐴 = ∅ → ( 𝐴 ↑o 𝑥 ) = ( ∅ ↑o 𝑥 ) )
60 59 sseq1d ⊢ ( 𝐴 = ∅ → ( ( 𝐴 ↑o 𝑥 ) ⊆ ( 𝐵 ↑o 𝑥 ) ↔ ( ∅ ↑o 𝑥 ) ⊆ ( 𝐵 ↑o 𝑥 ) ) )
61 58 60 imbitrrid ⊢ ( 𝐴 = ∅ → ( Lim 𝑥 → ( 𝐴 ↑o 𝑥 ) ⊆ ( 𝐵 ↑o 𝑥 ) ) )
62 61 adantl ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) ∧ 𝐴 = ∅ ) → ( Lim 𝑥 → ( 𝐴 ↑o 𝑥 ) ⊆ ( 𝐵 ↑o 𝑥 ) ) )
63 62 a1dd ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) ∧ 𝐴 = ∅ ) → ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐵 ↑o 𝑦 ) → ( 𝐴 ↑o 𝑥 ) ⊆ ( 𝐵 ↑o 𝑥 ) ) ) )
64 ss2iun ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐵 ↑o 𝑦 ) → ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐵 ↑o 𝑦 ) )
65 oelim ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
66 50 65 mpanlr1 ⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝑥 ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
67 66 an32s ⊢ ( ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ∧ Lim 𝑥 ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
68 67 adantllr ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ Lim 𝑥 ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
69 21 anim1i ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) ∧ Lim 𝑥 ) → ( 𝐵 ∈ On ∧ Lim 𝑥 ) )
70 ne0i ⊢ ( 𝐴 ∈ 𝐵 → 𝐵 ≠ ∅ )
71 on0eln0 ⊢ ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 ↔ 𝐵 ≠ ∅ ) )
72 70 71 imbitrrid ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → ∅ ∈ 𝐵 ) )
73 72 imp ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → ∅ ∈ 𝐵 )
74 73 adantr ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) ∧ Lim 𝑥 ) → ∅ ∈ 𝐵 )
75 oelim ⊢ ( ( ( 𝐵 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ∧ ∅ ∈ 𝐵 ) → ( 𝐵 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐵 ↑o 𝑦 ) )
76 50 75 mpanlr1 ⊢ ( ( ( 𝐵 ∈ On ∧ Lim 𝑥 ) ∧ ∅ ∈ 𝐵 ) → ( 𝐵 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐵 ↑o 𝑦 ) )
77 69 74 76 syl2anc ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) ∧ Lim 𝑥 ) → ( 𝐵 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐵 ↑o 𝑦 ) )
78 77 ad4ant24 ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ Lim 𝑥 ) → ( 𝐵 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐵 ↑o 𝑦 ) )
79 68 78 sseq12d ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ Lim 𝑥 ) → ( ( 𝐴 ↑o 𝑥 ) ⊆ ( 𝐵 ↑o 𝑥 ) ↔ ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐵 ↑o 𝑦 ) ) )
80 64 79 imbitrrid ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ Lim 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐵 ↑o 𝑦 ) → ( 𝐴 ↑o 𝑥 ) ⊆ ( 𝐵 ↑o 𝑥 ) ) )
81 80 ex ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐵 ↑o 𝑦 ) → ( 𝐴 ↑o 𝑥 ) ⊆ ( 𝐵 ↑o 𝑥 ) ) ) )
82 63 81 oe0lem ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) ) → ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐵 ↑o 𝑦 ) → ( 𝐴 ↑o 𝑥 ) ⊆ ( 𝐵 ↑o 𝑥 ) ) ) )
83 13 ancri ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) ) )
84 82 83 syl11 ⊢ ( Lim 𝑥 → ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐵 ↑o 𝑦 ) → ( 𝐴 ↑o 𝑥 ) ⊆ ( 𝐵 ↑o 𝑥 ) ) ) )
85 3 6 9 12 20 49 84 tfinds3 ⊢ ( 𝐶 ∈ On → ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ↑o 𝐶 ) ⊆ ( 𝐵 ↑o 𝐶 ) ) )
86 85 expd ⊢ ( 𝐶 ∈ On → ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → ( 𝐴 ↑o 𝐶 ) ⊆ ( 𝐵 ↑o 𝐶 ) ) ) )
87 86 impcom ⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( 𝐴 ↑o 𝐶 ) ⊆ ( 𝐵 ↑o 𝐶 ) ) )