Metamath Proof Explorer

Theorem axccdom

Description: Relax the constraint on ax-cc to dominance instead of equinumerosity. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses axccdom.1 
|- ( ph -> X ~<_ _om )
axccdom.2 
|- ( ( ph /\ z e. X ) -> z =/= (/) )
Assertion axccdom 
|- ( ph -> E. f ( f Fn X /\ A. z e. X ( f ` z ) e. z ) )

Proof

Step Hyp Ref Expression
1 axccdom.1 
 |-  ( ph -> X ~<_ _om )
2 axccdom.2 
 |-  ( ( ph /\ z e. X ) -> z =/= (/) )
3 simpr 
 |-  ( ( ph /\ X e. Fin ) -> X e. Fin )
4 simpr 
 |-  ( ( ( ph /\ X e. Fin ) /\ z e. X ) -> z e. X )
5 2 adantlr 
 |-  ( ( ( ph /\ X e. Fin ) /\ z e. X ) -> z =/= (/) )
6 3 4 5 choicefi 
 |-  ( ( ph /\ X e. Fin ) -> E. f ( f Fn X /\ A. z e. X ( f ` z ) e. z ) )
7 1 adantr 
 |-  ( ( ph /\ -. X e. Fin ) -> X ~<_ _om )
8 isfinite2 
 |-  ( X ~< _om -> X e. Fin )
9 8 con3i 
 |-  ( -. X e. Fin -> -. X ~< _om )
10 9 adantl 
 |-  ( ( ph /\ -. X e. Fin ) -> -. X ~< _om )
11 7 10 jca 
 |-  ( ( ph /\ -. X e. Fin ) -> ( X ~<_ _om /\ -. X ~< _om ) )
12 bren2 
 |-  ( X ~~ _om <-> ( X ~<_ _om /\ -. X ~< _om ) )
13 11 12 sylibr 
 |-  ( ( ph /\ -. X e. Fin ) -> X ~~ _om )
14 ctex 
 |-  ( X ~<_ _om -> X e. _V )
15 1 14 syl 
 |-  ( ph -> X e. _V )
16 15 adantr 
 |-  ( ( ph /\ X ~~ _om ) -> X e. _V )
17 simpr 
 |-  ( ( ph /\ X ~~ _om ) -> X ~~ _om )
18 breq1 
 |-  ( x = X -> ( x ~~ _om <-> X ~~ _om ) )
19 raleq 
 |-  ( x = X -> ( A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) <-> A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) ) )
20 19 exbidv 
 |-  ( x = X -> ( E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) <-> E. g A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) ) )
21 18 20 imbi12d 
 |-  ( x = X -> ( ( x ~~ _om -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) ) <-> ( X ~~ _om -> E. g A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) ) ) )
22 ax-cc 
 |-  ( x ~~ _om -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
23 21 22 vtoclg 
 |-  ( X e. _V -> ( X ~~ _om -> E. g A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) ) )
24 16 17 23 sylc 
 |-  ( ( ph /\ X ~~ _om ) -> E. g A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) )
25 15 mptexd 
 |-  ( ph -> ( z e. X |-> ( g ` z ) ) e. _V )
26 25 adantr 
 |-  ( ( ph /\ A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) ) -> ( z e. X |-> ( g ` z ) ) e. _V )
27 fvex 
 |-  ( g ` z ) e. _V
28 27 rgenw 
 |-  A. z e. X ( g ` z ) e. _V
29 eqid 
 |-  ( z e. X |-> ( g ` z ) ) = ( z e. X |-> ( g ` z ) )
30 29 fnmpt 
 |-  ( A. z e. X ( g ` z ) e. _V -> ( z e. X |-> ( g ` z ) ) Fn X )
31 28 30 ax-mp 
 |-  ( z e. X |-> ( g ` z ) ) Fn X
32 31 a1i 
 |-  ( ( ph /\ A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) ) -> ( z e. X |-> ( g ` z ) ) Fn X )
33 nfv 
 |-  F/ z ph
34 nfra1 
 |-  F/ z A. z e. X ( z =/= (/) -> ( g ` z ) e. z )
35 33 34 nfan 
 |-  F/ z ( ph /\ A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) )
36 id 
 |-  ( z e. X -> z e. X )
37 27 a1i 
 |-  ( z e. X -> ( g ` z ) e. _V )
38 29 fvmpt2 
 |-  ( ( z e. X /\ ( g ` z ) e. _V ) -> ( ( z e. X |-> ( g ` z ) ) ` z ) = ( g ` z ) )
39 36 37 38 syl2anc 
 |-  ( z e. X -> ( ( z e. X |-> ( g ` z ) ) ` z ) = ( g ` z ) )
40 39 adantl 
 |-  ( ( ( ph /\ A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) ) /\ z e. X ) -> ( ( z e. X |-> ( g ` z ) ) ` z ) = ( g ` z ) )
