# Metamath Proof Explorer

## Theorem r1elwf

Description: Any member of the cumulative hierarchy is well-founded. (Contributed by Mario Carneiro, 28-May-2013) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion r1elwf ${⊢}{A}\in {R}_{1}\left({B}\right)\to {A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]$

### Proof

Step Hyp Ref Expression
1 r1funlim ${⊢}\left(\mathrm{Fun}{R}_{1}\wedge \mathrm{Lim}\mathrm{dom}{R}_{1}\right)$
2 1 simpri ${⊢}\mathrm{Lim}\mathrm{dom}{R}_{1}$
3 limord ${⊢}\mathrm{Lim}\mathrm{dom}{R}_{1}\to \mathrm{Ord}\mathrm{dom}{R}_{1}$
4 ordsson ${⊢}\mathrm{Ord}\mathrm{dom}{R}_{1}\to \mathrm{dom}{R}_{1}\subseteq \mathrm{On}$
5 2 3 4 mp2b ${⊢}\mathrm{dom}{R}_{1}\subseteq \mathrm{On}$
6 elfvdm ${⊢}{A}\in {R}_{1}\left({B}\right)\to {B}\in \mathrm{dom}{R}_{1}$
7 5 6 sseldi ${⊢}{A}\in {R}_{1}\left({B}\right)\to {B}\in \mathrm{On}$
8 r1tr ${⊢}\mathrm{Tr}{R}_{1}\left({B}\right)$
9 trss ${⊢}\mathrm{Tr}{R}_{1}\left({B}\right)\to \left({A}\in {R}_{1}\left({B}\right)\to {A}\subseteq {R}_{1}\left({B}\right)\right)$
10 8 9 ax-mp ${⊢}{A}\in {R}_{1}\left({B}\right)\to {A}\subseteq {R}_{1}\left({B}\right)$
11 elpwg ${⊢}{A}\in {R}_{1}\left({B}\right)\to \left({A}\in 𝒫{R}_{1}\left({B}\right)↔{A}\subseteq {R}_{1}\left({B}\right)\right)$
12 10 11 mpbird ${⊢}{A}\in {R}_{1}\left({B}\right)\to {A}\in 𝒫{R}_{1}\left({B}\right)$
13 r1sucg ${⊢}{B}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left(\mathrm{suc}{B}\right)=𝒫{R}_{1}\left({B}\right)$
14 6 13 syl ${⊢}{A}\in {R}_{1}\left({B}\right)\to {R}_{1}\left(\mathrm{suc}{B}\right)=𝒫{R}_{1}\left({B}\right)$
15 12 14 eleqtrrd ${⊢}{A}\in {R}_{1}\left({B}\right)\to {A}\in {R}_{1}\left(\mathrm{suc}{B}\right)$
16 suceq ${⊢}{x}={B}\to \mathrm{suc}{x}=\mathrm{suc}{B}$
17 16 fveq2d ${⊢}{x}={B}\to {R}_{1}\left(\mathrm{suc}{x}\right)={R}_{1}\left(\mathrm{suc}{B}\right)$
18 17 eleq2d ${⊢}{x}={B}\to \left({A}\in {R}_{1}\left(\mathrm{suc}{x}\right)↔{A}\in {R}_{1}\left(\mathrm{suc}{B}\right)\right)$
19 18 rspcev ${⊢}\left({B}\in \mathrm{On}\wedge {A}\in {R}_{1}\left(\mathrm{suc}{B}\right)\right)\to \exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{A}\in {R}_{1}\left(\mathrm{suc}{x}\right)$
20 7 15 19 syl2anc ${⊢}{A}\in {R}_{1}\left({B}\right)\to \exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{A}\in {R}_{1}\left(\mathrm{suc}{x}\right)$
21 rankwflemb ${⊢}{A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]↔\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{A}\in {R}_{1}\left(\mathrm{suc}{x}\right)$
22 20 21 sylibr ${⊢}{A}\in {R}_{1}\left({B}\right)\to {A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]$