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 
|- ( CHOICE <-> A. f ( f : dom f --> Comp -> ( Xt_ ` f ) e. Comp ) )

Proof

Step Hyp Ref Expression
1 vex 
 |-  f e. _V
2 1 dmex 
 |-  dom f e. _V
3 2 a1i 
 |-  ( ( CHOICE /\ f : dom f --> Comp ) -> dom f e. _V )
4 simpr 
 |-  ( ( CHOICE /\ f : dom f --> Comp ) -> f : dom f --> Comp )
5 fvex 
 |-  ( Xt_ ` f ) e. _V
6 5 uniex 
 |-  U. ( Xt_ ` f ) e. _V
7 acufl 
 |-  ( CHOICE -> UFL = _V )
8 7 adantr 
 |-  ( ( CHOICE /\ f : dom f --> Comp ) -> UFL = _V )
9 6 8 eleqtrrid 
 |-  ( ( CHOICE /\ f : dom f --> Comp ) -> U. ( Xt_ ` f ) e. UFL )
10 simpl 
 |-  ( ( CHOICE /\ f : dom f --> Comp ) -> CHOICE )
11 dfac10 
 |-  ( CHOICE <-> dom card = _V )
12 10 11 sylib 
 |-  ( ( CHOICE /\ f : dom f --> Comp ) -> dom card = _V )
13 6 12 eleqtrrid 
 |-  ( ( CHOICE /\ f : dom f --> Comp ) -> U. ( Xt_ ` f ) e. dom card )
14 9 13 elind 
 |-  ( ( CHOICE /\ f : dom f --> Comp ) -> U. ( Xt_ ` f ) e. ( UFL i^i dom card ) )
15 eqid 
 |-  ( Xt_ ` f ) = ( Xt_ ` f )
16 eqid 
 |-  U. ( Xt_ ` f ) = U. ( Xt_ ` f )
17 15 16 ptcmpg 
 |-  ( ( dom f e. _V /\ f : dom f --> Comp /\ U. ( Xt_ ` f ) e. ( UFL i^i dom card ) ) -> ( Xt_ ` f ) e. Comp )
18 3 4 14 17 syl3anc 
 |-  ( ( CHOICE /\ f : dom f --> Comp ) -> ( Xt_ ` f ) e. Comp )
19 18 ex 
 |-  ( CHOICE -> ( f : dom f --> Comp -> ( Xt_ ` f ) e. Comp ) )
20 19 alrimiv 
 |-  ( CHOICE -> A. f ( f : dom f --> Comp -> ( Xt_ ` f ) e. Comp ) )
21 fvex 
 |-  ( g ` y ) e. _V
22 kelac2lem 
 |-  ( ( g ` y ) e. _V -> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) e. Comp )
23 21 22 mp1i 
 |-  ( ( ( Fun g /\ (/) e/ ran g ) /\ y e. dom g ) -> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) e. Comp )
24 23 fmpttd 
 |-  ( ( Fun g /\ (/) e/ ran g ) -> ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) : dom g --> Comp )
25 24 ffdmd 
 |-  ( ( Fun g /\ (/) e/ ran g ) -> ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) : dom ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) --> Comp )
26 vex 
 |-  g e. _V
27 26 dmex 
 |-  dom g e. _V
28 27 mptex 
 |-  ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) e. _V
29 id 
 |-  ( f = ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) -> f = ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) )
30 dmeq 
 |-  ( f = ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) -> dom f = dom ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) )
31 29 30 feq12d 
 |-  ( f = ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) -> ( f : dom f --> Comp <-> ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) : dom ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) --> Comp ) )
32 fveq2 
 |-  ( f = ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) -> ( Xt_ ` f ) = ( Xt_ ` ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) ) )
33 32 eleq1d 
 |-  ( f = ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) -> ( ( Xt_ ` f ) e. Comp <-> ( Xt_ ` ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) ) e. Comp ) )
34 31 33 imbi12d 
 |-  ( f = ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) -> ( ( f : dom f --> Comp -> ( Xt_ ` f ) e. Comp ) <-> ( ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) : dom ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) --> Comp -> ( Xt_ ` ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) ) e. Comp ) ) )
35 28 34 spcv 
 |-  ( A. f ( f : dom f --> Comp -> ( Xt_ ` f ) e. Comp ) -> ( ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) : dom ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) --> Comp -> ( Xt_ ` ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) ) e. Comp ) )
36 25 35 syl5com 
 |-  ( ( Fun g /\ (/) e/ ran g ) -> ( A. f ( f : dom f --> Comp -> ( Xt_ ` f ) e. Comp ) -> ( Xt_ ` ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) ) e. Comp ) )
37 fvex 
 |-  ( g ` x ) e. _V