41 rspa 
 |-  ( ( A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) /\ z e. X ) -> ( z =/= (/) -> ( g ` z ) e. z ) )
42 41 adantll 
 |-  ( ( ( ph /\ A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) ) /\ z e. X ) -> ( z =/= (/) -> ( g ` z ) e. z ) )
43 2 adantlr 
 |-  ( ( ( ph /\ A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) ) /\ z e. X ) -> z =/= (/) )
44 id 
 |-  ( ( z =/= (/) -> ( g ` z ) e. z ) -> ( z =/= (/) -> ( g ` z ) e. z ) )
45 42 43 44 sylc 
 |-  ( ( ( ph /\ A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) ) /\ z e. X ) -> ( g ` z ) e. z )
46 40 45 eqeltrd 
 |-  ( ( ( ph /\ A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) ) /\ z e. X ) -> ( ( z e. X |-> ( g ` z ) ) ` z ) e. z )
47 46 ex 
 |-  ( ( ph /\ A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) ) -> ( z e. X -> ( ( z e. X |-> ( g ` z ) ) ` z ) e. z ) )
48 35 47 ralrimi 
 |-  ( ( ph /\ A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) ) -> A. z e. X ( ( z e. X |-> ( g ` z ) ) ` z ) e. z )
49 32 48 jca 
 |-  ( ( ph /\ A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) ) -> ( ( z e. X |-> ( g ` z ) ) Fn X /\ A. z e. X ( ( z e. X |-> ( g ` z ) ) ` z ) e. z ) )
50 fneq1 
 |-  ( f = ( z e. X |-> ( g ` z ) ) -> ( f Fn X <-> ( z e. X |-> ( g ` z ) ) Fn X ) )
51 nfcv 
 |-  F/_ z f
52 nfmpt1 
 |-  F/_ z ( z e. X |-> ( g ` z ) )
53 51 52 nfeq 
 |-  F/ z f = ( z e. X |-> ( g ` z ) )
54 fveq1 
 |-  ( f = ( z e. X |-> ( g ` z ) ) -> ( f ` z ) = ( ( z e. X |-> ( g ` z ) ) ` z ) )
55 54 eleq1d 
 |-  ( f = ( z e. X |-> ( g ` z ) ) -> ( ( f ` z ) e. z <-> ( ( z e. X |-> ( g ` z ) ) ` z ) e. z ) )
56 53 55 ralbid 
 |-  ( f = ( z e. X |-> ( g ` z ) ) -> ( A. z e. X ( f ` z ) e. z <-> A. z e. X ( ( z e. X |-> ( g ` z ) ) ` z ) e. z ) )
57 50 56 anbi12d 
 |-  ( f = ( z e. X |-> ( g ` z ) ) -> ( ( f Fn X /\ A. z e. X ( f ` z ) e. z ) <-> ( ( z e. X |-> ( g ` z ) ) Fn X /\ A. z e. X ( ( z e. X |-> ( g ` z ) ) ` z ) e. z ) ) )
58 57 spcegv 
 |-  ( ( z e. X |-> ( g ` z ) ) e. _V -> ( ( ( z e. X |-> ( g ` z ) ) Fn X /\ A. z e. X ( ( z e. X |-> ( g ` z ) ) ` z ) e. z ) -> E. f ( f Fn X /\ A. z e. X ( f ` z ) e. z ) ) )
59 26 49 58 sylc 
 |-  ( ( ph /\ A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) ) -> E. f ( f Fn X /\ A. z e. X ( f ` z ) e. z ) )
60 59 adantlr 
 |-  ( ( ( ph /\ X ~~ _om ) /\ A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) ) -> E. f ( f Fn X /\ A. z e. X ( f ` z ) e. z ) )
61 60 ex 
 |-  ( ( ph /\ X ~~ _om ) -> ( A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) -> E. f ( f Fn X /\ A. z e. X ( f ` z ) e. z ) ) )
62 61 exlimdv 
 |-  ( ( ph /\ X ~~ _om ) -> ( E. g A. z e. X ( z =/= (/) -> ( g ` z ) e. z ) -> E. f ( f Fn X /\ A. z e. X ( f ` z ) e. z ) ) )
63 24 62 mpd 
 |-  ( ( ph /\ X ~~ _om ) -> E. f ( f Fn X /\ A. z e. X ( f ` z ) e. z ) )
64 13 63 syldan 
 |-  ( ( ph /\ -. X e. Fin ) -> E. f ( f Fn X /\ A. z e. X ( f ` z ) e. z ) )
65 6 64 pm2.61dan 
 |-  ( ph -> E. f ( f Fn X /\ A. z e. X ( f ` z ) e. z ) )