# Metamath Proof Explorer

## Theorem fin23lem16

Description: Lemma for fin23 . U ranges over the original set; in particular ran U is a set, although we do not assume here that U is. (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Hypothesis fin23lem.a ${⊢}{U}={seq}_{\omega }\left(\left({i}\in \mathrm{\omega },{u}\in \mathrm{V}⟼if\left({t}\left({i}\right)\cap {u}=\varnothing ,{u},{t}\left({i}\right)\cap {u}\right)\right),\bigcup \mathrm{ran}{t}\right)$
Assertion fin23lem16 ${⊢}\bigcup \mathrm{ran}{U}=\bigcup \mathrm{ran}{t}$

### Proof

Step Hyp Ref Expression
1 fin23lem.a ${⊢}{U}={seq}_{\omega }\left(\left({i}\in \mathrm{\omega },{u}\in \mathrm{V}⟼if\left({t}\left({i}\right)\cap {u}=\varnothing ,{u},{t}\left({i}\right)\cap {u}\right)\right),\bigcup \mathrm{ran}{t}\right)$
2 unissb ${⊢}\bigcup \mathrm{ran}{U}\subseteq \bigcup \mathrm{ran}{t}↔\forall {a}\in \mathrm{ran}{U}\phantom{\rule{.4em}{0ex}}{a}\subseteq \bigcup \mathrm{ran}{t}$
3 1 fnseqom ${⊢}{U}Fn\mathrm{\omega }$
4 fvelrnb ${⊢}{U}Fn\mathrm{\omega }\to \left({a}\in \mathrm{ran}{U}↔\exists {b}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{U}\left({b}\right)={a}\right)$
5 3 4 ax-mp ${⊢}{a}\in \mathrm{ran}{U}↔\exists {b}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{U}\left({b}\right)={a}$
6 peano1 ${⊢}\varnothing \in \mathrm{\omega }$
7 0ss ${⊢}\varnothing \subseteq {b}$
8 1 fin23lem15 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \varnothing \in \mathrm{\omega }\right)\wedge \varnothing \subseteq {b}\right)\to {U}\left({b}\right)\subseteq {U}\left(\varnothing \right)$
9 7 8 mpan2 ${⊢}\left({b}\in \mathrm{\omega }\wedge \varnothing \in \mathrm{\omega }\right)\to {U}\left({b}\right)\subseteq {U}\left(\varnothing \right)$
10 6 9 mpan2 ${⊢}{b}\in \mathrm{\omega }\to {U}\left({b}\right)\subseteq {U}\left(\varnothing \right)$
11 vex ${⊢}{t}\in \mathrm{V}$
12 11 rnex ${⊢}\mathrm{ran}{t}\in \mathrm{V}$
13 12 uniex ${⊢}\bigcup \mathrm{ran}{t}\in \mathrm{V}$
14 1 seqom0g ${⊢}\bigcup \mathrm{ran}{t}\in \mathrm{V}\to {U}\left(\varnothing \right)=\bigcup \mathrm{ran}{t}$
15 13 14 ax-mp ${⊢}{U}\left(\varnothing \right)=\bigcup \mathrm{ran}{t}$
16 10 15 sseqtrdi ${⊢}{b}\in \mathrm{\omega }\to {U}\left({b}\right)\subseteq \bigcup \mathrm{ran}{t}$
17 sseq1 ${⊢}{U}\left({b}\right)={a}\to \left({U}\left({b}\right)\subseteq \bigcup \mathrm{ran}{t}↔{a}\subseteq \bigcup \mathrm{ran}{t}\right)$
18 16 17 syl5ibcom ${⊢}{b}\in \mathrm{\omega }\to \left({U}\left({b}\right)={a}\to {a}\subseteq \bigcup \mathrm{ran}{t}\right)$
19 18 rexlimiv ${⊢}\exists {b}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{U}\left({b}\right)={a}\to {a}\subseteq \bigcup \mathrm{ran}{t}$
20 5 19 sylbi ${⊢}{a}\in \mathrm{ran}{U}\to {a}\subseteq \bigcup \mathrm{ran}{t}$
21 2 20 mprgbir ${⊢}\bigcup \mathrm{ran}{U}\subseteq \bigcup \mathrm{ran}{t}$
22 fnfvelrn ${⊢}\left({U}Fn\mathrm{\omega }\wedge \varnothing \in \mathrm{\omega }\right)\to {U}\left(\varnothing \right)\in \mathrm{ran}{U}$
23 3 6 22 mp2an ${⊢}{U}\left(\varnothing \right)\in \mathrm{ran}{U}$
24 15 23 eqeltrri ${⊢}\bigcup \mathrm{ran}{t}\in \mathrm{ran}{U}$
25 elssuni ${⊢}\bigcup \mathrm{ran}{t}\in \mathrm{ran}{U}\to \bigcup \mathrm{ran}{t}\subseteq \bigcup \mathrm{ran}{U}$
26 24 25 ax-mp ${⊢}\bigcup \mathrm{ran}{t}\subseteq \bigcup \mathrm{ran}{U}$
27 21 26 eqssi ${⊢}\bigcup \mathrm{ran}{U}=\bigcup \mathrm{ran}{t}$