Theorem oeoelem

Description: Lemma for oeoe . (Contributed by Eric Schmidt, 26-May-2009)

	Ref	Expression
Hypotheses	oeoelem.1	⊢ 𝐴 ∈ On
	oeoelem.2	⊢ ∅ ∈ 𝐴
Assertion	oeoelem	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ↑o 𝐵 ) ↑o 𝐶 ) = ( 𝐴 ↑o ( 𝐵 ·o 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oeoelem.1	⊢ 𝐴 ∈ On
2		oeoelem.2	⊢ ∅ ∈ 𝐴
3		oveq2	⊢ ( 𝑥 = ∅ → ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑥 ) = ( ( 𝐴 ↑o 𝐵 ) ↑o ∅ ) )
4		oveq2	⊢ ( 𝑥 = ∅ → ( 𝐵 ·o 𝑥 ) = ( 𝐵 ·o ∅ ) )
5	4	oveq2d	⊢ ( 𝑥 = ∅ → ( 𝐴 ↑o ( 𝐵 ·o 𝑥 ) ) = ( 𝐴 ↑o ( 𝐵 ·o ∅ ) ) )
6	3 5	eqeq12d	⊢ ( 𝑥 = ∅ → ( ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑥 ) = ( 𝐴 ↑o ( 𝐵 ·o 𝑥 ) ) ↔ ( ( 𝐴 ↑o 𝐵 ) ↑o ∅ ) = ( 𝐴 ↑o ( 𝐵 ·o ∅ ) ) ) )
7		oveq2	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑥 ) = ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑦 ) )
8		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐵 ·o 𝑥 ) = ( 𝐵 ·o 𝑦 ) )
9	8	oveq2d	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ↑o ( 𝐵 ·o 𝑥 ) ) = ( 𝐴 ↑o ( 𝐵 ·o 𝑦 ) ) )
10	7 9	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑥 ) = ( 𝐴 ↑o ( 𝐵 ·o 𝑥 ) ) ↔ ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑦 ) = ( 𝐴 ↑o ( 𝐵 ·o 𝑦 ) ) ) )
11		oveq2	⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑥 ) = ( ( 𝐴 ↑o 𝐵 ) ↑o suc 𝑦 ) )
12		oveq2	⊢ ( 𝑥 = suc 𝑦 → ( 𝐵 ·o 𝑥 ) = ( 𝐵 ·o suc 𝑦 ) )
13	12	oveq2d	⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ↑o ( 𝐵 ·o 𝑥 ) ) = ( 𝐴 ↑o ( 𝐵 ·o suc 𝑦 ) ) )
14	11 13	eqeq12d	⊢ ( 𝑥 = suc 𝑦 → ( ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑥 ) = ( 𝐴 ↑o ( 𝐵 ·o 𝑥 ) ) ↔ ( ( 𝐴 ↑o 𝐵 ) ↑o suc 𝑦 ) = ( 𝐴 ↑o ( 𝐵 ·o suc 𝑦 ) ) ) )
15		oveq2	⊢ ( 𝑥 = 𝐶 → ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑥 ) = ( ( 𝐴 ↑o 𝐵 ) ↑o 𝐶 ) )
16		oveq2	⊢ ( 𝑥 = 𝐶 → ( 𝐵 ·o 𝑥 ) = ( 𝐵 ·o 𝐶 ) )
17	16	oveq2d	⊢ ( 𝑥 = 𝐶 → ( 𝐴 ↑o ( 𝐵 ·o 𝑥 ) ) = ( 𝐴 ↑o ( 𝐵 ·o 𝐶 ) ) )
18	15 17	eqeq12d	⊢ ( 𝑥 = 𝐶 → ( ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑥 ) = ( 𝐴 ↑o ( 𝐵 ·o 𝑥 ) ) ↔ ( ( 𝐴 ↑o 𝐵 ) ↑o 𝐶 ) = ( 𝐴 ↑o ( 𝐵 ·o 𝐶 ) ) ) )
19		oecl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o 𝐵 ) ∈ On )
20	1 19	mpan	⊢ ( 𝐵 ∈ On → ( 𝐴 ↑o 𝐵 ) ∈ On )
21		oe0	⊢ ( ( 𝐴 ↑o 𝐵 ) ∈ On → ( ( 𝐴 ↑o 𝐵 ) ↑o ∅ ) = 1o )
22	20 21	syl	⊢ ( 𝐵 ∈ On → ( ( 𝐴 ↑o 𝐵 ) ↑o ∅ ) = 1o )
23		om0	⊢ ( 𝐵 ∈ On → ( 𝐵 ·o ∅ ) = ∅ )
24	23	oveq2d	⊢ ( 𝐵 ∈ On → ( 𝐴 ↑o ( 𝐵 ·o ∅ ) ) = ( 𝐴 ↑o ∅ ) )
25		oe0	⊢ ( 𝐴 ∈ On → ( 𝐴 ↑o ∅ ) = 1o )
26	1 25	ax-mp	⊢ ( 𝐴 ↑o ∅ ) = 1o
27	24 26	eqtrdi	⊢ ( 𝐵 ∈ On → ( 𝐴 ↑o ( 𝐵 ·o ∅ ) ) = 1o )
28	22 27	eqtr4d	⊢ ( 𝐵 ∈ On → ( ( 𝐴 ↑o 𝐵 ) ↑o ∅ ) = ( 𝐴 ↑o ( 𝐵 ·o ∅ ) ) )
29		oveq1	⊢ ( ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑦 ) = ( 𝐴 ↑o ( 𝐵 ·o 𝑦 ) ) → ( ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑦 ) ·o ( 𝐴 ↑o 𝐵 ) ) = ( ( 𝐴 ↑o ( 𝐵 ·o 𝑦 ) ) ·o ( 𝐴 ↑o 𝐵 ) ) )
30		oesuc	⊢ ( ( ( 𝐴 ↑o 𝐵 ) ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐴 ↑o 𝐵 ) ↑o suc 𝑦 ) = ( ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑦 ) ·o ( 𝐴 ↑o 𝐵 ) ) )
31	20 30	sylan	⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐴 ↑o 𝐵 ) ↑o suc 𝑦 ) = ( ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑦 ) ·o ( 𝐴 ↑o 𝐵 ) ) )
32		omsuc	⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 ·o suc 𝑦 ) = ( ( 𝐵 ·o 𝑦 ) +o 𝐵 ) )
33	32	oveq2d	⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o ( 𝐵 ·o suc 𝑦 ) ) = ( 𝐴 ↑o ( ( 𝐵 ·o 𝑦 ) +o 𝐵 ) ) )
34		omcl	⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 ·o 𝑦 ) ∈ On )
35		oeoa	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ·o 𝑦 ) ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o ( ( 𝐵 ·o 𝑦 ) +o 𝐵 ) ) = ( ( 𝐴 ↑o ( 𝐵 ·o 𝑦 ) ) ·o ( 𝐴 ↑o 𝐵 ) ) )
36	1 35	mp3an1	⊢ ( ( ( 𝐵 ·o 𝑦 ) ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o ( ( 𝐵 ·o 𝑦 ) +o 𝐵 ) ) = ( ( 𝐴 ↑o ( 𝐵 ·o 𝑦 ) ) ·o ( 𝐴 ↑o 𝐵 ) ) )
37	34 36	sylan	⊢ ( ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o ( ( 𝐵 ·o 𝑦 ) +o 𝐵 ) ) = ( ( 𝐴 ↑o ( 𝐵 ·o 𝑦 ) ) ·o ( 𝐴 ↑o 𝐵 ) ) )
38	37	anabss1	⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o ( ( 𝐵 ·o 𝑦 ) +o 𝐵 ) ) = ( ( 𝐴 ↑o ( 𝐵 ·o 𝑦 ) ) ·o ( 𝐴 ↑o 𝐵 ) ) )
39	33 38	eqtrd	⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o ( 𝐵 ·o suc 𝑦 ) ) = ( ( 𝐴 ↑o ( 𝐵 ·o 𝑦 ) ) ·o ( 𝐴 ↑o 𝐵 ) ) )
40	31 39	eqeq12d	⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( ( ( 𝐴 ↑o 𝐵 ) ↑o suc 𝑦 ) = ( 𝐴 ↑o ( 𝐵 ·o suc 𝑦 ) ) ↔ ( ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑦 ) ·o ( 𝐴 ↑o 𝐵 ) ) = ( ( 𝐴 ↑o ( 𝐵 ·o 𝑦 ) ) ·o ( 𝐴 ↑o 𝐵 ) ) ) )
41	29 40	imbitrrid	⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑦 ) = ( 𝐴 ↑o ( 𝐵 ·o 𝑦 ) ) → ( ( 𝐴 ↑o 𝐵 ) ↑o suc 𝑦 ) = ( 𝐴 ↑o ( 𝐵 ·o suc 𝑦 ) ) ) )
42	41	expcom	⊢ ( 𝑦 ∈ On → ( 𝐵 ∈ On → ( ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑦 ) = ( 𝐴 ↑o ( 𝐵 ·o 𝑦 ) ) → ( ( 𝐴 ↑o 𝐵 ) ↑o suc 𝑦 ) = ( 𝐴 ↑o ( 𝐵 ·o suc 𝑦 ) ) ) ) )
43		iuneq2	⊢ ( ∀ 𝑦 ∈ 𝑥 ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑦 ) = ( 𝐴 ↑o ( 𝐵 ·o 𝑦 ) ) → ∪ 𝑦 ∈ 𝑥 ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑦 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o ( 𝐵 ·o 𝑦 ) ) )
44		vex	⊢ 𝑥 ∈ V
45		oen0	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ∅ ∈ ( 𝐴 ↑o 𝐵 ) )
46	2 45	mpan2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ∅ ∈ ( 𝐴 ↑o 𝐵 ) )
47		oelim	⊢ ( ( ( ( 𝐴 ↑o 𝐵 ) ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ∧ ∅ ∈ ( 𝐴 ↑o 𝐵 ) ) → ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑦 ) )
48	19 47	sylanl1	⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ∧ ∅ ∈ ( 𝐴 ↑o 𝐵 ) ) → ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑦 ) )
49	46 48	mpidan	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑦 ) )
50	1 49	mpanl1	⊢ ( ( 𝐵 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑦 ) )
51	44 50	mpanr1	⊢ ( ( 𝐵 ∈ On ∧ Lim 𝑥 ) → ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑦 ) )
52		omlim	⊢ ( ( 𝐵 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( 𝐵 ·o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐵 ·o 𝑦 ) )
53	44 52	mpanr1	⊢ ( ( 𝐵 ∈ On ∧ Lim 𝑥 ) → ( 𝐵 ·o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐵 ·o 𝑦 ) )
54	53	oveq2d	⊢ ( ( 𝐵 ∈ On ∧ Lim 𝑥 ) → ( 𝐴 ↑o ( 𝐵 ·o 𝑥 ) ) = ( 𝐴 ↑o ∪ 𝑦 ∈ 𝑥 ( 𝐵 ·o 𝑦 ) ) )
55		limord	⊢ ( Lim 𝑥 → Ord 𝑥 )
56		ordelon	⊢ ( ( Ord 𝑥 ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On )
57	55 56	sylan	⊢ ( ( Lim 𝑥 ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On )
58	57 34	sylan2	⊢ ( ( 𝐵 ∈ On ∧ ( Lim 𝑥 ∧ 𝑦 ∈ 𝑥 ) ) → ( 𝐵 ·o 𝑦 ) ∈ On )
59	58	anassrs	⊢ ( ( ( 𝐵 ∈ On ∧ Lim 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐵 ·o 𝑦 ) ∈ On )
60	59	ralrimiva	⊢ ( ( 𝐵 ∈ On ∧ Lim 𝑥 ) → ∀ 𝑦 ∈ 𝑥 ( 𝐵 ·o 𝑦 ) ∈ On )
61		0ellim	⊢ ( Lim 𝑥 → ∅ ∈ 𝑥 )
62	61	ne0d	⊢ ( Lim 𝑥 → 𝑥 ≠ ∅ )
63	62	adantl	⊢ ( ( 𝐵 ∈ On ∧ Lim 𝑥 ) → 𝑥 ≠ ∅ )
64		vex	⊢ 𝑤 ∈ V
65		oelim	⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝑤 ∈ V ∧ Lim 𝑤 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝑤 ) = ∪ 𝑧 ∈ 𝑤 ( 𝐴 ↑o 𝑧 ) )
66	2 65	mpan2	⊢ ( ( 𝐴 ∈ On ∧ ( 𝑤 ∈ V ∧ Lim 𝑤 ) ) → ( 𝐴 ↑o 𝑤 ) = ∪ 𝑧 ∈ 𝑤 ( 𝐴 ↑o 𝑧 ) )
67	1 66	mpan	⊢ ( ( 𝑤 ∈ V ∧ Lim 𝑤 ) → ( 𝐴 ↑o 𝑤 ) = ∪ 𝑧 ∈ 𝑤 ( 𝐴 ↑o 𝑧 ) )
68	64 67	mpan	⊢ ( Lim 𝑤 → ( 𝐴 ↑o 𝑤 ) = ∪ 𝑧 ∈ 𝑤 ( 𝐴 ↑o 𝑧 ) )
69		oewordi	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝑧 ⊆ 𝑤 → ( 𝐴 ↑o 𝑧 ) ⊆ ( 𝐴 ↑o 𝑤 ) ) )
70	2 69	mpan2	⊢ ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ∧ 𝐴 ∈ On ) → ( 𝑧 ⊆ 𝑤 → ( 𝐴 ↑o 𝑧 ) ⊆ ( 𝐴 ↑o 𝑤 ) ) )
71	1 70	mp3an3	⊢ ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) → ( 𝑧 ⊆ 𝑤 → ( 𝐴 ↑o 𝑧 ) ⊆ ( 𝐴 ↑o 𝑤 ) ) )
72	71	3impia	⊢ ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ∧ 𝑧 ⊆ 𝑤 ) → ( 𝐴 ↑o 𝑧 ) ⊆ ( 𝐴 ↑o 𝑤 ) )
73	68 72	onoviun	⊢ ( ( 𝑥 ∈ V ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐵 ·o 𝑦 ) ∈ On ∧ 𝑥 ≠ ∅ ) → ( 𝐴 ↑o ∪ 𝑦 ∈ 𝑥 ( 𝐵 ·o 𝑦 ) ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o ( 𝐵 ·o 𝑦 ) ) )
74	44 60 63 73	mp3an2i	⊢ ( ( 𝐵 ∈ On ∧ Lim 𝑥 ) → ( 𝐴 ↑o ∪ 𝑦 ∈ 𝑥 ( 𝐵 ·o 𝑦 ) ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o ( 𝐵 ·o 𝑦 ) ) )
75	54 74	eqtrd	⊢ ( ( 𝐵 ∈ On ∧ Lim 𝑥 ) → ( 𝐴 ↑o ( 𝐵 ·o 𝑥 ) ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o ( 𝐵 ·o 𝑦 ) ) )
76	51 75	eqeq12d	⊢ ( ( 𝐵 ∈ On ∧ Lim 𝑥 ) → ( ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑥 ) = ( 𝐴 ↑o ( 𝐵 ·o 𝑥 ) ) ↔ ∪ 𝑦 ∈ 𝑥 ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑦 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o ( 𝐵 ·o 𝑦 ) ) ) )
77	43 76	imbitrrid	⊢ ( ( 𝐵 ∈ On ∧ Lim 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑦 ) = ( 𝐴 ↑o ( 𝐵 ·o 𝑦 ) ) → ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑥 ) = ( 𝐴 ↑o ( 𝐵 ·o 𝑥 ) ) ) )
78	77	expcom	⊢ ( Lim 𝑥 → ( 𝐵 ∈ On → ( ∀ 𝑦 ∈ 𝑥 ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑦 ) = ( 𝐴 ↑o ( 𝐵 ·o 𝑦 ) ) → ( ( 𝐴 ↑o 𝐵 ) ↑o 𝑥 ) = ( 𝐴 ↑o ( 𝐵 ·o 𝑥 ) ) ) ) )
79	6 10 14 18 28 42 78	tfinds3	⊢ ( 𝐶 ∈ On → ( 𝐵 ∈ On → ( ( 𝐴 ↑o 𝐵 ) ↑o 𝐶 ) = ( 𝐴 ↑o ( 𝐵 ·o 𝐶 ) ) ) )
80	79	impcom	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ↑o 𝐵 ) ↑o 𝐶 ) = ( 𝐴 ↑o ( 𝐵 ·o 𝐶 ) ) )