Metamath Proof Explorer

Theorem setrecsss

Description: The setrecs operator respects the subset relation between two functions F and G . (Contributed by Emmett Weisz, 13-Mar-2022)

Ref Expression
Hypotheses setrecsss.1 ${⊢}{\phi }\to \mathrm{Fun}{G}$
setrecsss.2 ${⊢}{\phi }\to {F}\subseteq {G}$
Assertion setrecsss ${⊢}{\phi }\to \mathrm{setrecs}\left({F}\right)\subseteq \mathrm{setrecs}\left({G}\right)$

Proof

Step Hyp Ref Expression
1 setrecsss.1 ${⊢}{\phi }\to \mathrm{Fun}{G}$
2 setrecsss.2 ${⊢}{\phi }\to {F}\subseteq {G}$
3 eqid ${⊢}\mathrm{setrecs}\left({F}\right)=\mathrm{setrecs}\left({F}\right)$
4 imass1 ${⊢}{F}\subseteq {G}\to {F}\left[\left\{{x}\right\}\right]\subseteq {G}\left[\left\{{x}\right\}\right]$
5 2 4 syl ${⊢}{\phi }\to {F}\left[\left\{{x}\right\}\right]\subseteq {G}\left[\left\{{x}\right\}\right]$
6 5 unissd ${⊢}{\phi }\to \bigcup {F}\left[\left\{{x}\right\}\right]\subseteq \bigcup {G}\left[\left\{{x}\right\}\right]$
7 funss ${⊢}{F}\subseteq {G}\to \left(\mathrm{Fun}{G}\to \mathrm{Fun}{F}\right)$
8 2 1 7 sylc ${⊢}{\phi }\to \mathrm{Fun}{F}$
9 funfv ${⊢}\mathrm{Fun}{F}\to {F}\left({x}\right)=\bigcup {F}\left[\left\{{x}\right\}\right]$
10 8 9 syl ${⊢}{\phi }\to {F}\left({x}\right)=\bigcup {F}\left[\left\{{x}\right\}\right]$
11 funfv ${⊢}\mathrm{Fun}{G}\to {G}\left({x}\right)=\bigcup {G}\left[\left\{{x}\right\}\right]$
12 1 11 syl ${⊢}{\phi }\to {G}\left({x}\right)=\bigcup {G}\left[\left\{{x}\right\}\right]$
13 6 10 12 3sstr4d ${⊢}{\phi }\to {F}\left({x}\right)\subseteq {G}\left({x}\right)$
14 13 adantr ${⊢}\left({\phi }\wedge {x}\subseteq \mathrm{setrecs}\left({G}\right)\right)\to {F}\left({x}\right)\subseteq {G}\left({x}\right)$
15 eqid ${⊢}\mathrm{setrecs}\left({G}\right)=\mathrm{setrecs}\left({G}\right)$
16 vex ${⊢}{x}\in \mathrm{V}$
17 16 a1i ${⊢}\left({\phi }\wedge {x}\subseteq \mathrm{setrecs}\left({G}\right)\right)\to {x}\in \mathrm{V}$
18 simpr ${⊢}\left({\phi }\wedge {x}\subseteq \mathrm{setrecs}\left({G}\right)\right)\to {x}\subseteq \mathrm{setrecs}\left({G}\right)$
19 15 17 18 setrec1 ${⊢}\left({\phi }\wedge {x}\subseteq \mathrm{setrecs}\left({G}\right)\right)\to {G}\left({x}\right)\subseteq \mathrm{setrecs}\left({G}\right)$
20 14 19 sstrd ${⊢}\left({\phi }\wedge {x}\subseteq \mathrm{setrecs}\left({G}\right)\right)\to {F}\left({x}\right)\subseteq \mathrm{setrecs}\left({G}\right)$
21 20 ex ${⊢}{\phi }\to \left({x}\subseteq \mathrm{setrecs}\left({G}\right)\to {F}\left({x}\right)\subseteq \mathrm{setrecs}\left({G}\right)\right)$
22 21 alrimiv ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \mathrm{setrecs}\left({G}\right)\to {F}\left({x}\right)\subseteq \mathrm{setrecs}\left({G}\right)\right)$
23 3 22 setrec2v ${⊢}{\phi }\to \mathrm{setrecs}\left({F}\right)\subseteq \mathrm{setrecs}\left({G}\right)$