# Metamath Proof Explorer

## Theorem r1ordg

Description: Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of TakeutiZaring p. 77. (Contributed by NM, 8-Sep-2003)

Ref Expression
Assertion r1ordg ${⊢}{B}\in \mathrm{dom}{R}_{1}\to \left({A}\in {B}\to {R}_{1}\left({A}\right)\in {R}_{1}\left({B}\right)\right)$

### Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({B}\in \mathrm{dom}{R}_{1}\wedge {A}\in {B}\right)\to {B}\in \mathrm{dom}{R}_{1}$
2 r1funlim ${⊢}\left(\mathrm{Fun}{R}_{1}\wedge \mathrm{Lim}\mathrm{dom}{R}_{1}\right)$
3 2 simpri ${⊢}\mathrm{Lim}\mathrm{dom}{R}_{1}$
4 limord ${⊢}\mathrm{Lim}\mathrm{dom}{R}_{1}\to \mathrm{Ord}\mathrm{dom}{R}_{1}$
5 3 4 ax-mp ${⊢}\mathrm{Ord}\mathrm{dom}{R}_{1}$
6 ordsson ${⊢}\mathrm{Ord}\mathrm{dom}{R}_{1}\to \mathrm{dom}{R}_{1}\subseteq \mathrm{On}$
7 5 6 ax-mp ${⊢}\mathrm{dom}{R}_{1}\subseteq \mathrm{On}$
8 7 sseli ${⊢}{B}\in \mathrm{dom}{R}_{1}\to {B}\in \mathrm{On}$
9 1 8 syl ${⊢}\left({B}\in \mathrm{dom}{R}_{1}\wedge {A}\in {B}\right)\to {B}\in \mathrm{On}$
10 onelon ${⊢}\left({B}\in \mathrm{On}\wedge {A}\in {B}\right)\to {A}\in \mathrm{On}$
11 8 10 sylan ${⊢}\left({B}\in \mathrm{dom}{R}_{1}\wedge {A}\in {B}\right)\to {A}\in \mathrm{On}$
12 suceloni ${⊢}{A}\in \mathrm{On}\to \mathrm{suc}{A}\in \mathrm{On}$
13 11 12 syl ${⊢}\left({B}\in \mathrm{dom}{R}_{1}\wedge {A}\in {B}\right)\to \mathrm{suc}{A}\in \mathrm{On}$
14 eloni ${⊢}{B}\in \mathrm{On}\to \mathrm{Ord}{B}$
15 ordsucss ${⊢}\mathrm{Ord}{B}\to \left({A}\in {B}\to \mathrm{suc}{A}\subseteq {B}\right)$
16 14 15 syl ${⊢}{B}\in \mathrm{On}\to \left({A}\in {B}\to \mathrm{suc}{A}\subseteq {B}\right)$
17 16 imp ${⊢}\left({B}\in \mathrm{On}\wedge {A}\in {B}\right)\to \mathrm{suc}{A}\subseteq {B}$
18 8 17 sylan ${⊢}\left({B}\in \mathrm{dom}{R}_{1}\wedge {A}\in {B}\right)\to \mathrm{suc}{A}\subseteq {B}$
19 eleq1 ${⊢}{x}=\mathrm{suc}{A}\to \left({x}\in \mathrm{dom}{R}_{1}↔\mathrm{suc}{A}\in \mathrm{dom}{R}_{1}\right)$
20 fveq2 ${⊢}{x}=\mathrm{suc}{A}\to {R}_{1}\left({x}\right)={R}_{1}\left(\mathrm{suc}{A}\right)$
21 20 eleq2d ${⊢}{x}=\mathrm{suc}{A}\to \left({R}_{1}\left({A}\right)\in {R}_{1}\left({x}\right)↔{R}_{1}\left({A}\right)\in {R}_{1}\left(\mathrm{suc}{A}\right)\right)$
22 19 21 imbi12d ${⊢}{x}=\mathrm{suc}{A}\to \left(\left({x}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\in {R}_{1}\left({x}\right)\right)↔\left(\mathrm{suc}{A}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\in {R}_{1}\left(\mathrm{suc}{A}\right)\right)\right)$
23 eleq1 ${⊢}{x}={y}\to \left({x}\in \mathrm{dom}{R}_{1}↔{y}\in \mathrm{dom}{R}_{1}\right)$
24 fveq2 ${⊢}{x}={y}\to {R}_{1}\left({x}\right)={R}_{1}\left({y}\right)$
25 24 eleq2d ${⊢}{x}={y}\to \left({R}_{1}\left({A}\right)\in {R}_{1}\left({x}\right)↔{R}_{1}\left({A}\right)\in {R}_{1}\left({y}\right)\right)$
26 23 25 imbi12d ${⊢}{x}={y}\to \left(\left({x}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\in {R}_{1}\left({x}\right)\right)↔\left({y}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\in {R}_{1}\left({y}\right)\right)\right)$
27 eleq1 ${⊢}{x}=\mathrm{suc}{y}\to \left({x}\in \mathrm{dom}{R}_{1}↔\mathrm{suc}{y}\in \mathrm{dom}{R}_{1}\right)$
28 fveq2 ${⊢}{x}=\mathrm{suc}{y}\to {R}_{1}\left({x}\right)={R}_{1}\left(\mathrm{suc}{y}\right)$
29 28 eleq2d ${⊢}{x}=\mathrm{suc}{y}\to \left({R}_{1}\left({A}\right)\in {R}_{1}\left({x}\right)↔{R}_{1}\left({A}\right)\in {R}_{1}\left(\mathrm{suc}{y}\right)\right)$
30 27 29 imbi12d ${⊢}{x}=\mathrm{suc}{y}\to \left(\left({x}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\in {R}_{1}\left({x}\right)\right)↔\left(\mathrm{suc}{y}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\in {R}_{1}\left(\mathrm{suc}{y}\right)\right)\right)$
31 eleq1 ${⊢}{x}={B}\to \left({x}\in \mathrm{dom}{R}_{1}↔{B}\in \mathrm{dom}{R}_{1}\right)$
32 fveq2 ${⊢}{x}={B}\to {R}_{1}\left({x}\right)={R}_{1}\left({B}\right)$
33 32 eleq2d ${⊢}{x}={B}\to \left({R}_{1}\left({A}\right)\in {R}_{1}\left({x}\right)↔{R}_{1}\left({A}\right)\in {R}_{1}\left({B}\right)\right)$
34 31 33 imbi12d ${⊢}{x}={B}\to \left(\left({x}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\in {R}_{1}\left({x}\right)\right)↔\left({B}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\in {R}_{1}\left({B}\right)\right)\right)$
35 fvex ${⊢}{R}_{1}\left({A}\right)\in \mathrm{V}$
36 35 pwid ${⊢}{R}_{1}\left({A}\right)\in 𝒫{R}_{1}\left({A}\right)$
37 limsuc ${⊢}\mathrm{Lim}\mathrm{dom}{R}_{1}\to \left({A}\in \mathrm{dom}{R}_{1}↔\mathrm{suc}{A}\in \mathrm{dom}{R}_{1}\right)$
38 3 37 ax-mp ${⊢}{A}\in \mathrm{dom}{R}_{1}↔\mathrm{suc}{A}\in \mathrm{dom}{R}_{1}$
39 r1sucg ${⊢}{A}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left(\mathrm{suc}{A}\right)=𝒫{R}_{1}\left({A}\right)$
40 38 39 sylbir ${⊢}\mathrm{suc}{A}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left(\mathrm{suc}{A}\right)=𝒫{R}_{1}\left({A}\right)$
41 36 40 eleqtrrid ${⊢}\mathrm{suc}{A}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\in {R}_{1}\left(\mathrm{suc}{A}\right)$
42 41 a1i ${⊢}\mathrm{suc}{A}\in \mathrm{On}\to \left(\mathrm{suc}{A}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\in {R}_{1}\left(\mathrm{suc}{A}\right)\right)$
43 limsuc ${⊢}\mathrm{Lim}\mathrm{dom}{R}_{1}\to \left({y}\in \mathrm{dom}{R}_{1}↔\mathrm{suc}{y}\in \mathrm{dom}{R}_{1}\right)$
44 3 43 ax-mp ${⊢}{y}\in \mathrm{dom}{R}_{1}↔\mathrm{suc}{y}\in \mathrm{dom}{R}_{1}$
45 r1tr ${⊢}\mathrm{Tr}{R}_{1}\left({y}\right)$
46 dftr4 ${⊢}\mathrm{Tr}{R}_{1}\left({y}\right)↔{R}_{1}\left({y}\right)\subseteq 𝒫{R}_{1}\left({y}\right)$
47 45 46 mpbi ${⊢}{R}_{1}\left({y}\right)\subseteq 𝒫{R}_{1}\left({y}\right)$
48 r1sucg ${⊢}{y}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left(\mathrm{suc}{y}\right)=𝒫{R}_{1}\left({y}\right)$
49 47 48 sseqtrrid ${⊢}{y}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({y}\right)\subseteq {R}_{1}\left(\mathrm{suc}{y}\right)$
50 49 sseld ${⊢}{y}\in \mathrm{dom}{R}_{1}\to \left({R}_{1}\left({A}\right)\in {R}_{1}\left({y}\right)\to {R}_{1}\left({A}\right)\in {R}_{1}\left(\mathrm{suc}{y}\right)\right)$
51 50 a2i ${⊢}\left({y}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\in {R}_{1}\left({y}\right)\right)\to \left({y}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\in {R}_{1}\left(\mathrm{suc}{y}\right)\right)$
52 44 51 syl5bir ${⊢}\left({y}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\in {R}_{1}\left({y}\right)\right)\to \left(\mathrm{suc}{y}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\in {R}_{1}\left(\mathrm{suc}{y}\right)\right)$
53 52 a1i ${⊢}\left(\left({y}\in \mathrm{On}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \mathrm{suc}{A}\subseteq {y}\right)\to \left(\left({y}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\in {R}_{1}\left({y}\right)\right)\to \left(\mathrm{suc}{y}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\in {R}_{1}\left(\mathrm{suc}{y}\right)\right)\right)$
54 simprl ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \left(\mathrm{suc}{A}\subseteq {x}\wedge {x}\in \mathrm{dom}{R}_{1}\right)\right)\to \mathrm{suc}{A}\subseteq {x}$
55 simplr ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \left(\mathrm{suc}{A}\subseteq {x}\wedge {x}\in \mathrm{dom}{R}_{1}\right)\right)\to \mathrm{suc}{A}\in \mathrm{On}$
56 sucelon ${⊢}{A}\in \mathrm{On}↔\mathrm{suc}{A}\in \mathrm{On}$
57 55 56 sylibr ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \left(\mathrm{suc}{A}\subseteq {x}\wedge {x}\in \mathrm{dom}{R}_{1}\right)\right)\to {A}\in \mathrm{On}$
58 limord ${⊢}\mathrm{Lim}{x}\to \mathrm{Ord}{x}$
59 58 ad2antrr ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \left(\mathrm{suc}{A}\subseteq {x}\wedge {x}\in \mathrm{dom}{R}_{1}\right)\right)\to \mathrm{Ord}{x}$
60 ordelsuc ${⊢}\left({A}\in \mathrm{On}\wedge \mathrm{Ord}{x}\right)\to \left({A}\in {x}↔\mathrm{suc}{A}\subseteq {x}\right)$
61 57 59 60 syl2anc ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \left(\mathrm{suc}{A}\subseteq {x}\wedge {x}\in \mathrm{dom}{R}_{1}\right)\right)\to \left({A}\in {x}↔\mathrm{suc}{A}\subseteq {x}\right)$
62 54 61 mpbird ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \left(\mathrm{suc}{A}\subseteq {x}\wedge {x}\in \mathrm{dom}{R}_{1}\right)\right)\to {A}\in {x}$
63 limsuc ${⊢}\mathrm{Lim}{x}\to \left({A}\in {x}↔\mathrm{suc}{A}\in {x}\right)$
64 63 ad2antrr ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \left(\mathrm{suc}{A}\subseteq {x}\wedge {x}\in \mathrm{dom}{R}_{1}\right)\right)\to \left({A}\in {x}↔\mathrm{suc}{A}\in {x}\right)$
65 62 64 mpbid ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \left(\mathrm{suc}{A}\subseteq {x}\wedge {x}\in \mathrm{dom}{R}_{1}\right)\right)\to \mathrm{suc}{A}\in {x}$
66 simprr ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \left(\mathrm{suc}{A}\subseteq {x}\wedge {x}\in \mathrm{dom}{R}_{1}\right)\right)\to {x}\in \mathrm{dom}{R}_{1}$
67 ordtr1 ${⊢}\mathrm{Ord}\mathrm{dom}{R}_{1}\to \left(\left({A}\in {x}\wedge {x}\in \mathrm{dom}{R}_{1}\right)\to {A}\in \mathrm{dom}{R}_{1}\right)$
68 5 67 ax-mp ${⊢}\left({A}\in {x}\wedge {x}\in \mathrm{dom}{R}_{1}\right)\to {A}\in \mathrm{dom}{R}_{1}$
69 62 66 68 syl2anc ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \left(\mathrm{suc}{A}\subseteq {x}\wedge {x}\in \mathrm{dom}{R}_{1}\right)\right)\to {A}\in \mathrm{dom}{R}_{1}$
70 69 39 syl ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \left(\mathrm{suc}{A}\subseteq {x}\wedge {x}\in \mathrm{dom}{R}_{1}\right)\right)\to {R}_{1}\left(\mathrm{suc}{A}\right)=𝒫{R}_{1}\left({A}\right)$
71 36 70 eleqtrrid ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \left(\mathrm{suc}{A}\subseteq {x}\wedge {x}\in \mathrm{dom}{R}_{1}\right)\right)\to {R}_{1}\left({A}\right)\in {R}_{1}\left(\mathrm{suc}{A}\right)$
72 fveq2 ${⊢}{y}=\mathrm{suc}{A}\to {R}_{1}\left({y}\right)={R}_{1}\left(\mathrm{suc}{A}\right)$
73 72 eleq2d ${⊢}{y}=\mathrm{suc}{A}\to \left({R}_{1}\left({A}\right)\in {R}_{1}\left({y}\right)↔{R}_{1}\left({A}\right)\in {R}_{1}\left(\mathrm{suc}{A}\right)\right)$
74 73 rspcev ${⊢}\left(\mathrm{suc}{A}\in {x}\wedge {R}_{1}\left({A}\right)\in {R}_{1}\left(\mathrm{suc}{A}\right)\right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{R}_{1}\left({A}\right)\in {R}_{1}\left({y}\right)$
75 65 71 74 syl2anc ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \left(\mathrm{suc}{A}\subseteq {x}\wedge {x}\in \mathrm{dom}{R}_{1}\right)\right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{R}_{1}\left({A}\right)\in {R}_{1}\left({y}\right)$
76 eliun ${⊢}{R}_{1}\left({A}\right)\in \bigcup _{{y}\in {x}}{R}_{1}\left({y}\right)↔\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{R}_{1}\left({A}\right)\in {R}_{1}\left({y}\right)$
77 75 76 sylibr ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \left(\mathrm{suc}{A}\subseteq {x}\wedge {x}\in \mathrm{dom}{R}_{1}\right)\right)\to {R}_{1}\left({A}\right)\in \bigcup _{{y}\in {x}}{R}_{1}\left({y}\right)$
78 simpll ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \left(\mathrm{suc}{A}\subseteq {x}\wedge {x}\in \mathrm{dom}{R}_{1}\right)\right)\to \mathrm{Lim}{x}$
79 r1limg ${⊢}\left({x}\in \mathrm{dom}{R}_{1}\wedge \mathrm{Lim}{x}\right)\to {R}_{1}\left({x}\right)=\bigcup _{{y}\in {x}}{R}_{1}\left({y}\right)$
80 66 78 79 syl2anc ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \left(\mathrm{suc}{A}\subseteq {x}\wedge {x}\in \mathrm{dom}{R}_{1}\right)\right)\to {R}_{1}\left({x}\right)=\bigcup _{{y}\in {x}}{R}_{1}\left({y}\right)$
81 77 80 eleqtrrd ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \left(\mathrm{suc}{A}\subseteq {x}\wedge {x}\in \mathrm{dom}{R}_{1}\right)\right)\to {R}_{1}\left({A}\right)\in {R}_{1}\left({x}\right)$
82 81 expr ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \mathrm{suc}{A}\subseteq {x}\right)\to \left({x}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\in {R}_{1}\left({x}\right)\right)$
83 82 a1d ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \mathrm{suc}{A}\subseteq {x}\right)\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{A}\subseteq {y}\to \left({y}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\in {R}_{1}\left({y}\right)\right)\right)\to \left({x}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\in {R}_{1}\left({x}\right)\right)\right)$
84 22 26 30 34 42 53 83 tfindsg ${⊢}\left(\left({B}\in \mathrm{On}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \mathrm{suc}{A}\subseteq {B}\right)\to \left({B}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left({A}\right)\in {R}_{1}\left({B}\right)\right)$
85 84 impr ${⊢}\left(\left({B}\in \mathrm{On}\wedge \mathrm{suc}{A}\in \mathrm{On}\right)\wedge \left(\mathrm{suc}{A}\subseteq {B}\wedge {B}\in \mathrm{dom}{R}_{1}\right)\right)\to {R}_{1}\left({A}\right)\in {R}_{1}\left({B}\right)$
86 9 13 18 1 85 syl22anc ${⊢}\left({B}\in \mathrm{dom}{R}_{1}\wedge {A}\in {B}\right)\to {R}_{1}\left({A}\right)\in {R}_{1}\left({B}\right)$
87 86 ex ${⊢}{B}\in \mathrm{dom}{R}_{1}\to \left({A}\in {B}\to {R}_{1}\left({A}\right)\in {R}_{1}\left({B}\right)\right)$