Metamath Proof Explorer

Theorem ttac

Description: Tarski's theorem about choice: infxpidm is equivalent to ax-ac . (Contributed by Stefan O'Rear, 4-Nov-2014) (Proof shortened by Stefan O'Rear, 10-Jul-2015)

Ref Expression
Assertion ttac 
|- ( CHOICE <-> A. c ( _om ~<_ c -> ( c X. c ) ~~ c ) )

Proof

Step Hyp Ref Expression
1 dfac10 
 |-  ( CHOICE <-> dom card = _V )
2 vex 
 |-  c e. _V
3 eleq2 
 |-  ( dom card = _V -> ( c e. dom card <-> c e. _V ) )
4 2 3 mpbiri 
 |-  ( dom card = _V -> c e. dom card )
5 infxpidm2 
 |-  ( ( c e. dom card /\ _om ~<_ c ) -> ( c X. c ) ~~ c )
6 5 ex 
 |-  ( c e. dom card -> ( _om ~<_ c -> ( c X. c ) ~~ c ) )
7 4 6 syl 
 |-  ( dom card = _V -> ( _om ~<_ c -> ( c X. c ) ~~ c ) )
8 7 alrimiv 
 |-  ( dom card = _V -> A. c ( _om ~<_ c -> ( c X. c ) ~~ c ) )
9 finnum 
 |-  ( a e. Fin -> a e. dom card )
10 9 adantl 
 |-  ( ( A. c ( _om ~<_ c -> ( c X. c ) ~~ c ) /\ a e. Fin ) -> a e. dom card )
11 harcl 
 |-  ( har ` a ) e. On
12 onenon 
 |-  ( ( har ` a ) e. On -> ( har ` a ) e. dom card )
13 11 12 ax-mp 
 |-  ( har ` a ) e. dom card
14 fvex 
 |-  ( har ` a ) e. _V
15 vex 
 |-  a e. _V
16 14 15 unex 
 |-  ( ( har ` a ) u. a ) e. _V
17 harinf 
 |-  ( ( a e. _V /\ -. a e. Fin ) -> _om C_ ( har ` a ) )
18 15 17 mpan 
 |-  ( -. a e. Fin -> _om C_ ( har ` a ) )
19 ssun1 
 |-  ( har ` a ) C_ ( ( har ` a ) u. a )
20 18 19 sstrdi 
 |-  ( -. a e. Fin -> _om C_ ( ( har ` a ) u. a ) )
21 ssdomg 
 |-  ( ( ( har ` a ) u. a ) e. _V -> ( _om C_ ( ( har ` a ) u. a ) -> _om ~<_ ( ( har ` a ) u. a ) ) )
22 16 20 21 mpsyl 
 |-  ( -. a e. Fin -> _om ~<_ ( ( har ` a ) u. a ) )
23 breq2 
 |-  ( c = ( ( har ` a ) u. a ) -> ( _om ~<_ c <-> _om ~<_ ( ( har ` a ) u. a ) ) )
24 xpeq12 
 |-  ( ( c = ( ( har ` a ) u. a ) /\ c = ( ( har ` a ) u. a ) ) -> ( c X. c ) = ( ( ( har ` a ) u. a ) X. ( ( har ` a ) u. a ) ) )
25 24 anidms 
 |-  ( c = ( ( har ` a ) u. a ) -> ( c X. c ) = ( ( ( har ` a ) u. a ) X. ( ( har ` a ) u. a ) ) )
26 id 
 |-  ( c = ( ( har ` a ) u. a ) -> c = ( ( har ` a ) u. a ) )
27 25 26 breq12d 
 |-  ( c = ( ( har ` a ) u. a ) -> ( ( c X. c ) ~~ c <-> ( ( ( har ` a ) u. a ) X. ( ( har ` a ) u. a ) ) ~~ ( ( har ` a ) u. a ) ) )
28 23 27 imbi12d 
 |-  ( c = ( ( har ` a ) u. a ) -> ( ( _om ~<_ c -> ( c X. c ) ~~ c ) <-> ( _om ~<_ ( ( har ` a ) u. a ) -> ( ( ( har ` a ) u. a ) X. ( ( har ` a ) u. a ) ) ~~ ( ( har ` a ) u. a ) ) ) )
29 16 28 spcv 
 |-  ( A. c ( _om ~<_ c -> ( c X. c ) ~~ c ) -> ( _om ~<_ ( ( har ` a ) u. a ) -> ( ( ( har ` a ) u. a ) X. ( ( har ` a ) u. a ) ) ~~ ( ( har ` a ) u. a ) ) )
30 22 29 syl5 
 |-  ( A. c ( _om ~<_ c -> ( c X. c ) ~~ c ) -> ( -. a e. Fin -> ( ( ( har ` a ) u. a ) X. ( ( har ` a ) u. a ) ) ~~ ( ( har ` a ) u. a ) ) )
