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 𝐵 ) ) )