Theorem rdglim2 4007

Description: The value of the recursive definition generator at a limit ordinal, in terms of the union of all smaller values.

Assertion

Ref	Expression
rdglim2	⊢ ((B ∈ C ⋀ Lim B) → (rec(F, A) ‘B) = ∪{y∣∃x ∈ B y = (rec(F, A) ‘x)})

Distinct variable groups:   x,y,A   x,B,y   x,F,y

Proof of Theorem rdglim2

Step	Hyp	Ref	Expression
1		rdglim 4006	. 2 ⊢ ((B ∈ C ⋀ Lim B) → (rec(F, A) ‘B) = ∪(rec(F, A) “ B))
2		limord 3085	. . . . . . . . . . 11 ⊢ (Lim B → Ord B)
3		ordelord 3027	. . . . . . . . . . . . 13 ⊢ ((Ord B ⋀ x ∈ B) → Ord x)
4	3	ex 380	. . . . . . . . . . . 12 ⊢ (Ord B → (x ∈ B → Ord x))
5		visset 1860	. . . . . . . . . . . . 13 ⊢ x ∈ V
6	5	elon 3014	. . . . . . . . . . . 12 ⊢ (x ∈ On ↔ Ord x)
7	4, 6	syl6ibr 220	. . . . . . . . . . 11 ⊢ (Ord B → (x ∈ B → x ∈ On))
8	2, 7	syl 10	. . . . . . . . . 10 ⊢ (Lim B → (x ∈ B → x ∈ On))
9		rdgfnon 3997	. . . . . . . . . . . 12 ⊢ rec(F, A) Fn On
10		visset 1860	. . . . . . . . . . . . 13 ⊢ y ∈ V
11	10	fnopfvb 3811	. . . . . . . . . . . 12 ⊢ ((rec(F, A) Fn On ⋀ x ∈ On) → ((rec(F, A) ‘x) = y ↔ ⟨x, y⟩ ∈ rec(F, A)))
12	9, 11	mpan 707	. . . . . . . . . . 11 ⊢ (x ∈ On → ((rec(F, A) ‘x) = y ↔ ⟨x, y⟩ ∈ rec(F, A)))
13		eqcom 1524	. . . . . . . . . . 11 ⊢ (y = (rec(F, A) ‘x) ↔ (rec(F, A) ‘x) = y)
14	12, 13	syl5bb 543	. . . . . . . . . 10 ⊢ (x ∈ On → (y = (rec(F, A) ‘x) ↔ ⟨x, y⟩ ∈ rec(F, A)))
15	8, 14	syl6 22	. . . . . . . . 9 ⊢ (Lim B → (x ∈ B → (y = (rec(F, A) ‘x) ↔ ⟨x, y⟩ ∈ rec(F, A))))
16	15	pm5.32d 658	. . . . . . . 8 ⊢ (Lim B → ((x ∈ B ⋀ y = (rec(F, A) ‘x)) ↔ (x ∈ B ⋀ ⟨x, y⟩ ∈ rec(F, A))))
17	16	exbidv 1321	. . . . . . 7 ⊢ (Lim B → (∃x(x ∈ B ⋀ y = (rec(F, A) ‘x)) ↔ ∃x(x ∈ B ⋀ ⟨x, y⟩ ∈ rec(F, A))))
18		df-rex 1697	. . . . . . 7 ⊢ (∃x ∈ B y = (rec(F, A) ‘x) ↔ ∃x(x ∈ B ⋀ y = (rec(F, A) ‘x)))
19	17, 18	syl5rbb 544	. . . . . 6 ⊢ (Lim B → (∃x(x ∈ B ⋀ ⟨x, y⟩ ∈ rec(F, A)) ↔ ∃x ∈ B y = (rec(F, A) ‘x)))
20	19	abbidv 1624	. . . . 5 ⊢ (Lim B → {y∣∃x(x ∈ B ⋀ ⟨x, y⟩ ∈ rec(F, A))} = {y∣∃x ∈ B y = (rec(F, A) ‘x)})
21		dfima3 3463	. . . . 5 ⊢ (rec(F, A) “ B) = {y∣∃x(x ∈ B ⋀ ⟨x, y⟩ ∈ rec(F, A))}
22	20, 21	syl5eq 1566	. . . 4 ⊢ (Lim B → (rec(F, A) “ B) = {y∣∃x ∈ B y = (rec(F, A) ‘x)})
23	22	unieqd 2566	. . 3 ⊢ (Lim B → ∪(rec(F, A) “ B) = ∪{y∣∃x ∈ B y = (rec(F, A) ‘x)})
24	23	adantl 397	. 2 ⊢ ((B ∈ C ⋀ Lim B) → ∪(rec(F, A) “ B) = ∪{y∣∃x ∈ B y = (rec(F, A) ‘x)})
25	1, 24	eqtrd 1554	1 ⊢ ((B ∈ C ⋀ Lim B) → (rec(F, A) ‘B) = ∪{y∣∃x ∈ B y = (rec(F, A) ‘x)})

Syntax hints:   → wi 3   ↔ wb 153   ⋀ wa 230   = wceq 997   ∈ wcel 999  ∃wex 1021  {cab 1509  ∃wrex 1693  ⟨cop 2463  ∪cuni 2557  Ord word 3004  Oncon0 3005  Lim wlim 3006   “ cima 3230   Fn wfn 3234   ‘cfv 3239  reccrdg 3989

This theorem is referenced by:  rdglim2a 4008

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-rep 2748  ax-sep 2758  ax-nul 2765  ax-pow 2798  ax-pr 2835  ax-un 2922

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3or 788  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-rab 1699  df-v 1859  df-sbc 1989  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-if 2414  df-pw 2454  df-sn 2464  df-pr 2465  df-tp 2467  df-op 2468  df-uni 2558  df-iun 2622  df-br 2675  df-opab 2722  df-tr 2736  df-eprel 2888  df-id 2891  df-po 2896  df-so 2906  df-fr 2974  df-we 2991  df-ord 3008  df-on 3009  df-lim 3010  df-suc 3011  df-xp 3241  df-rel 3242  df-cnv 3243  df-co 3244  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fun 3249  df-fn 3250  df-fv 3255  df-rdg 3990

Copyright terms: Public domain