# Metamath Proof Explorer

## Theorem aomclem4

Description: Lemma for dfac11 . Limit case. Patch together well-orderings constructed so far using fnwe2 to cover the limit rank. (Contributed by Stefan O'Rear, 20-Jan-2015)

Ref Expression
Hypotheses aomclem4.f ${⊢}{F}=\left\{⟨{a},{b}⟩|\left(\mathrm{rank}\left({a}\right)\mathrm{E}\mathrm{rank}\left({b}\right)\vee \left(\mathrm{rank}\left({a}\right)=\mathrm{rank}\left({b}\right)\wedge {a}{z}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right){b}\right)\right)\right\}$
aomclem4.on ${⊢}{\phi }\to \mathrm{dom}{z}\in \mathrm{On}$
aomclem4.su ${⊢}{\phi }\to \mathrm{dom}{z}=\bigcup \mathrm{dom}{z}$
aomclem4.we ${⊢}{\phi }\to \forall {a}\in \mathrm{dom}{z}\phantom{\rule{.4em}{0ex}}{z}\left({a}\right)\mathrm{We}{R}_{1}\left({a}\right)$
Assertion aomclem4 ${⊢}{\phi }\to {F}\mathrm{We}{R}_{1}\left(\mathrm{dom}{z}\right)$

### Proof

