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 dfac10 
 |-  ( CHOICE <-> dom card = _V )
11 10 birani 
 |-  ( ( CHOICE /\ f : dom f --> Comp ) -> dom card = _V )
12 6 11 eleqtrrid 
 |-  ( ( CHOICE /\ f : dom f --> Comp ) -> U. ( Xt_ ` f ) e. dom card )
13 9 12 elind 
 |-  ( ( CHOICE /\ f : dom f --> Comp ) -> U. ( Xt_ ` f ) e. ( UFL i^i dom card ) )
14 eqid 
 |-  ( Xt_ ` f ) = ( Xt_ ` f )
15 eqid 
 |-  U. ( Xt_ ` f ) = U. ( Xt_ ` f )
16 14 15 ptcmpg 
 |-  ( ( dom f e. _V /\ f : dom f --> Comp /\ U. ( Xt_ ` f ) e. ( UFL i^i dom card ) ) -> ( Xt_ ` f ) e. Comp )
17 3 4 13 16 syl3anc 
 |-  ( ( CHOICE /\ f : dom f --> Comp ) -> ( Xt_ ` f ) e. Comp )
18 17 ex 
 |-  ( CHOICE -> ( f : dom f --> Comp -> ( Xt_ ` f ) e. Comp ) )
19 18 alrimiv 
 |-  ( CHOICE -> A. f ( f : dom f --> Comp -> ( Xt_ ` f ) e. Comp ) )
20 fvex 
 |-  ( g ` y ) e. _V
21 kelac2lem 
 |-  ( ( g ` y ) e. _V -> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) e. Comp )
22 20 21 mp1i 
 |-  ( ( ( Fun g /\ (/) e/ ran g ) /\ y e. dom g ) -> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) e. Comp )
23 22 fmpttd 
 |-  ( ( Fun g /\ (/) e/ ran g ) -> ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) : dom g --> Comp )
24 23 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 )
25 vex 
 |-  g e. _V
26 25 dmex 
 |-  dom g e. _V
27 26 mptex 
 |-  ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) e. _V
28 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 ) } } ) ) )
29 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 ) } } ) ) )
30 28 29 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 ) )
31 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 ) } } ) ) ) )
32 31 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 ) )
33 30 32 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 ) ) )
34 27 33 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 ) )
35 24 34 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 ) )
36 fvex 
 |-  ( g ` x ) e. _V
37 36 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 )
38 df-nel 
 |-  ( (/) e/ ran g <-> -. (/) e. ran g )
39 38 biimpi 
 |-  ( (/) e/ ran g -> -. (/) e. ran g )
40 39 ad2antlr 
 |-  ( ( ( Fun g /\ (/) e/ ran g ) /\ x e. dom g ) -> -. (/) e. ran g )
41 fvelrn 
 |-  ( ( Fun g /\ x e. dom g ) -> ( g ` x ) e. ran g )
42 41 adantlr 
 |-  ( ( ( Fun g /\ (/) e/ ran g ) /\ x e. dom g ) -> ( g ` x ) e. ran g )
43 eleq1 
 |-  ( ( g ` x ) = (/) -> ( ( g ` x ) e. ran g <-> (/) e. ran g ) )
44 42 43 syl5ibcom 
 |-  ( ( ( Fun g /\ (/) e/ ran g ) /\ x e. dom g ) -> ( ( g ` x ) = (/) -> (/) e. ran g ) )
45 44 necon3bd 
 |-  ( ( ( Fun g /\ (/) e/ ran g ) /\ x e. dom g ) -> ( -. (/) e. ran g -> ( g ` x ) =/= (/) ) )
46 40 45 mpd 
 |-  ( ( ( Fun g /\ (/) e/ ran g ) /\ x e. dom g ) -> ( g ` x ) =/= (/) )
47 46 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 ) =/= (/) )
48 fveq2 
 |-  ( y = x -> ( g ` y ) = ( g ` x ) )
49 48 unieqd 
 |-  ( y = x -> U. ( g ` y ) = U. ( g ` x ) )
50 49 pweqd 
 |-  ( y = x -> ~P U. ( g ` y ) = ~P U. ( g ` x ) )
51 50 sneqd 
 |-  ( y = x -> { ~P U. ( g ` y ) } = { ~P U. ( g ` x ) } )
52 48 51 preq12d 
 |-  ( y = x -> { ( g ` y ) , { ~P U. ( g ` y ) } } = { ( g ` x ) , { ~P U. ( g ` x ) } } )
53 52 fveq2d 
 |-  ( y = x -> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) = ( topGen ` { ( g ` x ) , { ~P U. ( g ` x ) } } ) )
54 53 cbvmptv 
 |-  ( y e. dom g |-> ( topGen ` { ( g ` y ) , { ~P U. ( g ` y ) } } ) ) = ( x e. dom g |-> ( topGen ` { ( g ` x ) , { ~P U. ( g ` x ) } } ) )
55 54 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 ) } } ) ) )
56 55 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 )
57 56 bilani 
 |-  ( ( ( 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 )
58 37 47 57 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 ) =/= (/) )
59 58 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 ) =/= (/) ) )
60 35 59 syldc 
 |-  ( A. f ( f : dom f --> Comp -> ( Xt_ ` f ) e. Comp ) -> ( ( Fun g /\ (/) e/ ran g ) -> X_ x e. dom g ( g ` x ) =/= (/) ) )
61 60 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 ) =/= (/) ) )
62 dfac9 
 |-  ( CHOICE <-> A. g ( ( Fun g /\ (/) e/ ran g ) -> X_ x e. dom g ( g ` x ) =/= (/) ) )
63 61 62 sylibr 
 |-  ( A. f ( f : dom f --> Comp -> ( Xt_ ` f ) e. Comp ) -> CHOICE )
64 19 63 impbii 
 |-  ( CHOICE <-> A. f ( f : dom f --> Comp -> ( Xt_ ` f ) e. Comp ) )