38 37 a1i 
 |-  ( ( ( ( Fun g /\ (/) e/ ran g ) /\ ( Xt_ ` ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) ) e. Comp ) /\ x e. dom g ) -> ( g ` x ) e. _V )
39 df-nel 
 |-  ( (/) e/ ran g <-> -. (/) e. ran g )
40 39 biimpi 
 |-  ( (/) e/ ran g -> -. (/) e. ran g )
41 40 ad2antlr 
 |-  ( ( ( Fun g /\ (/) e/ ran g ) /\ x e. dom g ) -> -. (/) e. ran g )
42 fvelrn 
 |-  ( ( Fun g /\ x e. dom g ) -> ( g ` x ) e. ran g )
43 42 adantlr 
 |-  ( ( ( Fun g /\ (/) e/ ran g ) /\ x e. dom g ) -> ( g ` x ) e. ran g )
44 eleq1 
 |-  ( ( g ` x ) = (/) -> ( ( g ` x ) e. ran g <-> (/) e. ran g ) )
45 43 44 syl5ibcom 
 |-  ( ( ( Fun g /\ (/) e/ ran g ) /\ x e. dom g ) -> ( ( g ` x ) = (/) -> (/) e. ran g ) )
46 45 necon3bd 
 |-  ( ( ( Fun g /\ (/) e/ ran g ) /\ x e. dom g ) -> ( -. (/) e. ran g -> ( g ` x ) =/= (/) ) )
47 41 46 mpd 
 |-  ( ( ( Fun g /\ (/) e/ ran g ) /\ x e. dom g ) -> ( g ` x ) =/= (/) )
48 47 adantlr 
 |-  ( ( ( ( Fun g /\ (/) e/ ran g ) /\ ( Xt_ ` ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) ) e. Comp ) /\ x e. dom g ) -> ( g ` x ) =/= (/) )
49 fveq2 
 |-  ( y = x -> ( g ` y ) = ( g ` x ) )
50 49 unieqd 
 |-  ( y = x -> U. ( g ` y ) = U. ( g ` x ) )
51 50 pweqd 
 |-  ( y = x -> ~P U. ( g ` y ) = ~P U. ( g ` x ) )
52 51 sneqd 
 |-  ( y = x -> { ~P U. ( g ` y ) } = { ~P U. ( g ` x ) } )
53 49 52 preq12d 
 |-  ( y = x -> { ( g ` y ) , { ~P U. ( g ` y ) } } = { ( g ` x ) , { ~P U. ( g ` x ) } } )
54 53 fveq2d 
 |-  ( y = x -> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) = ( topGen ` { ( g ` x ) , { ~P U. ( g ` x ) } } ) )
55 54 cbvmptv 
 |-  ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) = ( x e. dom g |-> ( topGen ` { ( g ` x ) , { ~P U. ( g ` x ) } } ) )
56 55 fveq2i 
 |-  ( Xt_ ` ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) ) = ( Xt_ ` ( x e. dom g |-> ( topGen ` { ( g ` x ) , { ~P U. ( g ` x ) } } ) ) )
57 56 eleq1i 
 |-  ( ( Xt_ ` ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) ) e. Comp <-> ( Xt_ ` ( x e. dom g |-> ( topGen ` { ( g ` x ) , { ~P U. ( g ` x ) } } ) ) ) e. Comp )
58 57 biimpi 
 |-  ( ( Xt_ ` ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) ) e. Comp -> ( Xt_ ` ( x e. dom g |-> ( topGen ` { ( g ` x ) , { ~P U. ( g ` x ) } } ) ) ) e. Comp )
59 58 adantl 
 |-  ( ( ( Fun g /\ (/) e/ ran g ) /\ ( Xt_ ` ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) ) e. Comp ) -> ( Xt_ ` ( x e. dom g |-> ( topGen ` { ( g ` x ) , { ~P U. ( g ` x ) } } ) ) ) e. Comp )
60 38 48 59 kelac2 
 |-  ( ( ( Fun g /\ (/) e/ ran g ) /\ ( Xt_ ` ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) ) e. Comp ) -> X_ x e. dom g ( g ` x ) =/= (/) )
61 60 ex 
 |-  ( ( Fun g /\ (/) e/ ran g ) -> ( ( Xt_ ` ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) ) e. Comp -> X_ x e. dom g ( g ` x ) =/= (/) ) )
62 36 61 syldc 
 |-  ( A. f ( f : dom f --> Comp -> ( Xt_ ` f ) e. Comp ) -> ( ( Fun g /\ (/) e/ ran g ) -> X_ x e. dom g ( g ` x ) =/= (/) ) )
63 62 alrimiv 
 |-  ( A. f ( f : dom f --> Comp -> ( Xt_ ` f ) e. Comp ) -> A. g ( ( Fun g /\ (/) e/ ran g ) -> X_ x e. dom g ( g ` x ) =/= (/) ) )
64 dfac9 
 |-  ( CHOICE <-> A. g ( ( Fun g /\ (/) e/ ran g ) -> X_ x e. dom g ( g ` x ) =/= (/) ) )
65 63 64 sylibr 
 |-  ( A. f ( f : dom f --> Comp -> ( Xt_ ` f ) e. Comp ) -> CHOICE )
66 20 65 impbii 
 |-  ( CHOICE <-> A. f ( f : dom f --> Comp -> ( Xt_ ` f ) e. Comp ) )