Metamath Proof Explorer

Theorem fineqvac

Description: If the Axiom of Infinity is negated, then the Axiom of Choice becomes redundant. For a shorter proof using ax-rep and ax-pow , see fineqvacALT . (Contributed by BTernaryTau, 21-Sep-2024)

Ref Expression
Assertion fineqvac 
|- ( Fin = _V -> CHOICE )

Proof

Step Hyp Ref Expression
1 vex 
 |-  w e. _V
2 eleq2w2 
 |-  ( Fin = _V -> ( w e. Fin <-> w e. _V ) )
3 1 2 mpbiri 
 |-  ( Fin = _V -> w e. Fin )
4 sseq2 
 |-  ( x = (/) -> ( f C_ x <-> f C_ (/) ) )
5 dmeq 
 |-  ( x = (/) -> dom x = dom (/) )
6 5 fneq2d 
 |-  ( x = (/) -> ( f Fn dom x <-> f Fn dom (/) ) )
7 4 6 anbi12d 
 |-  ( x = (/) -> ( ( f C_ x /\ f Fn dom x ) <-> ( f C_ (/) /\ f Fn dom (/) ) ) )
8 7 exbidv 
 |-  ( x = (/) -> ( E. f ( f C_ x /\ f Fn dom x ) <-> E. f ( f C_ (/) /\ f Fn dom (/) ) ) )
9 sseq2 
 |-  ( x = y -> ( f C_ x <-> f C_ y ) )
10 dmeq 
 |-  ( x = y -> dom x = dom y )
11 10 fneq2d 
 |-  ( x = y -> ( f Fn dom x <-> f Fn dom y ) )
12 9 11 anbi12d 
 |-  ( x = y -> ( ( f C_ x /\ f Fn dom x ) <-> ( f C_ y /\ f Fn dom y ) ) )
13 12 exbidv 
 |-  ( x = y -> ( E. f ( f C_ x /\ f Fn dom x ) <-> E. f ( f C_ y /\ f Fn dom y ) ) )
14 sseq2 
 |-  ( x = ( y u. { z } ) -> ( f C_ x <-> f C_ ( y u. { z } ) ) )
15 dmeq 
 |-  ( x = ( y u. { z } ) -> dom x = dom ( y u. { z } ) )
16 15 fneq2d 
 |-  ( x = ( y u. { z } ) -> ( f Fn dom x <-> f Fn dom ( y u. { z } ) ) )
17 14 16 anbi12d 
 |-  ( x = ( y u. { z } ) -> ( ( f C_ x /\ f Fn dom x ) <-> ( f C_ ( y u. { z } ) /\ f Fn dom ( y u. { z } ) ) ) )
18 17 exbidv 
 |-  ( x = ( y u. { z } ) -> ( E. f ( f C_ x /\ f Fn dom x ) <-> E. f ( f C_ ( y u. { z } ) /\ f Fn dom ( y u. { z } ) ) ) )
19 sseq2 
 |-  ( x = w -> ( f C_ x <-> f C_ w ) )
20 dmeq 
 |-  ( x = w -> dom x = dom w )
21 20 fneq2d 
 |-  ( x = w -> ( f Fn dom x <-> f Fn dom w ) )
22 19 21 anbi12d 
 |-  ( x = w -> ( ( f C_ x /\ f Fn dom x ) <-> ( f C_ w /\ f Fn dom w ) ) )
23 22 exbidv 
 |-  ( x = w -> ( E. f ( f C_ x /\ f Fn dom x ) <-> E. f ( f C_ w /\ f Fn dom w ) ) )
24 ssid 
 |-  (/) C_ (/)
25 fun0 
 |-  Fun (/)
26 funfn 
 |-  ( Fun (/) <-> (/) Fn dom (/) )
27 25 26 mpbi 
 |-  (/) Fn dom (/)
28 0ex 
 |-  (/) e. _V
29 sseq1 
 |-  ( f = (/) -> ( f C_ (/) <-> (/) C_ (/) ) )
30 fneq1 
 |-  ( f = (/) -> ( f Fn dom (/) <-> (/) Fn dom (/) ) )
31 29 30 anbi12d 
 |-  ( f = (/) -> ( ( f C_ (/) /\ f Fn dom (/) ) <-> ( (/) C_ (/) /\ (/) Fn dom (/) ) ) )
32 28 31 spcev 
 |-  ( ( (/) C_ (/) /\ (/) Fn dom (/) ) -> E. f ( f C_ (/) /\ f Fn dom (/) ) )
33 24 27 32 mp2an 
 |-  E. f ( f C_ (/) /\ f Fn dom (/) )
34 sseq1 
 |-  ( f = g -> ( f C_ y <-> g C_ y ) )
