Metamath Proof Explorer

Theorem marypha2

Description: Version of marypha1 using a functional family of sets instead of a relation. (Contributed by Stefan O'Rear, 20-Feb-2015)

Ref Expression
Hypotheses marypha2.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
marypha2.b ${⊢}{\phi }\to {F}:{A}⟶\mathrm{Fin}$
marypha2.c ${⊢}\left({\phi }\wedge {d}\subseteq {A}\right)\to {d}\preccurlyeq \bigcup {F}\left[{d}\right]$
Assertion marypha2 ${⊢}{\phi }\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:{A}\underset{1-1}{⟶}\mathrm{V}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {F}\left({x}\right)\right)$

Proof

Step Hyp Ref Expression
1 marypha2.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
2 marypha2.b ${⊢}{\phi }\to {F}:{A}⟶\mathrm{Fin}$
3 marypha2.c ${⊢}\left({\phi }\wedge {d}\subseteq {A}\right)\to {d}\preccurlyeq \bigcup {F}\left[{d}\right]$
4 2 1 unirnffid ${⊢}{\phi }\to \bigcup \mathrm{ran}{F}\in \mathrm{Fin}$
5 eqid ${⊢}\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)=\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)$
6 5 marypha2lem1 ${⊢}\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)\subseteq {A}×\bigcup \mathrm{ran}{F}$
7 6 a1i ${⊢}{\phi }\to \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)\subseteq {A}×\bigcup \mathrm{ran}{F}$
8 2 ffnd ${⊢}{\phi }\to {F}Fn{A}$
9 5 marypha2lem4 ${⊢}\left({F}Fn{A}\wedge {d}\subseteq {A}\right)\to \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)\left[{d}\right]=\bigcup {F}\left[{d}\right]$
10 8 9 sylan ${⊢}\left({\phi }\wedge {d}\subseteq {A}\right)\to \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)\left[{d}\right]=\bigcup {F}\left[{d}\right]$
11 3 10 breqtrrd ${⊢}\left({\phi }\wedge {d}\subseteq {A}\right)\to {d}\preccurlyeq \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)\left[{d}\right]$
12 1 4 7 11 marypha1 ${⊢}{\phi }\to \exists {g}\in 𝒫\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)\phantom{\rule{.4em}{0ex}}{g}:{A}\underset{1-1}{⟶}\bigcup \mathrm{ran}{F}$
13 df-rex ${⊢}\exists {g}\in 𝒫\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)\phantom{\rule{.4em}{0ex}}{g}:{A}\underset{1-1}{⟶}\bigcup \mathrm{ran}{F}↔\exists {g}\phantom{\rule{.4em}{0ex}}\left({g}\in 𝒫\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)\wedge {g}:{A}\underset{1-1}{⟶}\bigcup \mathrm{ran}{F}\right)$
14 ssv ${⊢}\bigcup \mathrm{ran}{F}\subseteq \mathrm{V}$
15 f1ss ${⊢}\left({g}:{A}\underset{1-1}{⟶}\bigcup \mathrm{ran}{F}\wedge \bigcup \mathrm{ran}{F}\subseteq \mathrm{V}\right)\to {g}:{A}\underset{1-1}{⟶}\mathrm{V}$
16 14 15 mpan2 ${⊢}{g}:{A}\underset{1-1}{⟶}\bigcup \mathrm{ran}{F}\to {g}:{A}\underset{1-1}{⟶}\mathrm{V}$
17 16 ad2antll ${⊢}\left({\phi }\wedge \left({g}\in 𝒫\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)\wedge {g}:{A}\underset{1-1}{⟶}\bigcup \mathrm{ran}{F}\right)\right)\to {g}:{A}\underset{1-1}{⟶}\mathrm{V}$
18 elpwi ${⊢}{g}\in 𝒫\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)\to {g}\subseteq \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)$
19 18 ad2antrl ${⊢}\left({\phi }\wedge \left({g}\in 𝒫\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)\wedge {g}:{A}\underset{1-1}{⟶}\bigcup \mathrm{ran}{F}\right)\right)\to {g}\subseteq \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)$
20 f1fn ${⊢}{g}:{A}\underset{1-1}{⟶}\bigcup \mathrm{ran}{F}\to {g}Fn{A}$
21 20 ad2antll ${⊢}\left({\phi }\wedge \left({g}\in 𝒫\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)\wedge {g}:{A}\underset{1-1}{⟶}\bigcup \mathrm{ran}{F}\right)\right)\to {g}Fn{A}$
22 5 marypha2lem3 ${⊢}\left({F}Fn{A}\wedge {g}Fn{A}\right)\to \left({g}\subseteq \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {F}\left({x}\right)\right)$
23 8 21 22 syl2an2r ${⊢}\left({\phi }\wedge \left({g}\in 𝒫\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)\wedge {g}:{A}\underset{1-1}{⟶}\bigcup \mathrm{ran}{F}\right)\right)\to \left({g}\subseteq \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {F}\left({x}\right)\right)$
24 19 23 mpbid ${⊢}\left({\phi }\wedge \left({g}\in 𝒫\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)\wedge {g}:{A}\underset{1-1}{⟶}\bigcup \mathrm{ran}{F}\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {F}\left({x}\right)$
25 17 24 jca ${⊢}\left({\phi }\wedge \left({g}\in 𝒫\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)\wedge {g}:{A}\underset{1-1}{⟶}\bigcup \mathrm{ran}{F}\right)\right)\to \left({g}:{A}\underset{1-1}{⟶}\mathrm{V}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {F}\left({x}\right)\right)$
26 25 ex ${⊢}{\phi }\to \left(\left({g}\in 𝒫\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)\wedge {g}:{A}\underset{1-1}{⟶}\bigcup \mathrm{ran}{F}\right)\to \left({g}:{A}\underset{1-1}{⟶}\mathrm{V}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {F}\left({x}\right)\right)\right)$
27 26 eximdv ${⊢}{\phi }\to \left(\exists {g}\phantom{\rule{.4em}{0ex}}\left({g}\in 𝒫\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)\wedge {g}:{A}\underset{1-1}{⟶}\bigcup \mathrm{ran}{F}\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:{A}\underset{1-1}{⟶}\mathrm{V}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {F}\left({x}\right)\right)\right)$
28 13 27 syl5bi ${⊢}{\phi }\to \left(\exists {g}\in 𝒫\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{F}\left({x}\right)\right)\phantom{\rule{.4em}{0ex}}{g}:{A}\underset{1-1}{⟶}\bigcup \mathrm{ran}{F}\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:{A}\underset{1-1}{⟶}\mathrm{V}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {F}\left({x}\right)\right)\right)$
29 12 28 mpd ${⊢}{\phi }\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:{A}\underset{1-1}{⟶}\mathrm{V}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {F}\left({x}\right)\right)$