# Metamath Proof Explorer

## Theorem isf32lem3

Description: Lemma for isfin3-2 . Being a chain, difference sets are disjoint (one case). (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 isf32lem3 ${⊢}\left(\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge \left({B}\in {A}\wedge {\phi }\right)\right)\to \left({F}\left({A}\right)\setminus {F}\left(\mathrm{suc}{A}\right)\right)\cap \left({F}\left({B}\right)\setminus {F}\left(\mathrm{suc}{B}\right)\right)=\varnothing$

### 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 eldifi ${⊢}{a}\in \left({F}\left({A}\right)\setminus {F}\left(\mathrm{suc}{A}\right)\right)\to {a}\in {F}\left({A}\right)$
5 simpll ${⊢}\left(\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge \left({B}\in {A}\wedge {\phi }\right)\right)\to {A}\in \mathrm{\omega }$
6 peano2 ${⊢}{B}\in \mathrm{\omega }\to \mathrm{suc}{B}\in \mathrm{\omega }$
7 6 ad2antlr ${⊢}\left(\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge \left({B}\in {A}\wedge {\phi }\right)\right)\to \mathrm{suc}{B}\in \mathrm{\omega }$
8 nnord ${⊢}{A}\in \mathrm{\omega }\to \mathrm{Ord}{A}$
9 8 ad2antrr ${⊢}\left(\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge \left({B}\in {A}\wedge {\phi }\right)\right)\to \mathrm{Ord}{A}$
10 simprl ${⊢}\left(\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge \left({B}\in {A}\wedge {\phi }\right)\right)\to {B}\in {A}$
11 ordsucss ${⊢}\mathrm{Ord}{A}\to \left({B}\in {A}\to \mathrm{suc}{B}\subseteq {A}\right)$
12 9 10 11 sylc ${⊢}\left(\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge \left({B}\in {A}\wedge {\phi }\right)\right)\to \mathrm{suc}{B}\subseteq {A}$
13 simprr ${⊢}\left(\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge \left({B}\in {A}\wedge {\phi }\right)\right)\to {\phi }$
14 1 2 3 isf32lem1 ${⊢}\left(\left({A}\in \mathrm{\omega }\wedge \mathrm{suc}{B}\in \mathrm{\omega }\right)\wedge \left(\mathrm{suc}{B}\subseteq {A}\wedge {\phi }\right)\right)\to {F}\left({A}\right)\subseteq {F}\left(\mathrm{suc}{B}\right)$
15 5 7 12 13 14 syl22anc ${⊢}\left(\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge \left({B}\in {A}\wedge {\phi }\right)\right)\to {F}\left({A}\right)\subseteq {F}\left(\mathrm{suc}{B}\right)$
16 15 sseld ${⊢}\left(\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge \left({B}\in {A}\wedge {\phi }\right)\right)\to \left({a}\in {F}\left({A}\right)\to {a}\in {F}\left(\mathrm{suc}{B}\right)\right)$
17 elndif ${⊢}{a}\in {F}\left(\mathrm{suc}{B}\right)\to ¬{a}\in \left({F}\left({B}\right)\setminus {F}\left(\mathrm{suc}{B}\right)\right)$
18 4 16 17 syl56 ${⊢}\left(\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge \left({B}\in {A}\wedge {\phi }\right)\right)\to \left({a}\in \left({F}\left({A}\right)\setminus {F}\left(\mathrm{suc}{A}\right)\right)\to ¬{a}\in \left({F}\left({B}\right)\setminus {F}\left(\mathrm{suc}{B}\right)\right)\right)$
19 18 ralrimiv ${⊢}\left(\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge \left({B}\in {A}\wedge {\phi }\right)\right)\to \forall {a}\in \left({F}\left({A}\right)\setminus {F}\left(\mathrm{suc}{A}\right)\right)\phantom{\rule{.4em}{0ex}}¬{a}\in \left({F}\left({B}\right)\setminus {F}\left(\mathrm{suc}{B}\right)\right)$
20 disj ${⊢}\left({F}\left({A}\right)\setminus {F}\left(\mathrm{suc}{A}\right)\right)\cap \left({F}\left({B}\right)\setminus {F}\left(\mathrm{suc}{B}\right)\right)=\varnothing ↔\forall {a}\in \left({F}\left({A}\right)\setminus {F}\left(\mathrm{suc}{A}\right)\right)\phantom{\rule{.4em}{0ex}}¬{a}\in \left({F}\left({B}\right)\setminus {F}\left(\mathrm{suc}{B}\right)\right)$
21 19 20 sylibr ${⊢}\left(\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge \left({B}\in {A}\wedge {\phi }\right)\right)\to \left({F}\left({A}\right)\setminus {F}\left(\mathrm{suc}{A}\right)\right)\cap \left({F}\left({B}\right)\setminus {F}\left(\mathrm{suc}{B}\right)\right)=\varnothing$