Theorem oeeu

Description: The division algorithm for ordinal exponentiation. (Contributed by Mario Carneiro, 25-May-2015)

	Ref	Expression
Assertion	oeeu	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ∃! 𝑤 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( 𝐴 ∖ 1o ) ∃ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } = ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) }
2	1	oeeulem	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ( ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ∈ On ∧ ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ⊆ 𝐵 ∧ 𝐵 ∈ ( 𝐴 ↑o suc ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ) )
3	2	simp1d	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ∈ On )
4		fvexd	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ( 1st ‘ ( ℩ 𝑑 ∃ 𝑏 ∈ On ∃ 𝑐 ∈ ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ·o 𝑏 ) +o 𝑐 ) = 𝐵 ) ) ) ∈ V )
5		fvexd	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ( 2nd ‘ ( ℩ 𝑑 ∃ 𝑏 ∈ On ∃ 𝑐 ∈ ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ·o 𝑏 ) +o 𝑐 ) = 𝐵 ) ) ) ∈ V )
6		eqid	⊢ ( ℩ 𝑑 ∃ 𝑏 ∈ On ∃ 𝑐 ∈ ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ·o 𝑏 ) +o 𝑐 ) = 𝐵 ) ) = ( ℩ 𝑑 ∃ 𝑏 ∈ On ∃ 𝑐 ∈ ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ·o 𝑏 ) +o 𝑐 ) = 𝐵 ) )
7		eqid	⊢ ( 1st ‘ ( ℩ 𝑑 ∃ 𝑏 ∈ On ∃ 𝑐 ∈ ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ·o 𝑏 ) +o 𝑐 ) = 𝐵 ) ) ) = ( 1st ‘ ( ℩ 𝑑 ∃ 𝑏 ∈ On ∃ 𝑐 ∈ ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ·o 𝑏 ) +o 𝑐 ) = 𝐵 ) ) )
8		eqid	⊢ ( 2nd ‘ ( ℩ 𝑑 ∃ 𝑏 ∈ On ∃ 𝑐 ∈ ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ·o 𝑏 ) +o 𝑐 ) = 𝐵 ) ) ) = ( 2nd ‘ ( ℩ 𝑑 ∃ 𝑏 ∈ On ∃ 𝑐 ∈ ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ·o 𝑏 ) +o 𝑐 ) = 𝐵 ) ) )
9	1 6 7 8	oeeui	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ∧ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ) ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ↔ ( 𝑥 = ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ∧ 𝑦 = ( 1st ‘ ( ℩ 𝑑 ∃ 𝑏 ∈ On ∃ 𝑐 ∈ ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ·o 𝑏 ) +o 𝑐 ) = 𝐵 ) ) ) ∧ 𝑧 = ( 2nd ‘ ( ℩ 𝑑 ∃ 𝑏 ∈ On ∃ 𝑐 ∈ ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( ( 𝐴 ↑o ∪ ∩ { 𝑎 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑎 ) } ) ·o 𝑏 ) +o 𝑐 ) = 𝐵 ) ) ) ) ) )
10	3 4 5 9	euotd	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ∃! 𝑤 ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ∧ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ) ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) )
11		df-3an	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ∧ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ) ↔ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ) ∧ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ) )
12	11	biancomi	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ∧ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ) ↔ ( 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ) ) )
13	12	anbi1i	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ∧ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ) ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ↔ ( ( 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ) ) ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) )
14	13	anbi2i	⊢ ( ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ∧ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ) ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) ↔ ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ) ) ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) )
15		an12	⊢ ( ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ) ) ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) ↔ ( ( 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ) ) ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) )
16		anass	⊢ ( ( ( 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ) ) ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) ↔ ( 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ) ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) ) )
17	14 15 16	3bitri	⊢ ( ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ∧ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ) ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) ↔ ( 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ) ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) ) )
18	17	exbii	⊢ ( ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ∧ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ) ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) ↔ ∃ 𝑧 ( 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ) ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) ) )
19		df-rex	⊢ ( ∃ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ) ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) ↔ ∃ 𝑧 ( 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ) ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) ) )
20		r19.42v	⊢ ( ∃ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ) ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) ↔ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ) ∧ ∃ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) )
21	18 19 20	3bitr2i	⊢ ( ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ∧ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ) ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) ↔ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ) ∧ ∃ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) )
22	21	2exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ∧ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ) ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ) ∧ ∃ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) )
23		r2ex	⊢ ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( 𝐴 ∖ 1o ) ∃ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ) ∧ ∃ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) )
24	22 23	bitr4i	⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ∧ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ) ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) ↔ ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( 𝐴 ∖ 1o ) ∃ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) )
25	24	eubii	⊢ ( ∃! 𝑤 ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ( 𝐴 ∖ 1o ) ∧ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ) ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) ↔ ∃! 𝑤 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( 𝐴 ∖ 1o ) ∃ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) )
26	10 25	sylib	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ∃! 𝑤 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( 𝐴 ∖ 1o ) ∃ 𝑧 ∈ ( 𝐴 ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) )