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

Metamath Proof Explorer

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