# Metamath Proof Explorer

## Theorem kelac1

Description: Kelley's choice, basic form: if a collection of sets can be cast as closed sets in the factors of a topology, and there is a definable element in each topology (which need not be in the closed set - if it were this would be trivial), then compactness (via finite intersection) guarantees that the final product is nonempty. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Hypotheses kelac1.z ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {S}\ne \varnothing$
kelac1.j ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {J}\in \mathrm{Top}$
kelac1.c ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {C}\in \mathrm{Clsd}\left({J}\right)$
kelac1.b ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {B}:{S}\underset{1-1 onto}{⟶}{C}$
kelac1.u ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {U}\in \bigcup {J}$
kelac1.k ${⊢}{\phi }\to {\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)\in \mathrm{Comp}$
Assertion kelac1 ${⊢}{\phi }\to \underset{{x}\in {I}}{⨉}{S}\ne \varnothing$

### Proof

Step Hyp Ref Expression
1 kelac1.z ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {S}\ne \varnothing$
2 kelac1.j ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {J}\in \mathrm{Top}$
3 kelac1.c ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {C}\in \mathrm{Clsd}\left({J}\right)$
4 kelac1.b ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {B}:{S}\underset{1-1 onto}{⟶}{C}$
5 kelac1.u ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {U}\in \bigcup {J}$
6 kelac1.k ${⊢}{\phi }\to {\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)\in \mathrm{Comp}$
7 eqid ${⊢}\bigcup {J}=\bigcup {J}$
8 7 cldss ${⊢}{C}\in \mathrm{Clsd}\left({J}\right)\to {C}\subseteq \bigcup {J}$
9 3 8 syl ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {C}\subseteq \bigcup {J}$
10 9 ralrimiva ${⊢}{\phi }\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{C}\subseteq \bigcup {J}$
11 boxriin ${⊢}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{C}\subseteq \bigcup {J}\to \underset{{x}\in {I}}{⨉}{C}=\underset{{x}\in {I}}{⨉}\bigcup {J}\cap \bigcap _{{y}\in {I}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)$
12 10 11 syl ${⊢}{\phi }\to \underset{{x}\in {I}}{⨉}{C}=\underset{{x}\in {I}}{⨉}\bigcup {J}\cap \bigcap _{{y}\in {I}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)$
13 cmptop ${⊢}{\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)\in \mathrm{Comp}\to {\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)\in \mathrm{Top}$
14 0ntop ${⊢}¬\varnothing \in \mathrm{Top}$
15 fvprc ${⊢}¬\left({x}\in {I}⟼{J}\right)\in \mathrm{V}\to {\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)=\varnothing$
16 15 eleq1d ${⊢}¬\left({x}\in {I}⟼{J}\right)\in \mathrm{V}\to \left({\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)\in \mathrm{Top}↔\varnothing \in \mathrm{Top}\right)$
17 14 16 mtbiri ${⊢}¬\left({x}\in {I}⟼{J}\right)\in \mathrm{V}\to ¬{\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)\in \mathrm{Top}$
18 17 con4i ${⊢}{\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)\in \mathrm{Top}\to \left({x}\in {I}⟼{J}\right)\in \mathrm{V}$
19 6 13 18 3syl ${⊢}{\phi }\to \left({x}\in {I}⟼{J}\right)\in \mathrm{V}$
20 2 fmpttd ${⊢}{\phi }\to \left({x}\in {I}⟼{J}\right):{I}⟶\mathrm{Top}$
21 dmfex ${⊢}\left(\left({x}\in {I}⟼{J}\right)\in \mathrm{V}\wedge \left({x}\in {I}⟼{J}\right):{I}⟶\mathrm{Top}\right)\to {I}\in \mathrm{V}$
22 19 20 21 syl2anc ${⊢}{\phi }\to {I}\in \mathrm{V}$
23 2 ralrimiva ${⊢}{\phi }\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{J}\in \mathrm{Top}$
24 eqid ${⊢}{\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)={\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)$
25 24 ptunimpt ${⊢}\left({I}\in \mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{J}\in \mathrm{Top}\right)\to \underset{{x}\in {I}}{⨉}\bigcup {J}=\bigcup {\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)$
26 22 23 25 syl2anc ${⊢}{\phi }\to \underset{{x}\in {I}}{⨉}\bigcup {J}=\bigcup {\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)$
27 26 ineq1d ${⊢}{\phi }\to \underset{{x}\in {I}}{⨉}\bigcup {J}\cap \bigcap _{{y}\in {I}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)=\bigcup {\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)\cap \bigcap _{{y}\in {I}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)$
28 eqid ${⊢}\bigcup {\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)=\bigcup {\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)$
29 7 topcld ${⊢}{J}\in \mathrm{Top}\to \bigcup {J}\in \mathrm{Clsd}\left({J}\right)$
30 2 29 syl ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to \bigcup {J}\in \mathrm{Clsd}\left({J}\right)$
31 3 30 ifcld ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to if\left({x}={y},{C},\bigcup {J}\right)\in \mathrm{Clsd}\left({J}\right)$
32 22 2 31 ptcldmpt ${⊢}{\phi }\to \underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)\in \mathrm{Clsd}\left({\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)\right)$
33 32 adantr ${⊢}\left({\phi }\wedge {y}\in {I}\right)\to \underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)\in \mathrm{Clsd}\left({\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)\right)$
34 simprr ${⊢}\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\to {z}\in \mathrm{Fin}$
35 f1ofo ${⊢}{B}:{S}\underset{1-1 onto}{⟶}{C}\to {B}:{S}\underset{onto}{⟶}{C}$
36 foima ${⊢}{B}:{S}\underset{onto}{⟶}{C}\to {B}\left[{S}\right]={C}$
37 4 35 36 3syl ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {B}\left[{S}\right]={C}$
38 37 eqcomd ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {C}={B}\left[{S}\right]$
39 f1ofn ${⊢}{B}:{S}\underset{1-1 onto}{⟶}{C}\to {B}Fn{S}$
40 4 39 syl ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {B}Fn{S}$
41 ssid ${⊢}{S}\subseteq {S}$
42 fnimaeq0 ${⊢}\left({B}Fn{S}\wedge {S}\subseteq {S}\right)\to \left({B}\left[{S}\right]=\varnothing ↔{S}=\varnothing \right)$
43 40 41 42 sylancl ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to \left({B}\left[{S}\right]=\varnothing ↔{S}=\varnothing \right)$
44 43 necon3bid ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to \left({B}\left[{S}\right]\ne \varnothing ↔{S}\ne \varnothing \right)$
45 1 44 mpbird ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {B}\left[{S}\right]\ne \varnothing$
46 38 45 eqnetrd ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {C}\ne \varnothing$
47 n0 ${⊢}{C}\ne \varnothing ↔\exists {w}\phantom{\rule{.4em}{0ex}}{w}\in {C}$
48 46 47 sylib ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to \exists {w}\phantom{\rule{.4em}{0ex}}{w}\in {C}$
49 rexv ${⊢}\exists {w}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}{w}\in {C}↔\exists {w}\phantom{\rule{.4em}{0ex}}{w}\in {C}$
50 48 49 sylibr ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to \exists {w}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}{w}\in {C}$
51 50 ralrimiva ${⊢}{\phi }\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\exists {w}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}{w}\in {C}$
52 ssralv ${⊢}{z}\subseteq {I}\to \left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\exists {w}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}{w}\in {C}\to \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}\exists {w}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}{w}\in {C}\right)$
53 52 adantr ${⊢}\left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\to \left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\exists {w}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}{w}\in {C}\to \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}\exists {w}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}{w}\in {C}\right)$
54 51 53 mpan9 ${⊢}\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\to \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}\exists {w}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}{w}\in {C}$
55 eleq1 ${⊢}{w}={f}\left({x}\right)\to \left({w}\in {C}↔{f}\left({x}\right)\in {C}\right)$
56 55 ac6sfi ${⊢}\left({z}\in \mathrm{Fin}\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}\exists {w}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}{w}\in {C}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{z}⟶\mathrm{V}\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)$
57 34 54 56 syl2anc ${⊢}\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{z}⟶\mathrm{V}\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)$
58 26 eqcomd ${⊢}{\phi }\to \bigcup {\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)=\underset{{x}\in {I}}{⨉}\bigcup {J}$
59 58 ineq1d ${⊢}{\phi }\to \bigcup {\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)\cap \bigcap _{{y}\in {z}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)=\underset{{x}\in {I}}{⨉}\bigcup {J}\cap \bigcap _{{y}\in {z}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)$
60 59 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\to \bigcup {\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)\cap \bigcap _{{y}\in {z}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)=\underset{{x}\in {I}}{⨉}\bigcup {J}\cap \bigcap _{{y}\in {z}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)$
61 iftrue ${⊢}{x}\in {z}\to if\left({x}\in {z},{f}\left({x}\right),{U}\right)={f}\left({x}\right)$
62 61 ad2antrl ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \left({x}\in {z}\wedge {f}\left({x}\right)\in {C}\right)\right)\to if\left({x}\in {z},{f}\left({x}\right),{U}\right)={f}\left({x}\right)$
63 simpll ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge {x}\in {z}\right)\to {\phi }$
64 simprl ${⊢}\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\to {z}\subseteq {I}$
65 64 sselda ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge {x}\in {z}\right)\to {x}\in {I}$
66 63 65 9 syl2anc ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge {x}\in {z}\right)\to {C}\subseteq \bigcup {J}$
67 66 sseld ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge {x}\in {z}\right)\to \left({f}\left({x}\right)\in {C}\to {f}\left({x}\right)\in \bigcup {J}\right)$
68 67 impr ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \left({x}\in {z}\wedge {f}\left({x}\right)\in {C}\right)\right)\to {f}\left({x}\right)\in \bigcup {J}$
69 62 68 eqeltrd ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \left({x}\in {z}\wedge {f}\left({x}\right)\in {C}\right)\right)\to if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in \bigcup {J}$
70 69 expr ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge {x}\in {z}\right)\to \left({f}\left({x}\right)\in {C}\to if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in \bigcup {J}\right)$
71 70 ralimdva ${⊢}\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\to \left(\forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\to \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in \bigcup {J}\right)$
72 71 imp ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\to \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in \bigcup {J}$
73 eldifn ${⊢}{x}\in \left({I}\setminus {z}\right)\to ¬{x}\in {z}$
74 73 iffalsed ${⊢}{x}\in \left({I}\setminus {z}\right)\to if\left({x}\in {z},{f}\left({x}\right),{U}\right)={U}$
75 74 adantl ${⊢}\left({\phi }\wedge {x}\in \left({I}\setminus {z}\right)\right)\to if\left({x}\in {z},{f}\left({x}\right),{U}\right)={U}$
76 eldifi ${⊢}{x}\in \left({I}\setminus {z}\right)\to {x}\in {I}$
77 76 5 sylan2 ${⊢}\left({\phi }\wedge {x}\in \left({I}\setminus {z}\right)\right)\to {U}\in \bigcup {J}$
78 75 77 eqeltrd ${⊢}\left({\phi }\wedge {x}\in \left({I}\setminus {z}\right)\right)\to if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in \bigcup {J}$
79 78 ralrimiva ${⊢}{\phi }\to \forall {x}\in \left({I}\setminus {z}\right)\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in \bigcup {J}$
80 79 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\to \forall {x}\in \left({I}\setminus {z}\right)\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in \bigcup {J}$
81 ralun ${⊢}\left(\forall {x}\in {z}\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in \bigcup {J}\wedge \forall {x}\in \left({I}\setminus {z}\right)\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in \bigcup {J}\right)\to \forall {x}\in \left({z}\cup \left({I}\setminus {z}\right)\right)\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in \bigcup {J}$
82 72 80 81 syl2anc ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\to \forall {x}\in \left({z}\cup \left({I}\setminus {z}\right)\right)\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in \bigcup {J}$
83 undif ${⊢}{z}\subseteq {I}↔{z}\cup \left({I}\setminus {z}\right)={I}$
84 83 biimpi ${⊢}{z}\subseteq {I}\to {z}\cup \left({I}\setminus {z}\right)={I}$
85 84 ad2antrl ${⊢}\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\to {z}\cup \left({I}\setminus {z}\right)={I}$
86 85 raleqdv ${⊢}\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\to \left(\forall {x}\in \left({z}\cup \left({I}\setminus {z}\right)\right)\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in \bigcup {J}↔\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in \bigcup {J}\right)$
87 86 adantr ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\to \left(\forall {x}\in \left({z}\cup \left({I}\setminus {z}\right)\right)\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in \bigcup {J}↔\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in \bigcup {J}\right)$
88 82 87 mpbid ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in \bigcup {J}$
89 22 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\to {I}\in \mathrm{V}$
90 mptelixpg ${⊢}{I}\in \mathrm{V}\to \left(\left({x}\in {I}⟼if\left({x}\in {z},{f}\left({x}\right),{U}\right)\right)\in \underset{{x}\in {I}}{⨉}\bigcup {J}↔\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in \bigcup {J}\right)$
91 89 90 syl ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\to \left(\left({x}\in {I}⟼if\left({x}\in {z},{f}\left({x}\right),{U}\right)\right)\in \underset{{x}\in {I}}{⨉}\bigcup {J}↔\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in \bigcup {J}\right)$
92 88 91 mpbird ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\to \left({x}\in {I}⟼if\left({x}\in {z},{f}\left({x}\right),{U}\right)\right)\in \underset{{x}\in {I}}{⨉}\bigcup {J}$
93 eleq2 ${⊢}{C}=if\left({x}={y},{C},\bigcup {J}\right)\to \left({f}\left({x}\right)\in {C}↔{f}\left({x}\right)\in if\left({x}={y},{C},\bigcup {J}\right)\right)$
94 eleq2 ${⊢}\bigcup {J}=if\left({x}={y},{C},\bigcup {J}\right)\to \left({f}\left({x}\right)\in \bigcup {J}↔{f}\left({x}\right)\in if\left({x}={y},{C},\bigcup {J}\right)\right)$
95 simplrr ${⊢}\left(\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \left({x}\in {z}\wedge {f}\left({x}\right)\in {C}\right)\right)\wedge {x}={y}\right)\to {f}\left({x}\right)\in {C}$
96 68 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \left({x}\in {z}\wedge {f}\left({x}\right)\in {C}\right)\right)\wedge ¬{x}={y}\right)\to {f}\left({x}\right)\in \bigcup {J}$
97 93 94 95 96 ifbothda ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \left({x}\in {z}\wedge {f}\left({x}\right)\in {C}\right)\right)\to {f}\left({x}\right)\in if\left({x}={y},{C},\bigcup {J}\right)$
98 62 97 eqeltrd ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \left({x}\in {z}\wedge {f}\left({x}\right)\in {C}\right)\right)\to if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in if\left({x}={y},{C},\bigcup {J}\right)$
99 98 expr ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge {x}\in {z}\right)\to \left({f}\left({x}\right)\in {C}\to if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in if\left({x}={y},{C},\bigcup {J}\right)\right)$
100 99 ralimdva ${⊢}\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\to \left(\forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\to \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in if\left({x}={y},{C},\bigcup {J}\right)\right)$
101 100 imp ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\to \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in if\left({x}={y},{C},\bigcup {J}\right)$
102 101 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\wedge {y}\in {z}\right)\to \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in if\left({x}={y},{C},\bigcup {J}\right)$
103 77 adantlr ${⊢}\left(\left({\phi }\wedge {y}\in {z}\right)\wedge {x}\in \left({I}\setminus {z}\right)\right)\to {U}\in \bigcup {J}$
104 74 adantl ${⊢}\left(\left({\phi }\wedge {y}\in {z}\right)\wedge {x}\in \left({I}\setminus {z}\right)\right)\to if\left({x}\in {z},{f}\left({x}\right),{U}\right)={U}$
105 incom ${⊢}\left({I}\setminus {z}\right)\cap {z}={z}\cap \left({I}\setminus {z}\right)$
106 disjdif ${⊢}{z}\cap \left({I}\setminus {z}\right)=\varnothing$
107 105 106 eqtri ${⊢}\left({I}\setminus {z}\right)\cap {z}=\varnothing$
108 107 a1i ${⊢}\left(\left({\phi }\wedge {y}\in {z}\right)\wedge {x}\in \left({I}\setminus {z}\right)\right)\to \left({I}\setminus {z}\right)\cap {z}=\varnothing$
109 simpr ${⊢}\left(\left({\phi }\wedge {y}\in {z}\right)\wedge {x}\in \left({I}\setminus {z}\right)\right)\to {x}\in \left({I}\setminus {z}\right)$
110 simplr ${⊢}\left(\left({\phi }\wedge {y}\in {z}\right)\wedge {x}\in \left({I}\setminus {z}\right)\right)\to {y}\in {z}$
111 disjne ${⊢}\left(\left({I}\setminus {z}\right)\cap {z}=\varnothing \wedge {x}\in \left({I}\setminus {z}\right)\wedge {y}\in {z}\right)\to {x}\ne {y}$
112 108 109 110 111 syl3anc ${⊢}\left(\left({\phi }\wedge {y}\in {z}\right)\wedge {x}\in \left({I}\setminus {z}\right)\right)\to {x}\ne {y}$
113 112 neneqd ${⊢}\left(\left({\phi }\wedge {y}\in {z}\right)\wedge {x}\in \left({I}\setminus {z}\right)\right)\to ¬{x}={y}$
114 113 iffalsed ${⊢}\left(\left({\phi }\wedge {y}\in {z}\right)\wedge {x}\in \left({I}\setminus {z}\right)\right)\to if\left({x}={y},{C},\bigcup {J}\right)=\bigcup {J}$
115 103 104 114 3eltr4d ${⊢}\left(\left({\phi }\wedge {y}\in {z}\right)\wedge {x}\in \left({I}\setminus {z}\right)\right)\to if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in if\left({x}={y},{C},\bigcup {J}\right)$
116 115 ralrimiva ${⊢}\left({\phi }\wedge {y}\in {z}\right)\to \forall {x}\in \left({I}\setminus {z}\right)\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in if\left({x}={y},{C},\bigcup {J}\right)$
117 116 adantlr ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge {y}\in {z}\right)\to \forall {x}\in \left({I}\setminus {z}\right)\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in if\left({x}={y},{C},\bigcup {J}\right)$
118 117 adantlr ${⊢}\left(\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\wedge {y}\in {z}\right)\to \forall {x}\in \left({I}\setminus {z}\right)\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in if\left({x}={y},{C},\bigcup {J}\right)$
119 ralun ${⊢}\left(\forall {x}\in {z}\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in if\left({x}={y},{C},\bigcup {J}\right)\wedge \forall {x}\in \left({I}\setminus {z}\right)\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in if\left({x}={y},{C},\bigcup {J}\right)\right)\to \forall {x}\in \left({z}\cup \left({I}\setminus {z}\right)\right)\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in if\left({x}={y},{C},\bigcup {J}\right)$
120 102 118 119 syl2anc ${⊢}\left(\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\wedge {y}\in {z}\right)\to \forall {x}\in \left({z}\cup \left({I}\setminus {z}\right)\right)\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in if\left({x}={y},{C},\bigcup {J}\right)$
121 85 raleqdv ${⊢}\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\to \left(\forall {x}\in \left({z}\cup \left({I}\setminus {z}\right)\right)\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in if\left({x}={y},{C},\bigcup {J}\right)↔\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in if\left({x}={y},{C},\bigcup {J}\right)\right)$
122 121 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\wedge {y}\in {z}\right)\to \left(\forall {x}\in \left({z}\cup \left({I}\setminus {z}\right)\right)\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in if\left({x}={y},{C},\bigcup {J}\right)↔\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in if\left({x}={y},{C},\bigcup {J}\right)\right)$
123 120 122 mpbid ${⊢}\left(\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\wedge {y}\in {z}\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in if\left({x}={y},{C},\bigcup {J}\right)$
124 22 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\wedge {y}\in {z}\right)\to {I}\in \mathrm{V}$
125 mptelixpg ${⊢}{I}\in \mathrm{V}\to \left(\left({x}\in {I}⟼if\left({x}\in {z},{f}\left({x}\right),{U}\right)\right)\in \underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)↔\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in if\left({x}={y},{C},\bigcup {J}\right)\right)$
126 124 125 syl ${⊢}\left(\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\wedge {y}\in {z}\right)\to \left(\left({x}\in {I}⟼if\left({x}\in {z},{f}\left({x}\right),{U}\right)\right)\in \underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)↔\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}if\left({x}\in {z},{f}\left({x}\right),{U}\right)\in if\left({x}={y},{C},\bigcup {J}\right)\right)$
127 123 126 mpbird ${⊢}\left(\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\wedge {y}\in {z}\right)\to \left({x}\in {I}⟼if\left({x}\in {z},{f}\left({x}\right),{U}\right)\right)\in \underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)$
128 127 ralrimiva ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\to \forall {y}\in {z}\phantom{\rule{.4em}{0ex}}\left({x}\in {I}⟼if\left({x}\in {z},{f}\left({x}\right),{U}\right)\right)\in \underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)$
129 mptexg ${⊢}{I}\in \mathrm{V}\to \left({x}\in {I}⟼if\left({x}\in {z},{f}\left({x}\right),{U}\right)\right)\in \mathrm{V}$
130 22 129 syl ${⊢}{\phi }\to \left({x}\in {I}⟼if\left({x}\in {z},{f}\left({x}\right),{U}\right)\right)\in \mathrm{V}$
131 130 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\to \left({x}\in {I}⟼if\left({x}\in {z},{f}\left({x}\right),{U}\right)\right)\in \mathrm{V}$
132 eliin ${⊢}\left({x}\in {I}⟼if\left({x}\in {z},{f}\left({x}\right),{U}\right)\right)\in \mathrm{V}\to \left(\left({x}\in {I}⟼if\left({x}\in {z},{f}\left({x}\right),{U}\right)\right)\in \bigcap _{{y}\in {z}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)↔\forall {y}\in {z}\phantom{\rule{.4em}{0ex}}\left({x}\in {I}⟼if\left({x}\in {z},{f}\left({x}\right),{U}\right)\right)\in \underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)\right)$
133 131 132 syl ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\to \left(\left({x}\in {I}⟼if\left({x}\in {z},{f}\left({x}\right),{U}\right)\right)\in \bigcap _{{y}\in {z}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)↔\forall {y}\in {z}\phantom{\rule{.4em}{0ex}}\left({x}\in {I}⟼if\left({x}\in {z},{f}\left({x}\right),{U}\right)\right)\in \underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)\right)$
134 128 133 mpbird ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\to \left({x}\in {I}⟼if\left({x}\in {z},{f}\left({x}\right),{U}\right)\right)\in \bigcap _{{y}\in {z}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)$
135 92 134 elind ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\to \left({x}\in {I}⟼if\left({x}\in {z},{f}\left({x}\right),{U}\right)\right)\in \left(\underset{{x}\in {I}}{⨉}\bigcup {J}\cap \bigcap _{{y}\in {z}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)\right)$
136 135 ne0d ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\to \underset{{x}\in {I}}{⨉}\bigcup {J}\cap \bigcap _{{y}\in {z}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)\ne \varnothing$
137 60 136 eqnetrd ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\to \bigcup {\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)\cap \bigcap _{{y}\in {z}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)\ne \varnothing$
138 137 adantrl ${⊢}\left(\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\wedge \left({f}:{z}⟶\mathrm{V}\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\right)\to \bigcup {\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)\cap \bigcap _{{y}\in {z}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)\ne \varnothing$
139 57 138 exlimddv ${⊢}\left({\phi }\wedge \left({z}\subseteq {I}\wedge {z}\in \mathrm{Fin}\right)\right)\to \bigcup {\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)\cap \bigcap _{{y}\in {z}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)\ne \varnothing$
140 28 6 33 139 cmpfiiin ${⊢}{\phi }\to \bigcup {\prod }_{𝑡}\left(\left({x}\in {I}⟼{J}\right)\right)\cap \bigcap _{{y}\in {I}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)\ne \varnothing$
141 27 140 eqnetrd ${⊢}{\phi }\to \underset{{x}\in {I}}{⨉}\bigcup {J}\cap \bigcap _{{y}\in {I}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{C},\bigcup {J}\right)\ne \varnothing$
142 12 141 eqnetrd ${⊢}{\phi }\to \underset{{x}\in {I}}{⨉}{C}\ne \varnothing$
143 n0 ${⊢}\underset{{x}\in {I}}{⨉}{C}\ne \varnothing ↔\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in \underset{{x}\in {I}}{⨉}{C}$
144 142 143 sylib ${⊢}{\phi }\to \exists {y}\phantom{\rule{.4em}{0ex}}{y}\in \underset{{x}\in {I}}{⨉}{C}$
145 elixp2 ${⊢}{y}\in \underset{{x}\in {I}}{⨉}{C}↔\left({y}\in \mathrm{V}\wedge {y}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{y}\left({x}\right)\in {C}\right)$
146 145 simp3bi ${⊢}{y}\in \underset{{x}\in {I}}{⨉}{C}\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{y}\left({x}\right)\in {C}$
147 f1ocnv ${⊢}{B}:{S}\underset{1-1 onto}{⟶}{C}\to {{B}}^{-1}:{C}\underset{1-1 onto}{⟶}{S}$
148 f1of ${⊢}{{B}}^{-1}:{C}\underset{1-1 onto}{⟶}{S}\to {{B}}^{-1}:{C}⟶{S}$
149 ffvelrn ${⊢}\left({{B}}^{-1}:{C}⟶{S}\wedge {y}\left({x}\right)\in {C}\right)\to {{B}}^{-1}\left({y}\left({x}\right)\right)\in {S}$
150 149 ex ${⊢}{{B}}^{-1}:{C}⟶{S}\to \left({y}\left({x}\right)\in {C}\to {{B}}^{-1}\left({y}\left({x}\right)\right)\in {S}\right)$
151 4 147 148 150 4syl ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to \left({y}\left({x}\right)\in {C}\to {{B}}^{-1}\left({y}\left({x}\right)\right)\in {S}\right)$
152 151 ralimdva ${⊢}{\phi }\to \left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{y}\left({x}\right)\in {C}\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{{B}}^{-1}\left({y}\left({x}\right)\right)\in {S}\right)$
153 152 imp ${⊢}\left({\phi }\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{y}\left({x}\right)\in {C}\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{{B}}^{-1}\left({y}\left({x}\right)\right)\in {S}$
154 146 153 sylan2 ${⊢}\left({\phi }\wedge {y}\in \underset{{x}\in {I}}{⨉}{C}\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{{B}}^{-1}\left({y}\left({x}\right)\right)\in {S}$
155 mptelixpg ${⊢}{I}\in \mathrm{V}\to \left(\left({x}\in {I}⟼{{B}}^{-1}\left({y}\left({x}\right)\right)\right)\in \underset{{x}\in {I}}{⨉}{S}↔\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{{B}}^{-1}\left({y}\left({x}\right)\right)\in {S}\right)$
156 22 155 syl ${⊢}{\phi }\to \left(\left({x}\in {I}⟼{{B}}^{-1}\left({y}\left({x}\right)\right)\right)\in \underset{{x}\in {I}}{⨉}{S}↔\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{{B}}^{-1}\left({y}\left({x}\right)\right)\in {S}\right)$
157 156 adantr ${⊢}\left({\phi }\wedge {y}\in \underset{{x}\in {I}}{⨉}{C}\right)\to \left(\left({x}\in {I}⟼{{B}}^{-1}\left({y}\left({x}\right)\right)\right)\in \underset{{x}\in {I}}{⨉}{S}↔\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{{B}}^{-1}\left({y}\left({x}\right)\right)\in {S}\right)$
158 154 157 mpbird ${⊢}\left({\phi }\wedge {y}\in \underset{{x}\in {I}}{⨉}{C}\right)\to \left({x}\in {I}⟼{{B}}^{-1}\left({y}\left({x}\right)\right)\right)\in \underset{{x}\in {I}}{⨉}{S}$
159 158 ne0d ${⊢}\left({\phi }\wedge {y}\in \underset{{x}\in {I}}{⨉}{C}\right)\to \underset{{x}\in {I}}{⨉}{S}\ne \varnothing$
160 144 159 exlimddv ${⊢}{\phi }\to \underset{{x}\in {I}}{⨉}{S}\ne \varnothing$