# Metamath Proof Explorer

## Theorem isf32lem1

Description: Lemma for isfin3-2 . Derive weak ordering property. (Contributed by Stefan O'Rear, 5-Nov-2014)

Ref Expression
Hypotheses isf32lem.a ${⊢}{\phi }\to {F}:\mathrm{\omega }⟶𝒫{G}$
isf32lem.b ${⊢}{\phi }\to \forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{F}\left(\mathrm{suc}{x}\right)\subseteq {F}\left({x}\right)$
isf32lem.c ${⊢}{\phi }\to ¬\bigcap \mathrm{ran}{F}\in \mathrm{ran}{F}$
Assertion isf32lem1 ${⊢}\left(\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge \left({B}\subseteq {A}\wedge {\phi }\right)\right)\to {F}\left({A}\right)\subseteq {F}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 isf32lem.a ${⊢}{\phi }\to {F}:\mathrm{\omega }⟶𝒫{G}$
2 isf32lem.b ${⊢}{\phi }\to \forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{F}\left(\mathrm{suc}{x}\right)\subseteq {F}\left({x}\right)$
3 isf32lem.c ${⊢}{\phi }\to ¬\bigcap \mathrm{ran}{F}\in \mathrm{ran}{F}$
4 fveq2 ${⊢}{a}={B}\to {F}\left({a}\right)={F}\left({B}\right)$
5 4 sseq1d ${⊢}{a}={B}\to \left({F}\left({a}\right)\subseteq {F}\left({B}\right)↔{F}\left({B}\right)\subseteq {F}\left({B}\right)\right)$
6 5 imbi2d ${⊢}{a}={B}\to \left(\left({\phi }\to {F}\left({a}\right)\subseteq {F}\left({B}\right)\right)↔\left({\phi }\to {F}\left({B}\right)\subseteq {F}\left({B}\right)\right)\right)$
7 fveq2 ${⊢}{a}={b}\to {F}\left({a}\right)={F}\left({b}\right)$
8 7 sseq1d ${⊢}{a}={b}\to \left({F}\left({a}\right)\subseteq {F}\left({B}\right)↔{F}\left({b}\right)\subseteq {F}\left({B}\right)\right)$
9 8 imbi2d ${⊢}{a}={b}\to \left(\left({\phi }\to {F}\left({a}\right)\subseteq {F}\left({B}\right)\right)↔\left({\phi }\to {F}\left({b}\right)\subseteq {F}\left({B}\right)\right)\right)$
10 fveq2 ${⊢}{a}=\mathrm{suc}{b}\to {F}\left({a}\right)={F}\left(\mathrm{suc}{b}\right)$
11 10 sseq1d ${⊢}{a}=\mathrm{suc}{b}\to \left({F}\left({a}\right)\subseteq {F}\left({B}\right)↔{F}\left(\mathrm{suc}{b}\right)\subseteq {F}\left({B}\right)\right)$
12 11 imbi2d ${⊢}{a}=\mathrm{suc}{b}\to \left(\left({\phi }\to {F}\left({a}\right)\subseteq {F}\left({B}\right)\right)↔\left({\phi }\to {F}\left(\mathrm{suc}{b}\right)\subseteq {F}\left({B}\right)\right)\right)$
13 fveq2 ${⊢}{a}={A}\to {F}\left({a}\right)={F}\left({A}\right)$
14 13 sseq1d ${⊢}{a}={A}\to \left({F}\left({a}\right)\subseteq {F}\left({B}\right)↔{F}\left({A}\right)\subseteq {F}\left({B}\right)\right)$
15 14 imbi2d ${⊢}{a}={A}\to \left(\left({\phi }\to {F}\left({a}\right)\subseteq {F}\left({B}\right)\right)↔\left({\phi }\to {F}\left({A}\right)\subseteq {F}\left({B}\right)\right)\right)$
16 ssid ${⊢}{F}\left({B}\right)\subseteq {F}\left({B}\right)$
17 16 2a1i ${⊢}{B}\in \mathrm{\omega }\to \left({\phi }\to {F}\left({B}\right)\subseteq {F}\left({B}\right)\right)$
18 suceq ${⊢}{x}={b}\to \mathrm{suc}{x}=\mathrm{suc}{b}$
19 18 fveq2d ${⊢}{x}={b}\to {F}\left(\mathrm{suc}{x}\right)={F}\left(\mathrm{suc}{b}\right)$
20 fveq2 ${⊢}{x}={b}\to {F}\left({x}\right)={F}\left({b}\right)$
21 19 20 sseq12d ${⊢}{x}={b}\to \left({F}\left(\mathrm{suc}{x}\right)\subseteq {F}\left({x}\right)↔{F}\left(\mathrm{suc}{b}\right)\subseteq {F}\left({b}\right)\right)$
22 21 rspcv ${⊢}{b}\in \mathrm{\omega }\to \left(\forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{F}\left(\mathrm{suc}{x}\right)\subseteq {F}\left({x}\right)\to {F}\left(\mathrm{suc}{b}\right)\subseteq {F}\left({b}\right)\right)$
23 2 22 syl5 ${⊢}{b}\in \mathrm{\omega }\to \left({\phi }\to {F}\left(\mathrm{suc}{b}\right)\subseteq {F}\left({b}\right)\right)$
24 23 ad2antrr ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge {B}\subseteq {b}\right)\to \left({\phi }\to {F}\left(\mathrm{suc}{b}\right)\subseteq {F}\left({b}\right)\right)$
25 sstr2 ${⊢}{F}\left(\mathrm{suc}{b}\right)\subseteq {F}\left({b}\right)\to \left({F}\left({b}\right)\subseteq {F}\left({B}\right)\to {F}\left(\mathrm{suc}{b}\right)\subseteq {F}\left({B}\right)\right)$
26 24 25 syl6 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge {B}\subseteq {b}\right)\to \left({\phi }\to \left({F}\left({b}\right)\subseteq {F}\left({B}\right)\to {F}\left(\mathrm{suc}{b}\right)\subseteq {F}\left({B}\right)\right)\right)$
27 26 a2d ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge {B}\subseteq {b}\right)\to \left(\left({\phi }\to {F}\left({b}\right)\subseteq {F}\left({B}\right)\right)\to \left({\phi }\to {F}\left(\mathrm{suc}{b}\right)\subseteq {F}\left({B}\right)\right)\right)$
28 6 9 12 15 17 27 findsg ${⊢}\left(\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge {B}\subseteq {A}\right)\to \left({\phi }\to {F}\left({A}\right)\subseteq {F}\left({B}\right)\right)$
29 28 impr ${⊢}\left(\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge \left({B}\subseteq {A}\wedge {\phi }\right)\right)\to {F}\left({A}\right)\subseteq {F}\left({B}\right)$