35 fneq1 
 |-  ( f = g -> ( f Fn dom y <-> g Fn dom y ) )
36 34 35 anbi12d 
 |-  ( f = g -> ( ( f C_ y /\ f Fn dom y ) <-> ( g C_ y /\ g Fn dom y ) ) )
37 36 cbvexvw 
 |-  ( E. f ( f C_ y /\ f Fn dom y ) <-> E. g ( g C_ y /\ g Fn dom y ) )
38 ssun3 
 |-  ( g C_ y -> g C_ ( y u. { z } ) )
39 38 ad2antrr 
 |-  ( ( ( g C_ y /\ g Fn dom y ) /\ dom { z } = (/) ) -> g C_ ( y u. { z } ) )
40 dmun 
 |-  dom ( y u. { z } ) = ( dom y u. dom { z } )
41 uneq2 
 |-  ( dom { z } = (/) -> ( dom y u. dom { z } ) = ( dom y u. (/) ) )
42 un0 
 |-  ( dom y u. (/) ) = dom y
43 41 42 eqtrdi 
 |-  ( dom { z } = (/) -> ( dom y u. dom { z } ) = dom y )
44 40 43 syl5eq 
 |-  ( dom { z } = (/) -> dom ( y u. { z } ) = dom y )
45 44 fneq2d 
 |-  ( dom { z } = (/) -> ( g Fn dom ( y u. { z } ) <-> g Fn dom y ) )
46 45 biimparc 
 |-  ( ( g Fn dom y /\ dom { z } = (/) ) -> g Fn dom ( y u. { z } ) )
47 46 adantll 
 |-  ( ( ( g C_ y /\ g Fn dom y ) /\ dom { z } = (/) ) -> g Fn dom ( y u. { z } ) )
48 vex 
 |-  g e. _V
49 sseq1 
 |-  ( f = g -> ( f C_ ( y u. { z } ) <-> g C_ ( y u. { z } ) ) )
50 fneq1 
 |-  ( f = g -> ( f Fn dom ( y u. { z } ) <-> g Fn dom ( y u. { z } ) ) )
51 49 50 anbi12d 
 |-  ( f = g -> ( ( f C_ ( y u. { z } ) /\ f Fn dom ( y u. { z } ) ) <-> ( g C_ ( y u. { z } ) /\ g Fn dom ( y u. { z } ) ) ) )
52 48 51 spcev 
 |-  ( ( g C_ ( y u. { z } ) /\ g Fn dom ( y u. { z } ) ) -> E. f ( f C_ ( y u. { z } ) /\ f Fn dom ( y u. { z } ) ) )
53 39 47 52 syl2anc 
 |-  ( ( ( g C_ y /\ g Fn dom y ) /\ dom { z } = (/) ) -> E. f ( f C_ ( y u. { z } ) /\ f Fn dom ( y u. { z } ) ) )
54 dmsnn0 
 |-  ( z e. ( _V X. _V ) <-> dom { z } =/= (/) )
55 elvv 
 |-  ( z e. ( _V X. _V ) <-> E. u E. v z = <. u , v >. )
56 54 55 bitr3i 
 |-  ( dom { z } =/= (/) <-> E. u E. v z = <. u , v >. )
57 56 anbi2i 
 |-  ( ( ( g C_ y /\ g Fn dom y ) /\ dom { z } =/= (/) ) <-> ( ( g C_ y /\ g Fn dom y ) /\ E. u E. v z = <. u , v >. ) )
58 19.42vv 
 |-  ( E. u E. v ( ( g C_ y /\ g Fn dom y ) /\ z = <. u , v >. ) <-> ( ( g C_ y /\ g Fn dom y ) /\ E. u E. v z = <. u , v >. ) )
59 57 58 bitr4i 
 |-  ( ( ( g C_ y /\ g Fn dom y ) /\ dom { z } =/= (/) ) <-> E. u E. v ( ( g C_ y /\ g Fn dom y ) /\ z = <. u , v >. ) )
60 38 3ad2ant1 
 |-  ( ( g C_ y /\ g Fn dom y /\ z = <. u , v >. ) -> g C_ ( y u. { z } ) )
61 snssi 
 |-  ( u e. dom y -> { u } C_ dom y )
62 ssequn2 
 |-  ( { u } C_ dom y <-> ( dom y u. { u } ) = dom y )
63 61 62 sylib 
 |-  ( u e. dom y -> ( dom y u. { u } ) = dom y )
64 63 fneq2d 
 |-  ( u e. dom y -> ( g Fn ( dom y u. { u } ) <-> g Fn dom y ) )
