# Metamath Proof Explorer

## Theorem r1val1

Description: The value of the cumulative hierarchy of sets function expressed recursively. Theorem 7Q of Enderton p. 202. (Contributed by NM, 25-Nov-2003) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion r1val1 ${⊢}{A}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)=\bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)$

### Proof

Step Hyp Ref Expression
1 simpr ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {A}=\varnothing \right)\to {A}=\varnothing$
2 1 fveq2d ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {A}=\varnothing \right)\to {R}_{1}\left({A}\right)={R}_{1}\left(\varnothing \right)$
3 r10 ${⊢}{R}_{1}\left(\varnothing \right)=\varnothing$
4 2 3 syl6eq ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {A}=\varnothing \right)\to {R}_{1}\left({A}\right)=\varnothing$
5 0ss ${⊢}\varnothing \subseteq \bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)$
6 5 a1i ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {A}=\varnothing \right)\to \varnothing \subseteq \bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)$
7 4 6 eqsstrd ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {A}=\varnothing \right)\to {R}_{1}\left({A}\right)\subseteq \bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)$
8 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{A}\in \mathrm{dom}{R}_{1}$
9 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{R}_{1}\left({A}\right)$
10 nfiu1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)$
11 9 10 nfss ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{R}_{1}\left({A}\right)\subseteq \bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)$
12 simpr ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {A}=\mathrm{suc}{x}\right)\to {A}=\mathrm{suc}{x}$
13 12 fveq2d ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {A}=\mathrm{suc}{x}\right)\to {R}_{1}\left({A}\right)={R}_{1}\left(\mathrm{suc}{x}\right)$
14 eleq1 ${⊢}{A}=\mathrm{suc}{x}\to \left({A}\in \mathrm{dom}{R}_{1}↔\mathrm{suc}{x}\in \mathrm{dom}{R}_{1}\right)$
15 14 biimpac ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {A}=\mathrm{suc}{x}\right)\to \mathrm{suc}{x}\in \mathrm{dom}{R}_{1}$
16 r1funlim ${⊢}\left(\mathrm{Fun}{R}_{1}\wedge \mathrm{Lim}\mathrm{dom}{R}_{1}\right)$
17 16 simpri ${⊢}\mathrm{Lim}\mathrm{dom}{R}_{1}$
18 limsuc ${⊢}\mathrm{Lim}\mathrm{dom}{R}_{1}\to \left({x}\in \mathrm{dom}{R}_{1}↔\mathrm{suc}{x}\in \mathrm{dom}{R}_{1}\right)$
19 17 18 ax-mp ${⊢}{x}\in \mathrm{dom}{R}_{1}↔\mathrm{suc}{x}\in \mathrm{dom}{R}_{1}$
20 15 19 sylibr ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {A}=\mathrm{suc}{x}\right)\to {x}\in \mathrm{dom}{R}_{1}$
21 r1sucg ${⊢}{x}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left(\mathrm{suc}{x}\right)=𝒫{R}_{1}\left({x}\right)$
22 20 21 syl ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {A}=\mathrm{suc}{x}\right)\to {R}_{1}\left(\mathrm{suc}{x}\right)=𝒫{R}_{1}\left({x}\right)$
23 13 22 eqtrd ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {A}=\mathrm{suc}{x}\right)\to {R}_{1}\left({A}\right)=𝒫{R}_{1}\left({x}\right)$
24 vex ${⊢}{x}\in \mathrm{V}$
25 24 sucid ${⊢}{x}\in \mathrm{suc}{x}$
26 25 12 eleqtrrid ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {A}=\mathrm{suc}{x}\right)\to {x}\in {A}$
27 ssiun2 ${⊢}{x}\in {A}\to 𝒫{R}_{1}\left({x}\right)\subseteq \bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)$
28 26 27 syl ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {A}=\mathrm{suc}{x}\right)\to 𝒫{R}_{1}\left({x}\right)\subseteq \bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)$
29 23 28 eqsstrd ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {A}=\mathrm{suc}{x}\right)\to {R}_{1}\left({A}\right)\subseteq \bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)$
30 29 ex ${⊢}{A}\in \mathrm{dom}{R}_{1}\to \left({A}=\mathrm{suc}{x}\to {R}_{1}\left({A}\right)\subseteq \bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)\right)$
31 30 a1d ${⊢}{A}\in \mathrm{dom}{R}_{1}\to \left({x}\in \mathrm{On}\to \left({A}=\mathrm{suc}{x}\to {R}_{1}\left({A}\right)\subseteq \bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)\right)\right)$
32 8 11 31 rexlimd ${⊢}{A}\in \mathrm{dom}{R}_{1}\to \left(\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{A}=\mathrm{suc}{x}\to {R}_{1}\left({A}\right)\subseteq \bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)\right)$
33 32 imp ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge \exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{A}=\mathrm{suc}{x}\right)\to {R}_{1}\left({A}\right)\subseteq \bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)$
34 r1limg ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge \mathrm{Lim}{A}\right)\to {R}_{1}\left({A}\right)=\bigcup _{{x}\in {A}}{R}_{1}\left({x}\right)$
35 r1tr ${⊢}\mathrm{Tr}{R}_{1}\left({x}\right)$
36 dftr4 ${⊢}\mathrm{Tr}{R}_{1}\left({x}\right)↔{R}_{1}\left({x}\right)\subseteq 𝒫{R}_{1}\left({x}\right)$
37 35 36 mpbi ${⊢}{R}_{1}\left({x}\right)\subseteq 𝒫{R}_{1}\left({x}\right)$
38 37 a1i ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge \mathrm{Lim}{A}\right)\to {R}_{1}\left({x}\right)\subseteq 𝒫{R}_{1}\left({x}\right)$
39 38 ralrimivw ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge \mathrm{Lim}{A}\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{R}_{1}\left({x}\right)\subseteq 𝒫{R}_{1}\left({x}\right)$
40 ss2iun ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{R}_{1}\left({x}\right)\subseteq 𝒫{R}_{1}\left({x}\right)\to \bigcup _{{x}\in {A}}{R}_{1}\left({x}\right)\subseteq \bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)$
41 39 40 syl ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge \mathrm{Lim}{A}\right)\to \bigcup _{{x}\in {A}}{R}_{1}\left({x}\right)\subseteq \bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)$
42 34 41 eqsstrd ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge \mathrm{Lim}{A}\right)\to {R}_{1}\left({A}\right)\subseteq \bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)$
43 42 adantrl ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge \left({A}\in \mathrm{V}\wedge \mathrm{Lim}{A}\right)\right)\to {R}_{1}\left({A}\right)\subseteq \bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)$
44 limord ${⊢}\mathrm{Lim}\mathrm{dom}{R}_{1}\to \mathrm{Ord}\mathrm{dom}{R}_{1}$
45 17 44 ax-mp ${⊢}\mathrm{Ord}\mathrm{dom}{R}_{1}$
46 ordsson ${⊢}\mathrm{Ord}\mathrm{dom}{R}_{1}\to \mathrm{dom}{R}_{1}\subseteq \mathrm{On}$
47 45 46 ax-mp ${⊢}\mathrm{dom}{R}_{1}\subseteq \mathrm{On}$
48 47 sseli ${⊢}{A}\in \mathrm{dom}{R}_{1}\to {A}\in \mathrm{On}$
49 onzsl ${⊢}{A}\in \mathrm{On}↔\left({A}=\varnothing \vee \exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{A}=\mathrm{suc}{x}\vee \left({A}\in \mathrm{V}\wedge \mathrm{Lim}{A}\right)\right)$
50 48 49 sylib ${⊢}{A}\in \mathrm{dom}{R}_{1}\to \left({A}=\varnothing \vee \exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{A}=\mathrm{suc}{x}\vee \left({A}\in \mathrm{V}\wedge \mathrm{Lim}{A}\right)\right)$
51 7 33 43 50 mpjao3dan ${⊢}{A}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\subseteq \bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)$
52 ordtr1 ${⊢}\mathrm{Ord}\mathrm{dom}{R}_{1}\to \left(\left({x}\in {A}\wedge {A}\in \mathrm{dom}{R}_{1}\right)\to {x}\in \mathrm{dom}{R}_{1}\right)$
53 45 52 ax-mp ${⊢}\left({x}\in {A}\wedge {A}\in \mathrm{dom}{R}_{1}\right)\to {x}\in \mathrm{dom}{R}_{1}$
54 53 ancoms ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {x}\in {A}\right)\to {x}\in \mathrm{dom}{R}_{1}$
55 54 21 syl ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {x}\in {A}\right)\to {R}_{1}\left(\mathrm{suc}{x}\right)=𝒫{R}_{1}\left({x}\right)$
56 simpr ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {x}\in {A}\right)\to {x}\in {A}$
57 ordelord ${⊢}\left(\mathrm{Ord}\mathrm{dom}{R}_{1}\wedge {A}\in \mathrm{dom}{R}_{1}\right)\to \mathrm{Ord}{A}$
58 45 57 mpan ${⊢}{A}\in \mathrm{dom}{R}_{1}\to \mathrm{Ord}{A}$
59 58 adantr ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {x}\in {A}\right)\to \mathrm{Ord}{A}$
60 ordelsuc ${⊢}\left({x}\in {A}\wedge \mathrm{Ord}{A}\right)\to \left({x}\in {A}↔\mathrm{suc}{x}\subseteq {A}\right)$
61 56 59 60 syl2anc ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {x}\in {A}\right)\to \left({x}\in {A}↔\mathrm{suc}{x}\subseteq {A}\right)$
62 56 61 mpbid ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {x}\in {A}\right)\to \mathrm{suc}{x}\subseteq {A}$
63 54 19 sylib ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {x}\in {A}\right)\to \mathrm{suc}{x}\in \mathrm{dom}{R}_{1}$
64 simpl ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {x}\in {A}\right)\to {A}\in \mathrm{dom}{R}_{1}$
65 r1ord3g ${⊢}\left(\mathrm{suc}{x}\in \mathrm{dom}{R}_{1}\wedge {A}\in \mathrm{dom}{R}_{1}\right)\to \left(\mathrm{suc}{x}\subseteq {A}\to {R}_{1}\left(\mathrm{suc}{x}\right)\subseteq {R}_{1}\left({A}\right)\right)$
66 63 64 65 syl2anc ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {x}\in {A}\right)\to \left(\mathrm{suc}{x}\subseteq {A}\to {R}_{1}\left(\mathrm{suc}{x}\right)\subseteq {R}_{1}\left({A}\right)\right)$
67 62 66 mpd ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {x}\in {A}\right)\to {R}_{1}\left(\mathrm{suc}{x}\right)\subseteq {R}_{1}\left({A}\right)$
68 55 67 eqsstrrd ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge {x}\in {A}\right)\to 𝒫{R}_{1}\left({x}\right)\subseteq {R}_{1}\left({A}\right)$
69 68 ralrimiva ${⊢}{A}\in \mathrm{dom}{R}_{1}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}𝒫{R}_{1}\left({x}\right)\subseteq {R}_{1}\left({A}\right)$
70 iunss ${⊢}\bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)\subseteq {R}_{1}\left({A}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}𝒫{R}_{1}\left({x}\right)\subseteq {R}_{1}\left({A}\right)$
71 69 70 sylibr ${⊢}{A}\in \mathrm{dom}{R}_{1}\to \bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)\subseteq {R}_{1}\left({A}\right)$
72 51 71 eqssd ${⊢}{A}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)=\bigcup _{{x}\in {A}}𝒫{R}_{1}\left({x}\right)$