Theorem oev 8219

Description: Value of ordinal exponentiation. (Contributed by NM, 30-Dec-2004.) (Revised by Mario Carneiro, 23-Aug-2014.)

Assertion

Ref	Expression
oev	⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑o 𝐵) = if(𝐴 = ∅, (1o ∖ 𝐵), (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵)))

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem oev

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2740	. . 3 ⊢ (𝑦 = 𝐴 → (𝑦 = ∅ ↔ 𝐴 = ∅))
2		oveq2 7199	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ·o 𝑦) = (𝑥 ·o 𝐴))
3	2	mpteq2dv 5136	. . . . 5 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ V ↦ (𝑥 ·o 𝑦)) = (𝑥 ∈ V ↦ (𝑥 ·o 𝐴)))
4		rdgeq1 8125	. . . . 5 ⊢ ((𝑥 ∈ V ↦ (𝑥 ·o 𝑦)) = (𝑥 ∈ V ↦ (𝑥 ·o 𝐴)) → rec((𝑥 ∈ V ↦ (𝑥 ·o 𝑦)), 1o) = rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o))
5	3, 4	syl 17	. . . 4 ⊢ (𝑦 = 𝐴 → rec((𝑥 ∈ V ↦ (𝑥 ·o 𝑦)), 1o) = rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o))
6	5	fveq1d 6697	. . 3 ⊢ (𝑦 = 𝐴 → (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝑦)), 1o)‘𝑧) = (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝑧))
7	1, 6	ifbieq2d 4451	. 2 ⊢ (𝑦 = 𝐴 → if(𝑦 = ∅, (1o ∖ 𝑧), (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝑦)), 1o)‘𝑧)) = if(𝐴 = ∅, (1o ∖ 𝑧), (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝑧)))
8		difeq2 4017	. . 3 ⊢ (𝑧 = 𝐵 → (1o ∖ 𝑧) = (1o ∖ 𝐵))
9		fveq2 6695	. . 3 ⊢ (𝑧 = 𝐵 → (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝑧) = (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵))
10	8, 9	ifeq12d 4446	. 2 ⊢ (𝑧 = 𝐵 → if(𝐴 = ∅, (1o ∖ 𝑧), (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝑧)) = if(𝐴 = ∅, (1o ∖ 𝐵), (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵)))
11		df-oexp 8186	. 2 ⊢ ↑o = (𝑦 ∈ On, 𝑧 ∈ On ↦ if(𝑦 = ∅, (1o ∖ 𝑧), (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝑦)), 1o)‘𝑧)))
12		1oex 8193	. . . 4 ⊢ 1o ∈ V
13	12	difexi 5206	. . 3 ⊢ (1o ∖ 𝐵) ∈ V
14		fvex 6708	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) ∈ V
15	13, 14	ifex 4475	. 2 ⊢ if(𝐴 = ∅, (1o ∖ 𝐵), (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵)) ∈ V
16	7, 10, 11, 15	ovmpo 7347	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑o 𝐵) = if(𝐴 = ∅, (1o ∖ 𝐵), (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵)))

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2112  Vcvv 3398   ∖ cdif 3850  ∅c0 4223  ifcif 4425   ↦ cmpt 5120  Oncon0 6191  ‘cfv 6358  (class class class)co 7191  reccrdg 8123  1_oc1o 8173   ·_o comu 8178   ↑_o coe 8179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6140  df-suc 6197  df-iota 6316  df-fun 6360  df-fv 6366  df-ov 7194  df-oprab 7195  df-mpo 7196  df-wrecs 8025  df-recs 8086  df-rdg 8124  df-1o 8180  df-oexp 8186

This theorem is referenced by:  oevn0  8220  oe0m  8223