# Metamath Proof Explorer

## Theorem dfac21

Description: Tychonoff's theorem is a choice equivalent. Definition AC21 of Schechter p. 461. (Contributed by Stefan O'Rear, 22-Feb-2015) (Revised by Mario Carneiro, 27-Aug-2015)

Ref Expression
Assertion dfac21 ${⊢}\mathrm{CHOICE}↔\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}:\mathrm{dom}{f}⟶\mathrm{Comp}\to {\prod }_{𝑡}\left({f}\right)\in \mathrm{Comp}\right)$

### Proof

Step Hyp Ref Expression
1 vex ${⊢}{f}\in \mathrm{V}$
2 1 dmex ${⊢}\mathrm{dom}{f}\in \mathrm{V}$
3 2 a1i ${⊢}\left(\mathrm{CHOICE}\wedge {f}:\mathrm{dom}{f}⟶\mathrm{Comp}\right)\to \mathrm{dom}{f}\in \mathrm{V}$
4 simpr ${⊢}\left(\mathrm{CHOICE}\wedge {f}:\mathrm{dom}{f}⟶\mathrm{Comp}\right)\to {f}:\mathrm{dom}{f}⟶\mathrm{Comp}$
5 fvex ${⊢}{\prod }_{𝑡}\left({f}\right)\in \mathrm{V}$
6 5 uniex ${⊢}\bigcup {\prod }_{𝑡}\left({f}\right)\in \mathrm{V}$
7 acufl ${⊢}\mathrm{CHOICE}\to \mathrm{UFL}=\mathrm{V}$
8 7 adantr ${⊢}\left(\mathrm{CHOICE}\wedge {f}:\mathrm{dom}{f}⟶\mathrm{Comp}\right)\to \mathrm{UFL}=\mathrm{V}$
9 6 8 eleqtrrid ${⊢}\left(\mathrm{CHOICE}\wedge {f}:\mathrm{dom}{f}⟶\mathrm{Comp}\right)\to \bigcup {\prod }_{𝑡}\left({f}\right)\in \mathrm{UFL}$
10 simpl ${⊢}\left(\mathrm{CHOICE}\wedge {f}:\mathrm{dom}{f}⟶\mathrm{Comp}\right)\to \mathrm{CHOICE}$
11 dfac10 ${⊢}\mathrm{CHOICE}↔\mathrm{dom}\mathrm{card}=\mathrm{V}$
12 10 11 sylib ${⊢}\left(\mathrm{CHOICE}\wedge {f}:\mathrm{dom}{f}⟶\mathrm{Comp}\right)\to \mathrm{dom}\mathrm{card}=\mathrm{V}$
13 6 12 eleqtrrid ${⊢}\left(\mathrm{CHOICE}\wedge {f}:\mathrm{dom}{f}⟶\mathrm{Comp}\right)\to \bigcup {\prod }_{𝑡}\left({f}\right)\in \mathrm{dom}\mathrm{card}$
14 9 13 elind ${⊢}\left(\mathrm{CHOICE}\wedge {f}:\mathrm{dom}{f}⟶\mathrm{Comp}\right)\to \bigcup {\prod }_{𝑡}\left({f}\right)\in \left(\mathrm{UFL}\cap \mathrm{dom}\mathrm{card}\right)$
15 eqid ${⊢}{\prod }_{𝑡}\left({f}\right)={\prod }_{𝑡}\left({f}\right)$
16 eqid ${⊢}\bigcup {\prod }_{𝑡}\left({f}\right)=\bigcup {\prod }_{𝑡}\left({f}\right)$
17 15 16 ptcmpg ${⊢}\left(\mathrm{dom}{f}\in \mathrm{V}\wedge {f}:\mathrm{dom}{f}⟶\mathrm{Comp}\wedge \bigcup {\prod }_{𝑡}\left({f}\right)\in \left(\mathrm{UFL}\cap \mathrm{dom}\mathrm{card}\right)\right)\to {\prod }_{𝑡}\left({f}\right)\in \mathrm{Comp}$
18 3 4 14 17 syl3anc ${⊢}\left(\mathrm{CHOICE}\wedge {f}:\mathrm{dom}{f}⟶\mathrm{Comp}\right)\to {\prod }_{𝑡}\left({f}\right)\in \mathrm{Comp}$
19 18 ex ${⊢}\mathrm{CHOICE}\to \left({f}:\mathrm{dom}{f}⟶\mathrm{Comp}\to {\prod }_{𝑡}\left({f}\right)\in \mathrm{Comp}\right)$
20 19 alrimiv ${⊢}\mathrm{CHOICE}\to \forall {f}\phantom{\rule{.4em}{0ex}}\left({f}:\mathrm{dom}{f}⟶\mathrm{Comp}\to {\prod }_{𝑡}\left({f}\right)\in \mathrm{Comp}\right)$
21 fvex ${⊢}{g}\left({y}\right)\in \mathrm{V}$
22 kelac2lem ${⊢}{g}\left({y}\right)\in \mathrm{V}\to \mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\in \mathrm{Comp}$
23 21 22 mp1i ${⊢}\left(\left(\mathrm{Fun}{g}\wedge \varnothing \notin \mathrm{ran}{g}\right)\wedge {y}\in \mathrm{dom}{g}\right)\to \mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\in \mathrm{Comp}$
24 23 fmpttd ${⊢}\left(\mathrm{Fun}{g}\wedge \varnothing \notin \mathrm{ran}{g}\right)\to \left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right):\mathrm{dom}{g}⟶\mathrm{Comp}$
25 24 ffdmd ${⊢}\left(\mathrm{Fun}{g}\wedge \varnothing \notin \mathrm{ran}{g}\right)\to \left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right):\mathrm{dom}\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)⟶\mathrm{Comp}$
26 vex ${⊢}{g}\in \mathrm{V}$
27 26 dmex ${⊢}\mathrm{dom}{g}\in \mathrm{V}$
28 27 mptex ${⊢}\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)\in \mathrm{V}$
29 id ${⊢}{f}=\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)\to {f}=\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)$
30 dmeq ${⊢}{f}=\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)\to \mathrm{dom}{f}=\mathrm{dom}\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)$
31 29 30 feq12d ${⊢}{f}=\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)\to \left({f}:\mathrm{dom}{f}⟶\mathrm{Comp}↔\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right):\mathrm{dom}\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)⟶\mathrm{Comp}\right)$
32 fveq2 ${⊢}{f}=\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)\to {\prod }_{𝑡}\left({f}\right)={\prod }_{𝑡}\left(\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)\right)$
33 32 eleq1d ${⊢}{f}=\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)\to \left({\prod }_{𝑡}\left({f}\right)\in \mathrm{Comp}↔{\prod }_{𝑡}\left(\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)\right)\in \mathrm{Comp}\right)$
34 31 33 imbi12d ${⊢}{f}=\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)\to \left(\left({f}:\mathrm{dom}{f}⟶\mathrm{Comp}\to {\prod }_{𝑡}\left({f}\right)\in \mathrm{Comp}\right)↔\left(\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right):\mathrm{dom}\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)⟶\mathrm{Comp}\to {\prod }_{𝑡}\left(\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)\right)\in \mathrm{Comp}\right)\right)$
35 28 34 spcv ${⊢}\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}:\mathrm{dom}{f}⟶\mathrm{Comp}\to {\prod }_{𝑡}\left({f}\right)\in \mathrm{Comp}\right)\to \left(\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right):\mathrm{dom}\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)⟶\mathrm{Comp}\to {\prod }_{𝑡}\left(\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)\right)\in \mathrm{Comp}\right)$
36 25 35 syl5com ${⊢}\left(\mathrm{Fun}{g}\wedge \varnothing \notin \mathrm{ran}{g}\right)\to \left(\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}:\mathrm{dom}{f}⟶\mathrm{Comp}\to {\prod }_{𝑡}\left({f}\right)\in \mathrm{Comp}\right)\to {\prod }_{𝑡}\left(\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)\right)\in \mathrm{Comp}\right)$
37 fvex ${⊢}{g}\left({x}\right)\in \mathrm{V}$
38 37 a1i ${⊢}\left(\left(\left(\mathrm{Fun}{g}\wedge \varnothing \notin \mathrm{ran}{g}\right)\wedge {\prod }_{𝑡}\left(\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)\right)\in \mathrm{Comp}\right)\wedge {x}\in \mathrm{dom}{g}\right)\to {g}\left({x}\right)\in \mathrm{V}$
39 df-nel ${⊢}\varnothing \notin \mathrm{ran}{g}↔¬\varnothing \in \mathrm{ran}{g}$
40 39 biimpi ${⊢}\varnothing \notin \mathrm{ran}{g}\to ¬\varnothing \in \mathrm{ran}{g}$
41 40 ad2antlr ${⊢}\left(\left(\mathrm{Fun}{g}\wedge \varnothing \notin \mathrm{ran}{g}\right)\wedge {x}\in \mathrm{dom}{g}\right)\to ¬\varnothing \in \mathrm{ran}{g}$
42 fvelrn ${⊢}\left(\mathrm{Fun}{g}\wedge {x}\in \mathrm{dom}{g}\right)\to {g}\left({x}\right)\in \mathrm{ran}{g}$
43 42 adantlr ${⊢}\left(\left(\mathrm{Fun}{g}\wedge \varnothing \notin \mathrm{ran}{g}\right)\wedge {x}\in \mathrm{dom}{g}\right)\to {g}\left({x}\right)\in \mathrm{ran}{g}$
44 eleq1 ${⊢}{g}\left({x}\right)=\varnothing \to \left({g}\left({x}\right)\in \mathrm{ran}{g}↔\varnothing \in \mathrm{ran}{g}\right)$
45 43 44 syl5ibcom ${⊢}\left(\left(\mathrm{Fun}{g}\wedge \varnothing \notin \mathrm{ran}{g}\right)\wedge {x}\in \mathrm{dom}{g}\right)\to \left({g}\left({x}\right)=\varnothing \to \varnothing \in \mathrm{ran}{g}\right)$
46 45 necon3bd ${⊢}\left(\left(\mathrm{Fun}{g}\wedge \varnothing \notin \mathrm{ran}{g}\right)\wedge {x}\in \mathrm{dom}{g}\right)\to \left(¬\varnothing \in \mathrm{ran}{g}\to {g}\left({x}\right)\ne \varnothing \right)$
47 41 46 mpd ${⊢}\left(\left(\mathrm{Fun}{g}\wedge \varnothing \notin \mathrm{ran}{g}\right)\wedge {x}\in \mathrm{dom}{g}\right)\to {g}\left({x}\right)\ne \varnothing$
48 47 adantlr ${⊢}\left(\left(\left(\mathrm{Fun}{g}\wedge \varnothing \notin \mathrm{ran}{g}\right)\wedge {\prod }_{𝑡}\left(\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)\right)\in \mathrm{Comp}\right)\wedge {x}\in \mathrm{dom}{g}\right)\to {g}\left({x}\right)\ne \varnothing$
49 fveq2 ${⊢}{y}={x}\to {g}\left({y}\right)={g}\left({x}\right)$
50 49 unieqd ${⊢}{y}={x}\to \bigcup {g}\left({y}\right)=\bigcup {g}\left({x}\right)$
51 50 pweqd ${⊢}{y}={x}\to 𝒫\bigcup {g}\left({y}\right)=𝒫\bigcup {g}\left({x}\right)$
52 51 sneqd ${⊢}{y}={x}\to \left\{𝒫\bigcup {g}\left({y}\right)\right\}=\left\{𝒫\bigcup {g}\left({x}\right)\right\}$
53 49 52 preq12d ${⊢}{y}={x}\to \left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}=\left\{{g}\left({x}\right),\left\{𝒫\bigcup {g}\left({x}\right)\right\}\right\}$
54 53 fveq2d ${⊢}{y}={x}\to \mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)=\mathrm{topGen}\left(\left\{{g}\left({x}\right),\left\{𝒫\bigcup {g}\left({x}\right)\right\}\right\}\right)$
55 54 cbvmptv ${⊢}\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)=\left({x}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({x}\right),\left\{𝒫\bigcup {g}\left({x}\right)\right\}\right\}\right)\right)$
56 55 fveq2i ${⊢}{\prod }_{𝑡}\left(\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)\right)={\prod }_{𝑡}\left(\left({x}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({x}\right),\left\{𝒫\bigcup {g}\left({x}\right)\right\}\right\}\right)\right)\right)$
57 56 eleq1i ${⊢}{\prod }_{𝑡}\left(\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)\right)\in \mathrm{Comp}↔{\prod }_{𝑡}\left(\left({x}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({x}\right),\left\{𝒫\bigcup {g}\left({x}\right)\right\}\right\}\right)\right)\right)\in \mathrm{Comp}$
58 57 biimpi ${⊢}{\prod }_{𝑡}\left(\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)\right)\in \mathrm{Comp}\to {\prod }_{𝑡}\left(\left({x}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({x}\right),\left\{𝒫\bigcup {g}\left({x}\right)\right\}\right\}\right)\right)\right)\in \mathrm{Comp}$
59 58 adantl ${⊢}\left(\left(\mathrm{Fun}{g}\wedge \varnothing \notin \mathrm{ran}{g}\right)\wedge {\prod }_{𝑡}\left(\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)\right)\in \mathrm{Comp}\right)\to {\prod }_{𝑡}\left(\left({x}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({x}\right),\left\{𝒫\bigcup {g}\left({x}\right)\right\}\right\}\right)\right)\right)\in \mathrm{Comp}$
60 38 48 59 kelac2 ${⊢}\left(\left(\mathrm{Fun}{g}\wedge \varnothing \notin \mathrm{ran}{g}\right)\wedge {\prod }_{𝑡}\left(\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)\right)\in \mathrm{Comp}\right)\to \underset{{x}\in \mathrm{dom}{g}}{⨉}{g}\left({x}\right)\ne \varnothing$
61 60 ex ${⊢}\left(\mathrm{Fun}{g}\wedge \varnothing \notin \mathrm{ran}{g}\right)\to \left({\prod }_{𝑡}\left(\left({y}\in \mathrm{dom}{g}⟼\mathrm{topGen}\left(\left\{{g}\left({y}\right),\left\{𝒫\bigcup {g}\left({y}\right)\right\}\right\}\right)\right)\right)\in \mathrm{Comp}\to \underset{{x}\in \mathrm{dom}{g}}{⨉}{g}\left({x}\right)\ne \varnothing \right)$
62 36 61 syldc ${⊢}\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}:\mathrm{dom}{f}⟶\mathrm{Comp}\to {\prod }_{𝑡}\left({f}\right)\in \mathrm{Comp}\right)\to \left(\left(\mathrm{Fun}{g}\wedge \varnothing \notin \mathrm{ran}{g}\right)\to \underset{{x}\in \mathrm{dom}{g}}{⨉}{g}\left({x}\right)\ne \varnothing \right)$
63 62 alrimiv ${⊢}\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}:\mathrm{dom}{f}⟶\mathrm{Comp}\to {\prod }_{𝑡}\left({f}\right)\in \mathrm{Comp}\right)\to \forall {g}\phantom{\rule{.4em}{0ex}}\left(\left(\mathrm{Fun}{g}\wedge \varnothing \notin \mathrm{ran}{g}\right)\to \underset{{x}\in \mathrm{dom}{g}}{⨉}{g}\left({x}\right)\ne \varnothing \right)$
64 dfac9 ${⊢}\mathrm{CHOICE}↔\forall {g}\phantom{\rule{.4em}{0ex}}\left(\left(\mathrm{Fun}{g}\wedge \varnothing \notin \mathrm{ran}{g}\right)\to \underset{{x}\in \mathrm{dom}{g}}{⨉}{g}\left({x}\right)\ne \varnothing \right)$
65 63 64 sylibr ${⊢}\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}:\mathrm{dom}{f}⟶\mathrm{Comp}\to {\prod }_{𝑡}\left({f}\right)\in \mathrm{Comp}\right)\to \mathrm{CHOICE}$
66 20 65 impbii ${⊢}\mathrm{CHOICE}↔\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}:\mathrm{dom}{f}⟶\mathrm{Comp}\to {\prod }_{𝑡}\left({f}\right)\in \mathrm{Comp}\right)$