31 30 imp 
 |-  ( ( A. c ( _om ~<_ c -> ( c X. c ) ~~ c ) /\ -. a e. Fin ) -> ( ( ( har ` a ) u. a ) X. ( ( har ` a ) u. a ) ) ~~ ( ( har ` a ) u. a ) )
32 harndom 
 |-  -. ( har ` a ) ~<_ a
33 ssdomg 
 |-  ( ( ( har ` a ) u. a ) e. _V -> ( ( har ` a ) C_ ( ( har ` a ) u. a ) -> ( har ` a ) ~<_ ( ( har ` a ) u. a ) ) )
34 16 19 33 mp2 
 |-  ( har ` a ) ~<_ ( ( har ` a ) u. a )
35 domtr 
 |-  ( ( ( har ` a ) ~<_ ( ( har ` a ) u. a ) /\ ( ( har ` a ) u. a ) ~<_ a ) -> ( har ` a ) ~<_ a )
36 34 35 mpan 
 |-  ( ( ( har ` a ) u. a ) ~<_ a -> ( har ` a ) ~<_ a )
37 32 36 mto 
 |-  -. ( ( har ` a ) u. a ) ~<_ a
38 unxpwdom2 
 |-  ( ( ( ( har ` a ) u. a ) X. ( ( har ` a ) u. a ) ) ~~ ( ( har ` a ) u. a ) -> ( ( ( har ` a ) u. a ) ~<_* ( har ` a ) \/ ( ( har ` a ) u. a ) ~<_ a ) )
39 orel2 
 |-  ( -. ( ( har ` a ) u. a ) ~<_ a -> ( ( ( ( har ` a ) u. a ) ~<_* ( har ` a ) \/ ( ( har ` a ) u. a ) ~<_ a ) -> ( ( har ` a ) u. a ) ~<_* ( har ` a ) ) )
40 37 38 39 mpsyl 
 |-  ( ( ( ( har ` a ) u. a ) X. ( ( har ` a ) u. a ) ) ~~ ( ( har ` a ) u. a ) -> ( ( har ` a ) u. a ) ~<_* ( har ` a ) )
41 31 40 syl 
 |-  ( ( A. c ( _om ~<_ c -> ( c X. c ) ~~ c ) /\ -. a e. Fin ) -> ( ( har ` a ) u. a ) ~<_* ( har ` a ) )
42 wdomnumr 
 |-  ( ( har ` a ) e. dom card -> ( ( ( har ` a ) u. a ) ~<_* ( har ` a ) <-> ( ( har ` a ) u. a ) ~<_ ( har ` a ) ) )
43 13 42 ax-mp 
 |-  ( ( ( har ` a ) u. a ) ~<_* ( har ` a ) <-> ( ( har ` a ) u. a ) ~<_ ( har ` a ) )
44 41 43 sylib 
 |-  ( ( A. c ( _om ~<_ c -> ( c X. c ) ~~ c ) /\ -. a e. Fin ) -> ( ( har ` a ) u. a ) ~<_ ( har ` a ) )
45 numdom 
 |-  ( ( ( har ` a ) e. dom card /\ ( ( har ` a ) u. a ) ~<_ ( har ` a ) ) -> ( ( har ` a ) u. a ) e. dom card )
46 13 44 45 sylancr 
 |-  ( ( A. c ( _om ~<_ c -> ( c X. c ) ~~ c ) /\ -. a e. Fin ) -> ( ( har ` a ) u. a ) e. dom card )
47 ssun2 
 |-  a C_ ( ( har ` a ) u. a )
48 ssnum 
 |-  ( ( ( ( har ` a ) u. a ) e. dom card /\ a C_ ( ( har ` a ) u. a ) ) -> a e. dom card )
49 46 47 48 sylancl 
 |-  ( ( A. c ( _om ~<_ c -> ( c X. c ) ~~ c ) /\ -. a e. Fin ) -> a e. dom card )
50 10 49 pm2.61dan 
 |-  ( A. c ( _om ~<_ c -> ( c X. c ) ~~ c ) -> a e. dom card )
51 50 alrimiv 
 |-  ( A. c ( _om ~<_ c -> ( c X. c ) ~~ c ) -> A. a a e. dom card )
52 eqv 
 |-  ( dom card = _V <-> A. a a e. dom card )
53 51 52 sylibr 
 |-  ( A. c ( _om ~<_ c -> ( c X. c ) ~~ c ) -> dom card = _V )
54 8 53 impbii 
 |-  ( dom card = _V <-> A. c ( _om ~<_ c -> ( c X. c ) ~~ c ) )
55 1 54 bitri 
 |-  ( CHOICE <-> A. c ( _om ~<_ c -> ( c X. c ) ~~ c ) )