65 64 biimparc 
 |-  ( ( g Fn dom y /\ u e. dom y ) -> g Fn ( dom y u. { u } ) )
66 65 3adant2 
 |-  ( ( g Fn dom y /\ z = <. u , v >. /\ u e. dom y ) -> g Fn ( dom y u. { u } ) )
67 sneq 
 |-  ( z = <. u , v >. -> { z } = { <. u , v >. } )
68 67 dmeqd 
 |-  ( z = <. u , v >. -> dom { z } = dom { <. u , v >. } )
69 vex 
 |-  v e. _V
70 69 dmsnop 
 |-  dom { <. u , v >. } = { u }
71 68 70 eqtrdi 
 |-  ( z = <. u , v >. -> dom { z } = { u } )
72 71 uneq2d 
 |-  ( z = <. u , v >. -> ( dom y u. dom { z } ) = ( dom y u. { u } ) )
73 40 72 syl5eq 
 |-  ( z = <. u , v >. -> dom ( y u. { z } ) = ( dom y u. { u } ) )
74 73 fneq2d 
 |-  ( z = <. u , v >. -> ( g Fn dom ( y u. { z } ) <-> g Fn ( dom y u. { u } ) ) )
75 74 3ad2ant2 
 |-  ( ( g Fn dom y /\ z = <. u , v >. /\ u e. dom y ) -> ( g Fn dom ( y u. { z } ) <-> g Fn ( dom y u. { u } ) ) )
76 66 75 mpbird 
 |-  ( ( g Fn dom y /\ z = <. u , v >. /\ u e. dom y ) -> g Fn dom ( y u. { z } ) )
77 76 3expia 
 |-  ( ( g Fn dom y /\ z = <. u , v >. ) -> ( u e. dom y -> g Fn dom ( y u. { z } ) ) )
78 77 3adant1 
 |-  ( ( g C_ y /\ g Fn dom y /\ z = <. u , v >. ) -> ( u e. dom y -> g Fn dom ( y u. { z } ) ) )
79 60 78 52 syl6an 
 |-  ( ( g C_ y /\ g Fn dom y /\ z = <. u , v >. ) -> ( u e. dom y -> E. f ( f C_ ( y u. { z } ) /\ f Fn dom ( y u. { z } ) ) ) )
80 67 uneq2d 
 |-  ( z = <. u , v >. -> ( g u. { z } ) = ( g u. { <. u , v >. } ) )
81 80 adantl 
 |-  ( ( g C_ y /\ z = <. u , v >. ) -> ( g u. { z } ) = ( g u. { <. u , v >. } ) )
82 unss1 
 |-  ( g C_ y -> ( g u. { z } ) C_ ( y u. { z } ) )
83 82 adantr 
 |-  ( ( g C_ y /\ z = <. u , v >. ) -> ( g u. { z } ) C_ ( y u. { z } ) )
84 81 83 eqsstrrd 
 |-  ( ( g C_ y /\ z = <. u , v >. ) -> ( g u. { <. u , v >. } ) C_ ( y u. { z } ) )
85 84 3adant2 
 |-  ( ( g C_ y /\ g Fn dom y /\ z = <. u , v >. ) -> ( g u. { <. u , v >. } ) C_ ( y u. { z } ) )
86 vex 
 |-  u e. _V
87 86 a1i 
 |-  ( ( g Fn dom y /\ -. u e. dom y ) -> u e. _V )
88 69 a1i 
 |-  ( ( g Fn dom y /\ -. u e. dom y ) -> v e. _V )
89 simpl 
 |-  ( ( g Fn dom y /\ -. u e. dom y ) -> g Fn dom y )
90 eqid 
 |-  ( g u. { <. u , v >. } ) = ( g u. { <. u , v >. } )
91 eqid 
 |-  ( dom y u. { u } ) = ( dom y u. { u } )
92 simpr 
 |-  ( ( g Fn dom y /\ -. u e. dom y ) -> -. u e. dom y )
93 87 88 89 90 91 92 fnunop 
 |-  ( ( g Fn dom y /\ -. u e. dom y ) -> ( g u. { <. u , v >. } ) Fn ( dom y u. { u } ) )
94 93 ex 
 |-  ( g Fn dom y -> ( -. u e. dom y -> ( g u. { <. u , v >. } ) Fn ( dom y u. { u } ) ) )
95 94 3ad2ant2 
 |-  ( ( g C_ y /\ g Fn dom y /\ z = <. u , v >. ) -> ( -. u e. dom y -> ( g u. { <. u , v >. } ) Fn ( dom y u. { u } ) ) )
96 73 fneq2d 
 |-  ( z = <. u , v >. -> ( ( g u. { <. u , v >. } ) Fn dom ( y u. { z } ) <-> ( g u. { <. u , v >. } ) Fn ( dom y u. { u } ) ) )
