Theorem rdg0 6388

Description: The initial value of the recursive definition generator. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)

Hypothesis

Ref	Expression
rdg.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
rdg0	⊢ (rec(𝐹, 𝐴)‘∅) = 𝐴

Proof of Theorem rdg0

Dummy variables 𝑥 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0ex 4131	. . . . 5 ⊢ ∅ ∈ V
2		dmeq 4828	. . . . . . . 8 ⊢ (𝑔 = ∅ → dom 𝑔 = dom ∅)
3		fveq1 5515	. . . . . . . . 9 ⊢ (𝑔 = ∅ → (𝑔‘𝑥) = (∅‘𝑥))
4	3	fveq2d 5520	. . . . . . . 8 ⊢ (𝑔 = ∅ → (𝐹‘(𝑔‘𝑥)) = (𝐹‘(∅‘𝑥)))
5	2, 4	iuneq12d 3911	. . . . . . 7 ⊢ (𝑔 = ∅ → ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)) = ∪ 𝑥 ∈ dom ∅(𝐹‘(∅‘𝑥)))
6	5	uneq2d 3290	. . . . . 6 ⊢ (𝑔 = ∅ → (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))) = (𝐴 ∪ ∪ 𝑥 ∈ dom ∅(𝐹‘(∅‘𝑥))))
7		eqid 2177	. . . . . 6 ⊢ (𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)))) = (𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))
8		rdg.1	. . . . . . 7 ⊢ 𝐴 ∈ V
9		dm0 4842	. . . . . . . . . 10 ⊢ dom ∅ = ∅
10		iuneq1 3900	. . . . . . . . . 10 ⊢ (dom ∅ = ∅ → ∪ 𝑥 ∈ dom ∅(𝐹‘(∅‘𝑥)) = ∪ 𝑥 ∈ ∅ (𝐹‘(∅‘𝑥)))
11	9, 10	ax-mp 5	. . . . . . . . 9 ⊢ ∪ 𝑥 ∈ dom ∅(𝐹‘(∅‘𝑥)) = ∪ 𝑥 ∈ ∅ (𝐹‘(∅‘𝑥))
12		0iun 3945	. . . . . . . . 9 ⊢ ∪ 𝑥 ∈ ∅ (𝐹‘(∅‘𝑥)) = ∅
13	11, 12	eqtri 2198	. . . . . . . 8 ⊢ ∪ 𝑥 ∈ dom ∅(𝐹‘(∅‘𝑥)) = ∅
14	13, 1	eqeltri 2250	. . . . . . 7 ⊢ ∪ 𝑥 ∈ dom ∅(𝐹‘(∅‘𝑥)) ∈ V
15	8, 14	unex 4442	. . . . . 6 ⊢ (𝐴 ∪ ∪ 𝑥 ∈ dom ∅(𝐹‘(∅‘𝑥))) ∈ V
16	6, 7, 15	fvmpt 5594	. . . . 5 ⊢ (∅ ∈ V → ((𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘∅) = (𝐴 ∪ ∪ 𝑥 ∈ dom ∅(𝐹‘(∅‘𝑥))))
17	1, 16	ax-mp 5	. . . 4 ⊢ ((𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘∅) = (𝐴 ∪ ∪ 𝑥 ∈ dom ∅(𝐹‘(∅‘𝑥)))
18	17, 15	eqeltri 2250	. . 3 ⊢ ((𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘∅) ∈ V
19		df-irdg 6371	. . . 4 ⊢ rec(𝐹, 𝐴) = recs((𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)))))
20	19	tfr0 6324	. . 3 ⊢ (((𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘∅) ∈ V → (rec(𝐹, 𝐴)‘∅) = ((𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘∅))
21	18, 20	ax-mp 5	. 2 ⊢ (rec(𝐹, 𝐴)‘∅) = ((𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘∅)
22	13	uneq2i 3287	. . . 4 ⊢ (𝐴 ∪ ∪ 𝑥 ∈ dom ∅(𝐹‘(∅‘𝑥))) = (𝐴 ∪ ∅)
23	17, 22	eqtri 2198	. . 3 ⊢ ((𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘∅) = (𝐴 ∪ ∅)
24		un0 3457	. . 3 ⊢ (𝐴 ∪ ∅) = 𝐴
25	23, 24	eqtri 2198	. 2 ⊢ ((𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘∅) = 𝐴
26	21, 25	eqtri 2198	1 ⊢ (rec(𝐹, 𝐴)‘∅) = 𝐴

Syntax hints:   = wceq 1353   ∈ wcel 2148  Vcvv 2738   ∪ cun 3128  ∅c0 3423  ∪ ciun 3887   ↦ cmpt 4065  dom cdm 4627  ‘cfv 5217  reccrdg 6370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-nul 4130  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2740  df-sbc 2964  df-csb 3059  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-tr 4103  df-id 4294  df-iord 4367  df-on 4369  df-suc 4372  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-res 4639  df-iota 5179  df-fun 5219  df-fn 5220  df-fv 5225  df-recs 6306  df-irdg 6371

This theorem is referenced by:  rdg0g  6389  om0  6459