Step Hyp Ref Expression
1 aomclem4.f ${⊢}{F}=\left\{⟨{a},{b}⟩|\left(\mathrm{rank}\left({a}\right)\mathrm{E}\mathrm{rank}\left({b}\right)\vee \left(\mathrm{rank}\left({a}\right)=\mathrm{rank}\left({b}\right)\wedge {a}{z}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right){b}\right)\right)\right\}$
2 aomclem4.on ${⊢}{\phi }\to \mathrm{dom}{z}\in \mathrm{On}$
3 aomclem4.su ${⊢}{\phi }\to \mathrm{dom}{z}=\bigcup \mathrm{dom}{z}$
4 aomclem4.we ${⊢}{\phi }\to \forall {a}\in \mathrm{dom}{z}\phantom{\rule{.4em}{0ex}}{z}\left({a}\right)\mathrm{We}{R}_{1}\left({a}\right)$
5 suceq ${⊢}{c}=\mathrm{rank}\left({a}\right)\to \mathrm{suc}{c}=\mathrm{suc}\mathrm{rank}\left({a}\right)$
6 5 fveq2d ${⊢}{c}=\mathrm{rank}\left({a}\right)\to {z}\left(\mathrm{suc}{c}\right)={z}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)$
7 r1fnon ${⊢}{R}_{1}Fn\mathrm{On}$
8 fnfun ${⊢}{R}_{1}Fn\mathrm{On}\to \mathrm{Fun}{R}_{1}$
9 7 8 ax-mp ${⊢}\mathrm{Fun}{R}_{1}$
10 fndm ${⊢}{R}_{1}Fn\mathrm{On}\to \mathrm{dom}{R}_{1}=\mathrm{On}$
11 7 10 ax-mp ${⊢}\mathrm{dom}{R}_{1}=\mathrm{On}$
12 11 eqimss2i ${⊢}\mathrm{On}\subseteq \mathrm{dom}{R}_{1}$
13 9 12 pm3.2i ${⊢}\left(\mathrm{Fun}{R}_{1}\wedge \mathrm{On}\subseteq \mathrm{dom}{R}_{1}\right)$
14 funfvima2 ${⊢}\left(\mathrm{Fun}{R}_{1}\wedge \mathrm{On}\subseteq \mathrm{dom}{R}_{1}\right)\to \left(\mathrm{dom}{z}\in \mathrm{On}\to {R}_{1}\left(\mathrm{dom}{z}\right)\in {R}_{1}\left[\mathrm{On}\right]\right)$
15 13 2 14 mpsyl ${⊢}{\phi }\to {R}_{1}\left(\mathrm{dom}{z}\right)\in {R}_{1}\left[\mathrm{On}\right]$
16 elssuni ${⊢}{R}_{1}\left(\mathrm{dom}{z}\right)\in {R}_{1}\left[\mathrm{On}\right]\to {R}_{1}\left(\mathrm{dom}{z}\right)\subseteq \bigcup {R}_{1}\left[\mathrm{On}\right]$
17 15 16 syl ${⊢}{\phi }\to {R}_{1}\left(\mathrm{dom}{z}\right)\subseteq \bigcup {R}_{1}\left[\mathrm{On}\right]$
18 17 sselda ${⊢}\left({\phi }\wedge {b}\in {R}_{1}\left(\mathrm{dom}{z}\right)\right)\to {b}\in \bigcup {R}_{1}\left[\mathrm{On}\right]$
19 rankidb ${⊢}{b}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\to {b}\in {R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({b}\right)\right)$
20 18 19 syl ${⊢}\left({\phi }\wedge {b}\in {R}_{1}\left(\mathrm{dom}{z}\right)\right)\to {b}\in {R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({b}\right)\right)$
21 suceq ${⊢}\mathrm{rank}\left({b}\right)=\mathrm{rank}\left({a}\right)\to \mathrm{suc}\mathrm{rank}\left({b}\right)=\mathrm{suc}\mathrm{rank}\left({a}\right)$
22 21 fveq2d ${⊢}\mathrm{rank}\left({b}\right)=\mathrm{rank}\left({a}\right)\to {R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({b}\right)\right)={R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)$
23 22 eleq2d ${⊢}\mathrm{rank}\left({b}\right)=\mathrm{rank}\left({a}\right)\to \left({b}\in {R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({b}\right)\right)↔{b}\in {R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)\right)$
24 20 23 syl5ibcom ${⊢}\left({\phi }\wedge {b}\in {R}_{1}\left(\mathrm{dom}{z}\right)\right)\to \left(\mathrm{rank}\left({b}\right)=\mathrm{rank}\left({a}\right)\to {b}\in {R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)\right)$
25 24 expimpd ${⊢}{\phi }\to \left(\left({b}\in {R}_{1}\left(\mathrm{dom}{z}\right)\wedge \mathrm{rank}\left({b}\right)=\mathrm{rank}\left({a}\right)\right)\to {b}\in {R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)\right)$
26 25 ss2abdv ${⊢}{\phi }\to \left\{{b}|\left({b}\in {R}_{1}\left(\mathrm{dom}{z}\right)\wedge \mathrm{rank}\left({b}\right)=\mathrm{rank}\left({a}\right)\right)\right\}\subseteq \left\{{b}|{b}\in {R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)\right\}$
27 df-rab ${⊢}\left\{{b}\in {R}_{1}\left(\mathrm{dom}{z}\right)|\mathrm{rank}\left({b}\right)=\mathrm{rank}\left({a}\right)\right\}=\left\{{b}|\left({b}\in {R}_{1}\left(\mathrm{dom}{z}\right)\wedge \mathrm{rank}\left({b}\right)=\mathrm{rank}\left({a}\right)\right)\right\}$
28 abid1 ${⊢}{R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)=\left\{{b}|{b}\in {R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)\right\}$
29 26 27 28 3sstr4g ${⊢}{\phi }\to \left\{{b}\in {R}_{1}\left(\mathrm{dom}{z}\right)|\mathrm{rank}\left({b}\right)=\mathrm{rank}\left({a}\right)\right\}\subseteq {R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)$
30 29 adantr ${⊢}\left({\phi }\wedge {a}\in {R}_{1}\left(\mathrm{dom}{z}\right)\right)\to \left\{{b}\in {R}_{1}\left(\mathrm{dom}{z}\right)|\mathrm{rank}\left({b}\right)=\mathrm{rank}\left({a}\right)\right\}\subseteq {R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)$
31 fveq2 ${⊢}{b}=\mathrm{suc}\mathrm{rank}\left({a}\right)\to {z}\left({b}\right)={z}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)$
32 fveq2 ${⊢}{b}=\mathrm{suc}\mathrm{rank}\left({a}\right)\to {R}_{1}\left({b}\right)={R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)$
33 31 32 weeq12d ${⊢}{b}=\mathrm{suc}\mathrm{rank}\left({a}\right)\to \left({z}\left({b}\right)\mathrm{We}{R}_{1}\left({b}\right)↔{z}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)\mathrm{We}{R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)\right)$
34 fveq2 ${⊢}{a}={b}\to {z}\left({a}\right)={z}\left({b}\right)$
35 fveq2 ${⊢}{a}={b}\to {R}_{1}\left({a}\right)={R}_{1}\left({b}\right)$
36 34 35 weeq12d ${⊢}{a}={b}\to \left({z}\left({a}\right)\mathrm{We}{R}_{1}\left({a}\right)↔{z}\left({b}\right)\mathrm{We}{R}_{1}\left({b}\right)\right)$
37 36 cbvralvw ${⊢}\forall {a}\in \mathrm{dom}{z}\phantom{\rule{.4em}{0ex}}{z}\left({a}\right)\mathrm{We}{R}_{1}\left({a}\right)↔\forall {b}\in \mathrm{dom}{z}\phantom{\rule{.4em}{0ex}}{z}\left({b}\right)\mathrm{We}{R}_{1}\left({b}\right)$
38 4 37 sylib ${⊢}{\phi }\to \forall {b}\in \mathrm{dom}{z}\phantom{\rule{.4em}{0ex}}{z}\left({b}\right)\mathrm{We}{R}_{1}\left({b}\right)$
39 38 adantr ${⊢}\left({\phi }\wedge {a}\in {R}_{1}\left(\mathrm{dom}{z}\right)\right)\to \forall {b}\in \mathrm{dom}{z}\phantom{\rule{.4em}{0ex}}{z}\left({b}\right)\mathrm{We}{R}_{1}\left({b}\right)$
40 rankr1ai ${⊢}{a}\in {R}_{1}\left(\mathrm{dom}{z}\right)\to \mathrm{rank}\left({a}\right)\in \mathrm{dom}{z}$
41 40 adantl ${⊢}\left({\phi }\wedge {a}\in {R}_{1}\left(\mathrm{dom}{z}\right)\right)\to \mathrm{rank}\left({a}\right)\in \mathrm{dom}{z}$
42 eloni ${⊢}\mathrm{dom}{z}\in \mathrm{On}\to \mathrm{Ord}\mathrm{dom}{z}$
43 2 42 syl ${⊢}{\phi }\to \mathrm{Ord}\mathrm{dom}{z}$
44 limsuc2 ${⊢}\left(\mathrm{Ord}\mathrm{dom}{z}\wedge \mathrm{dom}{z}=\bigcup \mathrm{dom}{z}\right)\to \left(\mathrm{rank}\left({a}\right)\in \mathrm{dom}{z}↔\mathrm{suc}\mathrm{rank}\left({a}\right)\in \mathrm{dom}{z}\right)$
45 43 3 44 syl2anc ${⊢}{\phi }\to \left(\mathrm{rank}\left({a}\right)\in \mathrm{dom}{z}↔\mathrm{suc}\mathrm{rank}\left({a}\right)\in \mathrm{dom}{z}\right)$
46 45 adantr ${⊢}\left({\phi }\wedge {a}\in {R}_{1}\left(\mathrm{dom}{z}\right)\right)\to \left(\mathrm{rank}\left({a}\right)\in \mathrm{dom}{z}↔\mathrm{suc}\mathrm{rank}\left({a}\right)\in \mathrm{dom}{z}\right)$
47 41 46 mpbid ${⊢}\left({\phi }\wedge {a}\in {R}_{1}\left(\mathrm{dom}{z}\right)\right)\to \mathrm{suc}\mathrm{rank}\left({a}\right)\in \mathrm{dom}{z}$
48 33 39 47 rspcdva ${⊢}\left({\phi }\wedge {a}\in {R}_{1}\left(\mathrm{dom}{z}\right)\right)\to {z}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)\mathrm{We}{R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)$
49 wess ${⊢}\left\{{b}\in {R}_{1}\left(\mathrm{dom}{z}\right)|\mathrm{rank}\left({b}\right)=\mathrm{rank}\left({a}\right)\right\}\subseteq {R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)\to \left({z}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)\mathrm{We}{R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)\to {z}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)\mathrm{We}\left\{{b}\in {R}_{1}\left(\mathrm{dom}{z}\right)|\mathrm{rank}\left({b}\right)=\mathrm{rank}\left({a}\right)\right\}\right)$
50 30 48 49 sylc ${⊢}\left({\phi }\wedge {a}\in {R}_{1}\left(\mathrm{dom}{z}\right)\right)\to {z}\left(\mathrm{suc}\mathrm{rank}\left({a}\right)\right)\mathrm{We}\left\{{b}\in {R}_{1}\left(\mathrm{dom}{z}\right)|\mathrm{rank}\left({b}\right)=\mathrm{rank}\left({a}\right)\right\}$
51 rankf ${⊢}\mathrm{rank}:\bigcup {R}_{1}\left[\mathrm{On}\right]⟶\mathrm{On}$
52 51 a1i ${⊢}{\phi }\to \mathrm{rank}:\bigcup {R}_{1}\left[\mathrm{On}\right]⟶\mathrm{On}$
53 52 17 fssresd ${⊢}{\phi }\to \left({\mathrm{rank}↾}_{{R}_{1}\left(\mathrm{dom}{z}\right)}\right):{R}_{1}\left(\mathrm{dom}{z}\right)⟶\mathrm{On}$
54 epweon ${⊢}\mathrm{E}\mathrm{We}\mathrm{On}$
55 54 a1i ${⊢}{\phi }\to \mathrm{E}\mathrm{We}\mathrm{On}$
56 6 1 50 53 55 fnwe2 ${⊢}{\phi }\to {F}\mathrm{We}{R}_{1}\left(\mathrm{dom}{z}\right)$