# Metamath Proof Explorer

## Theorem ptcmplem5

Description: Lemma for ptcmp . (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypotheses ptcmp.1 ${⊢}{S}=\left({k}\in {A},{u}\in {F}\left({k}\right)⟼{\left({w}\in {X}⟼{w}\left({k}\right)\right)}^{-1}\left[{u}\right]\right)$
ptcmp.2 ${⊢}{X}=\underset{{n}\in {A}}{⨉}\bigcup {F}\left({n}\right)$
ptcmp.3 ${⊢}{\phi }\to {A}\in {V}$
ptcmp.4 ${⊢}{\phi }\to {F}:{A}⟶\mathrm{Comp}$
ptcmp.5 ${⊢}{\phi }\to {X}\in \left(\mathrm{UFL}\cap \mathrm{dom}\mathrm{card}\right)$
Assertion ptcmplem5 ${⊢}{\phi }\to {\prod }_{𝑡}\left({F}\right)\in \mathrm{Comp}$

### Proof

Step Hyp Ref Expression
1 ptcmp.1 ${⊢}{S}=\left({k}\in {A},{u}\in {F}\left({k}\right)⟼{\left({w}\in {X}⟼{w}\left({k}\right)\right)}^{-1}\left[{u}\right]\right)$
2 ptcmp.2 ${⊢}{X}=\underset{{n}\in {A}}{⨉}\bigcup {F}\left({n}\right)$
3 ptcmp.3 ${⊢}{\phi }\to {A}\in {V}$
4 ptcmp.4 ${⊢}{\phi }\to {F}:{A}⟶\mathrm{Comp}$
5 ptcmp.5 ${⊢}{\phi }\to {X}\in \left(\mathrm{UFL}\cap \mathrm{dom}\mathrm{card}\right)$
6 5 elin1d ${⊢}{\phi }\to {X}\in \mathrm{UFL}$
7 1 2 3 4 5 ptcmplem1 ${⊢}{\phi }\to \left({X}=\bigcup \left(\mathrm{ran}{S}\cup \left\{{X}\right\}\right)\wedge {\prod }_{𝑡}\left({F}\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\mathrm{ran}{S}\cup \left\{{X}\right\}\right)\right)\right)$
8 7 simpld ${⊢}{\phi }\to {X}=\bigcup \left(\mathrm{ran}{S}\cup \left\{{X}\right\}\right)$
9 7 simprd ${⊢}{\phi }\to {\prod }_{𝑡}\left({F}\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\mathrm{ran}{S}\cup \left\{{X}\right\}\right)\right)$
10 elpwi ${⊢}{y}\in 𝒫\mathrm{ran}{S}\to {y}\subseteq \mathrm{ran}{S}$
11 3 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({y}\subseteq \mathrm{ran}{S}\wedge {X}=\bigcup {y}\right)\right)\wedge ¬\exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}\right)\to {A}\in {V}$
12 4 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({y}\subseteq \mathrm{ran}{S}\wedge {X}=\bigcup {y}\right)\right)\wedge ¬\exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}\right)\to {F}:{A}⟶\mathrm{Comp}$
13 5 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({y}\subseteq \mathrm{ran}{S}\wedge {X}=\bigcup {y}\right)\right)\wedge ¬\exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}\right)\to {X}\in \left(\mathrm{UFL}\cap \mathrm{dom}\mathrm{card}\right)$
14 simplrl ${⊢}\left(\left({\phi }\wedge \left({y}\subseteq \mathrm{ran}{S}\wedge {X}=\bigcup {y}\right)\right)\wedge ¬\exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}\right)\to {y}\subseteq \mathrm{ran}{S}$
15 simplrr ${⊢}\left(\left({\phi }\wedge \left({y}\subseteq \mathrm{ran}{S}\wedge {X}=\bigcup {y}\right)\right)\wedge ¬\exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}\right)\to {X}=\bigcup {y}$
16 simpr ${⊢}\left(\left({\phi }\wedge \left({y}\subseteq \mathrm{ran}{S}\wedge {X}=\bigcup {y}\right)\right)\wedge ¬\exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}\right)\to ¬\exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}$
17 imaeq2 ${⊢}{z}={u}\to {\left({w}\in {X}⟼{w}\left({k}\right)\right)}^{-1}\left[{z}\right]={\left({w}\in {X}⟼{w}\left({k}\right)\right)}^{-1}\left[{u}\right]$
18 17 eleq1d ${⊢}{z}={u}\to \left({\left({w}\in {X}⟼{w}\left({k}\right)\right)}^{-1}\left[{z}\right]\in {y}↔{\left({w}\in {X}⟼{w}\left({k}\right)\right)}^{-1}\left[{u}\right]\in {y}\right)$
19 18 cbvrabv ${⊢}\left\{{z}\in {F}\left({k}\right)|{\left({w}\in {X}⟼{w}\left({k}\right)\right)}^{-1}\left[{z}\right]\in {y}\right\}=\left\{{u}\in {F}\left({k}\right)|{\left({w}\in {X}⟼{w}\left({k}\right)\right)}^{-1}\left[{u}\right]\in {y}\right\}$
20 1 2 11 12 13 14 15 16 19 ptcmplem4 ${⊢}¬\left(\left({\phi }\wedge \left({y}\subseteq \mathrm{ran}{S}\wedge {X}=\bigcup {y}\right)\right)\wedge ¬\exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}\right)$
21 iman ${⊢}\left(\left({\phi }\wedge \left({y}\subseteq \mathrm{ran}{S}\wedge {X}=\bigcup {y}\right)\right)\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}\right)↔¬\left(\left({\phi }\wedge \left({y}\subseteq \mathrm{ran}{S}\wedge {X}=\bigcup {y}\right)\right)\wedge ¬\exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}\right)$
22 20 21 mpbir ${⊢}\left({\phi }\wedge \left({y}\subseteq \mathrm{ran}{S}\wedge {X}=\bigcup {y}\right)\right)\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}$
23 22 expr ${⊢}\left({\phi }\wedge {y}\subseteq \mathrm{ran}{S}\right)\to \left({X}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}\right)$
24 10 23 sylan2 ${⊢}\left({\phi }\wedge {y}\in 𝒫\mathrm{ran}{S}\right)\to \left({X}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}\right)$
25 24 adantlr ${⊢}\left(\left({\phi }\wedge {y}\subseteq \mathrm{ran}{S}\cup \left\{{X}\right\}\right)\wedge {y}\in 𝒫\mathrm{ran}{S}\right)\to \left({X}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}\right)$
26 velpw ${⊢}{y}\in 𝒫\left(\mathrm{ran}{S}\cup \left\{{X}\right\}\right)↔{y}\subseteq \mathrm{ran}{S}\cup \left\{{X}\right\}$
27 eldif ${⊢}{y}\in \left(𝒫\left(\mathrm{ran}{S}\cup \left\{{X}\right\}\right)\setminus 𝒫\mathrm{ran}{S}\right)↔\left({y}\in 𝒫\left(\mathrm{ran}{S}\cup \left\{{X}\right\}\right)\wedge ¬{y}\in 𝒫\mathrm{ran}{S}\right)$
28 elpwunsn ${⊢}{y}\in \left(𝒫\left(\mathrm{ran}{S}\cup \left\{{X}\right\}\right)\setminus 𝒫\mathrm{ran}{S}\right)\to {X}\in {y}$
29 27 28 sylbir ${⊢}\left({y}\in 𝒫\left(\mathrm{ran}{S}\cup \left\{{X}\right\}\right)\wedge ¬{y}\in 𝒫\mathrm{ran}{S}\right)\to {X}\in {y}$
30 26 29 sylanbr ${⊢}\left({y}\subseteq \mathrm{ran}{S}\cup \left\{{X}\right\}\wedge ¬{y}\in 𝒫\mathrm{ran}{S}\right)\to {X}\in {y}$
31 30 adantll ${⊢}\left(\left({\phi }\wedge {y}\subseteq \mathrm{ran}{S}\cup \left\{{X}\right\}\right)\wedge ¬{y}\in 𝒫\mathrm{ran}{S}\right)\to {X}\in {y}$
32 snssi ${⊢}{X}\in {y}\to \left\{{X}\right\}\subseteq {y}$
33 32 adantl ${⊢}\left(\left({\phi }\wedge {y}\subseteq \mathrm{ran}{S}\cup \left\{{X}\right\}\right)\wedge {X}\in {y}\right)\to \left\{{X}\right\}\subseteq {y}$
34 snfi ${⊢}\left\{{X}\right\}\in \mathrm{Fin}$
35 elfpw ${⊢}\left\{{X}\right\}\in \left(𝒫{y}\cap \mathrm{Fin}\right)↔\left(\left\{{X}\right\}\subseteq {y}\wedge \left\{{X}\right\}\in \mathrm{Fin}\right)$
36 33 34 35 sylanblrc ${⊢}\left(\left({\phi }\wedge {y}\subseteq \mathrm{ran}{S}\cup \left\{{X}\right\}\right)\wedge {X}\in {y}\right)\to \left\{{X}\right\}\in \left(𝒫{y}\cap \mathrm{Fin}\right)$
37 unisng ${⊢}{X}\in {y}\to \bigcup \left\{{X}\right\}={X}$
38 37 eqcomd ${⊢}{X}\in {y}\to {X}=\bigcup \left\{{X}\right\}$
39 38 adantl ${⊢}\left(\left({\phi }\wedge {y}\subseteq \mathrm{ran}{S}\cup \left\{{X}\right\}\right)\wedge {X}\in {y}\right)\to {X}=\bigcup \left\{{X}\right\}$
40 unieq ${⊢}{z}=\left\{{X}\right\}\to \bigcup {z}=\bigcup \left\{{X}\right\}$
41 40 rspceeqv ${⊢}\left(\left\{{X}\right\}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\wedge {X}=\bigcup \left\{{X}\right\}\right)\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}$
42 36 39 41 syl2anc ${⊢}\left(\left({\phi }\wedge {y}\subseteq \mathrm{ran}{S}\cup \left\{{X}\right\}\right)\wedge {X}\in {y}\right)\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}$
43 42 a1d ${⊢}\left(\left({\phi }\wedge {y}\subseteq \mathrm{ran}{S}\cup \left\{{X}\right\}\right)\wedge {X}\in {y}\right)\to \left({X}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}\right)$
44 31 43 syldan ${⊢}\left(\left({\phi }\wedge {y}\subseteq \mathrm{ran}{S}\cup \left\{{X}\right\}\right)\wedge ¬{y}\in 𝒫\mathrm{ran}{S}\right)\to \left({X}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}\right)$
45 25 44 pm2.61dan ${⊢}\left({\phi }\wedge {y}\subseteq \mathrm{ran}{S}\cup \left\{{X}\right\}\right)\to \left({X}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}\right)$
46 45 impr ${⊢}\left({\phi }\wedge \left({y}\subseteq \mathrm{ran}{S}\cup \left\{{X}\right\}\wedge {X}=\bigcup {y}\right)\right)\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}$
47 6 8 9 46 alexsub ${⊢}{\phi }\to {\prod }_{𝑡}\left({F}\right)\in \mathrm{Comp}$