97 96 3ad2ant3 
 |-  ( ( g C_ y /\ g Fn dom y /\ z = <. u , v >. ) -> ( ( g u. { <. u , v >. } ) Fn dom ( y u. { z } ) <-> ( g u. { <. u , v >. } ) Fn ( dom y u. { u } ) ) )
98 95 97 sylibrd 
 |-  ( ( g C_ y /\ g Fn dom y /\ z = <. u , v >. ) -> ( -. u e. dom y -> ( g u. { <. u , v >. } ) Fn dom ( y u. { z } ) ) )
99 snex 
 |-  { <. u , v >. } e. _V
100 48 99 unex 
 |-  ( g u. { <. u , v >. } ) e. _V
101 sseq1 
 |-  ( f = ( g u. { <. u , v >. } ) -> ( f C_ ( y u. { z } ) <-> ( g u. { <. u , v >. } ) C_ ( y u. { z } ) ) )
102 fneq1 
 |-  ( f = ( g u. { <. u , v >. } ) -> ( f Fn dom ( y u. { z } ) <-> ( g u. { <. u , v >. } ) Fn dom ( y u. { z } ) ) )
103 101 102 anbi12d 
 |-  ( f = ( g u. { <. u , v >. } ) -> ( ( f C_ ( y u. { z } ) /\ f Fn dom ( y u. { z } ) ) <-> ( ( g u. { <. u , v >. } ) C_ ( y u. { z } ) /\ ( g u. { <. u , v >. } ) Fn dom ( y u. { z } ) ) ) )
104 100 103 spcev 
 |-  ( ( ( g u. { <. u , v >. } ) C_ ( y u. { z } ) /\ ( g u. { <. u , v >. } ) Fn dom ( y u. { z } ) ) -> E. f ( f C_ ( y u. { z } ) /\ f Fn dom ( y u. { z } ) ) )
105 85 98 104 syl6an 
 |-  ( ( g C_ y /\ g Fn dom y /\ z = <. u , v >. ) -> ( -. u e. dom y -> E. f ( f C_ ( y u. { z } ) /\ f Fn dom ( y u. { z } ) ) ) )
106 79 105 pm2.61d 
 |-  ( ( g C_ y /\ g Fn dom y /\ z = <. u , v >. ) -> E. f ( f C_ ( y u. { z } ) /\ f Fn dom ( y u. { z } ) ) )
107 106 3expa 
 |-  ( ( ( g C_ y /\ g Fn dom y ) /\ z = <. u , v >. ) -> E. f ( f C_ ( y u. { z } ) /\ f Fn dom ( y u. { z } ) ) )
108 107 exlimivv 
 |-  ( E. u E. v ( ( g C_ y /\ g Fn dom y ) /\ z = <. u , v >. ) -> E. f ( f C_ ( y u. { z } ) /\ f Fn dom ( y u. { z } ) ) )
109 59 108 sylbi 
 |-  ( ( ( g C_ y /\ g Fn dom y ) /\ dom { z } =/= (/) ) -> E. f ( f C_ ( y u. { z } ) /\ f Fn dom ( y u. { z } ) ) )
110 53 109 pm2.61dane 
 |-  ( ( g C_ y /\ g Fn dom y ) -> E. f ( f C_ ( y u. { z } ) /\ f Fn dom ( y u. { z } ) ) )
111 110 exlimiv 
 |-  ( E. g ( g C_ y /\ g Fn dom y ) -> E. f ( f C_ ( y u. { z } ) /\ f Fn dom ( y u. { z } ) ) )
112 37 111 sylbi 
 |-  ( E. f ( f C_ y /\ f Fn dom y ) -> E. f ( f C_ ( y u. { z } ) /\ f Fn dom ( y u. { z } ) ) )
113 112 a1i 
 |-  ( y e. Fin -> ( E. f ( f C_ y /\ f Fn dom y ) -> E. f ( f C_ ( y u. { z } ) /\ f Fn dom ( y u. { z } ) ) ) )
114 8 13 18 23 33 113 findcard2 
 |-  ( w e. Fin -> E. f ( f C_ w /\ f Fn dom w ) )
115 3 114 syl 
 |-  ( Fin = _V -> E. f ( f C_ w /\ f Fn dom w ) )
116 115 alrimiv 
 |-  ( Fin = _V -> A. w E. f ( f C_ w /\ f Fn dom w ) )
117 df-ac 
 |-  ( CHOICE <-> A. w E. f ( f C_ w /\ f Fn dom w ) )
118 116 117 sylibr 
 |-  ( Fin = _V -> CHOICE )