Metamath Proof Explorer

Theorem omordi

Description: Ordering property of ordinal multiplication. Half of Proposition 8.19 of TakeutiZaring p. 63. Lemma 3.15 of Schloeder p. 9. (Contributed by NM, 14-Dec-2004)

Ref Expression
Assertion omordi ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 onelon ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ On )
2 1 ex ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → 𝐴 ∈ On ) )
3 eleq2 ⊢ ( 𝑥 = ∅ → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ ∅ ) )
4 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝐶 ·o 𝑥 ) = ( 𝐶 ·o ∅ ) )
5 4 eleq2d ⊢ ( 𝑥 = ∅ → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o ∅ ) ) )
6 3 5 imbi12d ⊢ ( 𝑥 = ∅ → ( ( 𝐴 ∈ 𝑥 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ) ↔ ( 𝐴 ∈ ∅ → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o ∅ ) ) ) )
7 eleq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦 ) )
8 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐶 ·o 𝑥 ) = ( 𝐶 ·o 𝑦 ) )
9 8 eleq2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) )
10 7 9 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∈ 𝑥 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ) ↔ ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) ) )
11 eleq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ suc 𝑦 ) )
12 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐶 ·o 𝑥 ) = ( 𝐶 ·o suc 𝑦 ) )
13 12 eleq2d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝑦 ) ) )
14 11 13 imbi12d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ∈ 𝑥 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ) ↔ ( 𝐴 ∈ suc 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝑦 ) ) ) )
15 eleq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵 ) )
16 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐶 ·o 𝑥 ) = ( 𝐶 ·o 𝐵 ) )
17 16 eleq2d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )
18 15 17 imbi12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ∈ 𝑥 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ) ↔ ( 𝐴 ∈ 𝐵 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) )
19 noel ⊢ ¬ 𝐴 ∈ ∅
20 19 pm2.21i ⊢ ( 𝐴 ∈ ∅ → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o ∅ ) )
21 20 a1i ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ ∅ → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o ∅ ) ) )
22 elsuci ⊢ ( 𝐴 ∈ suc 𝑦 → ( 𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ) )
23 omcl ⊢ ( ( 𝐶 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐶 ·o 𝑦 ) ∈ On )
24 simpl ⊢ ( ( 𝐶 ∈ On ∧ 𝑦 ∈ On ) → 𝐶 ∈ On )
25 23 24 jca ⊢ ( ( 𝐶 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐶 ·o 𝑦 ) ∈ On ∧ 𝐶 ∈ On ) )
26 oaword1 ⊢ ( ( ( 𝐶 ·o 𝑦 ) ∈ On ∧ 𝐶 ∈ On ) → ( 𝐶 ·o 𝑦 ) ⊆ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) )
27 26 sseld ⊢ ( ( ( 𝐶 ·o 𝑦 ) ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) → ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
28 27 imim2d ⊢ ( ( ( 𝐶 ·o 𝑦 ) ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) → ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) ) )
29 28 imp ⊢ ( ( ( ( 𝐶 ·o 𝑦 ) ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) ) → ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
30 29 adantrl ⊢ ( ( ( ( 𝐶 ·o 𝑦 ) ∈ On ∧ 𝐶 ∈ On ) ∧ ( ∅ ∈ 𝐶 ∧ ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) ) ) → ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
31 oaord1 ⊢ ( ( ( 𝐶 ·o 𝑦 ) ∈ On ∧ 𝐶 ∈ On ) → ( ∅ ∈ 𝐶 ↔ ( 𝐶 ·o 𝑦 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
32 31 biimpa ⊢ ( ( ( ( 𝐶 ·o 𝑦 ) ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐶 ·o 𝑦 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) )
33 oveq2 ⊢ ( 𝐴 = 𝑦 → ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝑦 ) )
34 33 eleq1d ⊢ ( 𝐴 = 𝑦 → ( ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ↔ ( 𝐶 ·o 𝑦 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
35 32 34 syl5ibrcom ⊢ ( ( ( ( 𝐶 ·o 𝑦 ) ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 = 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
36 35 adantrr ⊢ ( ( ( ( 𝐶 ·o 𝑦 ) ∈ On ∧ 𝐶 ∈ On ) ∧ ( ∅ ∈ 𝐶 ∧ ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) ) ) → ( 𝐴 = 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
37 30 36 jaod ⊢ ( ( ( ( 𝐶 ·o 𝑦 ) ∈ On ∧ 𝐶 ∈ On ) ∧ ( ∅ ∈ 𝐶 ∧ ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) ) ) → ( ( 𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ) → ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
38 25 37 sylan ⊢ ( ( ( 𝐶 ∈ On ∧ 𝑦 ∈ On ) ∧ ( ∅ ∈ 𝐶 ∧ ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) ) ) → ( ( 𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ) → ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
39 22 38 syl5 ⊢ ( ( ( 𝐶 ∈ On ∧ 𝑦 ∈ On ) ∧ ( ∅ ∈ 𝐶 ∧ ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) ) ) → ( 𝐴 ∈ suc 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
40 omsuc ⊢ ( ( 𝐶 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐶 ·o suc 𝑦 ) = ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) )
41 40 eleq2d ⊢ ( ( 𝐶 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝑦 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
42 41 adantr ⊢ ( ( ( 𝐶 ∈ On ∧ 𝑦 ∈ On ) ∧ ( ∅ ∈ 𝐶 ∧ ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) ) ) → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝑦 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
43 39 42 sylibrd ⊢ ( ( ( 𝐶 ∈ On ∧ 𝑦 ∈ On ) ∧ ( ∅ ∈ 𝐶 ∧ ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) ) ) → ( 𝐴 ∈ suc 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝑦 ) ) )
44 43 exp43 ⊢ ( 𝐶 ∈ On → ( 𝑦 ∈ On → ( ∅ ∈ 𝐶 → ( ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) → ( 𝐴 ∈ suc 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝑦 ) ) ) ) ) )
45 44 com12 ⊢ ( 𝑦 ∈ On → ( 𝐶 ∈ On → ( ∅ ∈ 𝐶 → ( ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) → ( 𝐴 ∈ suc 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝑦 ) ) ) ) ) )
46 45 adantld ⊢ ( 𝑦 ∈ On → ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( ∅ ∈ 𝐶 → ( ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) → ( 𝐴 ∈ suc 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝑦 ) ) ) ) ) )
47 46 impd ⊢ ( 𝑦 ∈ On → ( ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) → ( 𝐴 ∈ suc 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝑦 ) ) ) ) )
48 id ⊢ ( ( 𝐶 ∈ On ∧ Lim 𝑥 ) → ( 𝐶 ∈ On ∧ Lim 𝑥 ) )
49 48 ad2ant2r ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) ∧ ( Lim 𝑥 ∧ ∅ ∈ 𝐶 ) ) → ( 𝐶 ∈ On ∧ Lim 𝑥 ) )
50 limsuc ⊢ ( Lim 𝑥 → ( 𝐴 ∈ 𝑥 ↔ suc 𝐴 ∈ 𝑥 ) )
51 50 biimpa ⊢ ( ( Lim 𝑥 ∧ 𝐴 ∈ 𝑥 ) → suc 𝐴 ∈ 𝑥 )
52 oveq2 ⊢ ( 𝑦 = suc 𝐴 → ( 𝐶 ·o 𝑦 ) = ( 𝐶 ·o suc 𝐴 ) )
53 52 ssiun2s ⊢ ( suc 𝐴 ∈ 𝑥 → ( 𝐶 ·o suc 𝐴 ) ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐶 ·o 𝑦 ) )
54 51 53 syl ⊢ ( ( Lim 𝑥 ∧ 𝐴 ∈ 𝑥 ) → ( 𝐶 ·o suc 𝐴 ) ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐶 ·o 𝑦 ) )
55 54 adantll ⊢ ( ( ( 𝐶 ∈ On ∧ Lim 𝑥 ) ∧ 𝐴 ∈ 𝑥 ) → ( 𝐶 ·o suc 𝐴 ) ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐶 ·o 𝑦 ) )
56 vex ⊢ 𝑥 ∈ V
57 omlim ⊢ ( ( 𝐶 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( 𝐶 ·o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐶 ·o 𝑦 ) )
58 56 57 mpanr1 ⊢ ( ( 𝐶 ∈ On ∧ Lim 𝑥 ) → ( 𝐶 ·o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐶 ·o 𝑦 ) )
59 58 adantr ⊢ ( ( ( 𝐶 ∈ On ∧ Lim 𝑥 ) ∧ 𝐴 ∈ 𝑥 ) → ( 𝐶 ·o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐶 ·o 𝑦 ) )
60 55 59 sseqtrrd ⊢ ( ( ( 𝐶 ∈ On ∧ Lim 𝑥 ) ∧ 𝐴 ∈ 𝑥 ) → ( 𝐶 ·o suc 𝐴 ) ⊆ ( 𝐶 ·o 𝑥 ) )
61 49 60 sylan ⊢ ( ( ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) ∧ ( Lim 𝑥 ∧ ∅ ∈ 𝐶 ) ) ∧ 𝐴 ∈ 𝑥 ) → ( 𝐶 ·o suc 𝐴 ) ⊆ ( 𝐶 ·o 𝑥 ) )
62 omcl ⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐶 ·o 𝐴 ) ∈ On )
63 oaord1 ⊢ ( ( ( 𝐶 ·o 𝐴 ) ∈ On ∧ 𝐶 ∈ On ) → ( ∅ ∈ 𝐶 ↔ ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝐴 ) +o 𝐶 ) ) )
64 62 63 sylan ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) ∧ 𝐶 ∈ On ) → ( ∅ ∈ 𝐶 ↔ ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝐴 ) +o 𝐶 ) ) )
65 64 anabss1 ⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( ∅ ∈ 𝐶 ↔ ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝐴 ) +o 𝐶 ) ) )
66 65 biimpa ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝐴 ) +o 𝐶 ) )
67 omsuc ⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐶 ·o suc 𝐴 ) = ( ( 𝐶 ·o 𝐴 ) +o 𝐶 ) )
68 67 adantr ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐶 ·o suc 𝐴 ) = ( ( 𝐶 ·o 𝐴 ) +o 𝐶 ) )
69 66 68 eleqtrrd ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝐴 ) )
70 69 adantrl ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) ∧ ( Lim 𝑥 ∧ ∅ ∈ 𝐶 ) ) → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝐴 ) )
71 70 adantr ⊢ ( ( ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) ∧ ( Lim 𝑥 ∧ ∅ ∈ 𝐶 ) ) ∧ 𝐴 ∈ 𝑥 ) → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝐴 ) )
72 61 71 sseldd ⊢ ( ( ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) ∧ ( Lim 𝑥 ∧ ∅ ∈ 𝐶 ) ) ∧ 𝐴 ∈ 𝑥 ) → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) )
73 72 exp53 ⊢ ( 𝐶 ∈ On → ( 𝐴 ∈ On → ( Lim 𝑥 → ( ∅ ∈ 𝐶 → ( 𝐴 ∈ 𝑥 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ) ) ) ) )
74 73 com13 ⊢ ( Lim 𝑥 → ( 𝐴 ∈ On → ( 𝐶 ∈ On → ( ∅ ∈ 𝐶 → ( 𝐴 ∈ 𝑥 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ) ) ) ) )
75 74 imp4c ⊢ ( Lim 𝑥 → ( ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ 𝑥 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ) ) )
76 75 a1dd ⊢ ( Lim 𝑥 → ( ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) → ( 𝐴 ∈ 𝑥 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ) ) ) )
77 6 10 14 18 21 47 76 tfinds3 ⊢ ( 𝐵 ∈ On → ( ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) )
78 77 com23 ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → ( ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) )
79 78 exp4a ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( ∅ ∈ 𝐶 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) ) )
80 79 exp4a ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ On → ( 𝐶 ∈ On → ( ∅ ∈ 𝐶 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) ) ) )
81 2 80 mpdd ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → ( 𝐶 ∈ On → ( ∅ ∈ 𝐶 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) ) )
82 81 com34 ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → ( ∅ ∈ 𝐶 → ( 𝐶 ∈ On → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) ) )
83 82 com24 ⊢ ( 𝐵 ∈ On → ( 𝐶 ∈ On → ( ∅ ∈ 𝐶 → ( 𝐴 ∈ 𝐵 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) ) )
84 83 imp31 ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )