# 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 ${⊢}{\phi }\to {X}\preccurlyeq \mathrm{\omega }$
axccdom.2 ${⊢}\left({\phi }\wedge {z}\in {X}\right)\to {z}\ne \varnothing$
Assertion axccdom ${⊢}{\phi }\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({z}\right)\in {z}\right)$

### Proof

Step Hyp Ref Expression
1 axccdom.1 ${⊢}{\phi }\to {X}\preccurlyeq \mathrm{\omega }$
2 axccdom.2 ${⊢}\left({\phi }\wedge {z}\in {X}\right)\to {z}\ne \varnothing$
3 simpr ${⊢}\left({\phi }\wedge {X}\in \mathrm{Fin}\right)\to {X}\in \mathrm{Fin}$
4 simpr ${⊢}\left(\left({\phi }\wedge {X}\in \mathrm{Fin}\right)\wedge {z}\in {X}\right)\to {z}\in {X}$
5 2 adantlr ${⊢}\left(\left({\phi }\wedge {X}\in \mathrm{Fin}\right)\wedge {z}\in {X}\right)\to {z}\ne \varnothing$
6 3 4 5 choicefi ${⊢}\left({\phi }\wedge {X}\in \mathrm{Fin}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({z}\right)\in {z}\right)$
7 1 adantr ${⊢}\left({\phi }\wedge ¬{X}\in \mathrm{Fin}\right)\to {X}\preccurlyeq \mathrm{\omega }$
8 isfinite2 ${⊢}{X}\prec \mathrm{\omega }\to {X}\in \mathrm{Fin}$
9 8 con3i ${⊢}¬{X}\in \mathrm{Fin}\to ¬{X}\prec \mathrm{\omega }$
10 9 adantl ${⊢}\left({\phi }\wedge ¬{X}\in \mathrm{Fin}\right)\to ¬{X}\prec \mathrm{\omega }$
11 7 10 jca ${⊢}\left({\phi }\wedge ¬{X}\in \mathrm{Fin}\right)\to \left({X}\preccurlyeq \mathrm{\omega }\wedge ¬{X}\prec \mathrm{\omega }\right)$
12 bren2 ${⊢}{X}\approx \mathrm{\omega }↔\left({X}\preccurlyeq \mathrm{\omega }\wedge ¬{X}\prec \mathrm{\omega }\right)$
13 11 12 sylibr ${⊢}\left({\phi }\wedge ¬{X}\in \mathrm{Fin}\right)\to {X}\approx \mathrm{\omega }$
14 ctex ${⊢}{X}\preccurlyeq \mathrm{\omega }\to {X}\in \mathrm{V}$
15 1 14 syl ${⊢}{\phi }\to {X}\in \mathrm{V}$
16 15 adantr ${⊢}\left({\phi }\wedge {X}\approx \mathrm{\omega }\right)\to {X}\in \mathrm{V}$
17 simpr ${⊢}\left({\phi }\wedge {X}\approx \mathrm{\omega }\right)\to {X}\approx \mathrm{\omega }$
18 breq1 ${⊢}{x}={X}\to \left({x}\approx \mathrm{\omega }↔{X}\approx \mathrm{\omega }\right)$
19 raleq ${⊢}{x}={X}\to \left(\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)↔\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\right)$
20 19 exbidv ${⊢}{x}={X}\to \left(\exists {g}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)↔\exists {g}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\right)$
21 18 20 imbi12d ${⊢}{x}={X}\to \left(\left({x}\approx \mathrm{\omega }\to \exists {g}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\right)↔\left({X}\approx \mathrm{\omega }\to \exists {g}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\right)\right)$
22 ax-cc ${⊢}{x}\approx \mathrm{\omega }\to \exists {g}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)$
23 21 22 vtoclg ${⊢}{X}\in \mathrm{V}\to \left({X}\approx \mathrm{\omega }\to \exists {g}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\right)$
24 16 17 23 sylc ${⊢}\left({\phi }\wedge {X}\approx \mathrm{\omega }\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)$
25 15 mptexd ${⊢}{\phi }\to \left({z}\in {X}⟼{g}\left({z}\right)\right)\in \mathrm{V}$
26 25 adantr ${⊢}\left({\phi }\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\right)\to \left({z}\in {X}⟼{g}\left({z}\right)\right)\in \mathrm{V}$
27 fvex ${⊢}{g}\left({z}\right)\in \mathrm{V}$
28 27 rgenw ${⊢}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{g}\left({z}\right)\in \mathrm{V}$
29 eqid ${⊢}\left({z}\in {X}⟼{g}\left({z}\right)\right)=\left({z}\in {X}⟼{g}\left({z}\right)\right)$
30 29 fnmpt ${⊢}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{g}\left({z}\right)\in \mathrm{V}\to \left({z}\in {X}⟼{g}\left({z}\right)\right)Fn{X}$
31 28 30 ax-mp ${⊢}\left({z}\in {X}⟼{g}\left({z}\right)\right)Fn{X}$
32 31 a1i ${⊢}\left({\phi }\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\right)\to \left({z}\in {X}⟼{g}\left({z}\right)\right)Fn{X}$
33 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{\phi }$
34 nfra1 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)$
35 33 34 nfan ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\right)$
36 id ${⊢}{z}\in {X}\to {z}\in {X}$
37 27 a1i ${⊢}{z}\in {X}\to {g}\left({z}\right)\in \mathrm{V}$
38 29 fvmpt2 ${⊢}\left({z}\in {X}\wedge {g}\left({z}\right)\in \mathrm{V}\right)\to \left({z}\in {X}⟼{g}\left({z}\right)\right)\left({z}\right)={g}\left({z}\right)$
39 36 37 38 syl2anc ${⊢}{z}\in {X}\to \left({z}\in {X}⟼{g}\left({z}\right)\right)\left({z}\right)={g}\left({z}\right)$
40 39 adantl ${⊢}\left(\left({\phi }\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\right)\wedge {z}\in {X}\right)\to \left({z}\in {X}⟼{g}\left({z}\right)\right)\left({z}\right)={g}\left({z}\right)$
41 rspa ${⊢}\left(\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\wedge {z}\in {X}\right)\to \left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)$
42 41 adantll ${⊢}\left(\left({\phi }\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\right)\wedge {z}\in {X}\right)\to \left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)$
43 2 adantlr ${⊢}\left(\left({\phi }\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\right)\wedge {z}\in {X}\right)\to {z}\ne \varnothing$
44 id ${⊢}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\to \left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)$
45 42 43 44 sylc ${⊢}\left(\left({\phi }\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\right)\wedge {z}\in {X}\right)\to {g}\left({z}\right)\in {z}$
46 40 45 eqeltrd ${⊢}\left(\left({\phi }\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\right)\wedge {z}\in {X}\right)\to \left({z}\in {X}⟼{g}\left({z}\right)\right)\left({z}\right)\in {z}$
47 46 ex ${⊢}\left({\phi }\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\right)\to \left({z}\in {X}\to \left({z}\in {X}⟼{g}\left({z}\right)\right)\left({z}\right)\in {z}\right)$
48 35 47 ralrimi ${⊢}\left({\phi }\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\right)\to \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\in {X}⟼{g}\left({z}\right)\right)\left({z}\right)\in {z}$
49 32 48 jca ${⊢}\left({\phi }\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\right)\to \left(\left({z}\in {X}⟼{g}\left({z}\right)\right)Fn{X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\in {X}⟼{g}\left({z}\right)\right)\left({z}\right)\in {z}\right)$
50 fneq1 ${⊢}{f}=\left({z}\in {X}⟼{g}\left({z}\right)\right)\to \left({f}Fn{X}↔\left({z}\in {X}⟼{g}\left({z}\right)\right)Fn{X}\right)$
51 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{f}$
52 nfmpt1 ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}\left({z}\in {X}⟼{g}\left({z}\right)\right)$
53 51 52 nfeq ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{f}=\left({z}\in {X}⟼{g}\left({z}\right)\right)$
54 fveq1 ${⊢}{f}=\left({z}\in {X}⟼{g}\left({z}\right)\right)\to {f}\left({z}\right)=\left({z}\in {X}⟼{g}\left({z}\right)\right)\left({z}\right)$
55 54 eleq1d ${⊢}{f}=\left({z}\in {X}⟼{g}\left({z}\right)\right)\to \left({f}\left({z}\right)\in {z}↔\left({z}\in {X}⟼{g}\left({z}\right)\right)\left({z}\right)\in {z}\right)$
56 53 55 ralbid ${⊢}{f}=\left({z}\in {X}⟼{g}\left({z}\right)\right)\to \left(\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({z}\right)\in {z}↔\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\in {X}⟼{g}\left({z}\right)\right)\left({z}\right)\in {z}\right)$
57 50 56 anbi12d ${⊢}{f}=\left({z}\in {X}⟼{g}\left({z}\right)\right)\to \left(\left({f}Fn{X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({z}\right)\in {z}\right)↔\left(\left({z}\in {X}⟼{g}\left({z}\right)\right)Fn{X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\in {X}⟼{g}\left({z}\right)\right)\left({z}\right)\in {z}\right)\right)$
58 57 spcegv ${⊢}\left({z}\in {X}⟼{g}\left({z}\right)\right)\in \mathrm{V}\to \left(\left(\left({z}\in {X}⟼{g}\left({z}\right)\right)Fn{X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\in {X}⟼{g}\left({z}\right)\right)\left({z}\right)\in {z}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({z}\right)\in {z}\right)\right)$
59 26 49 58 sylc ${⊢}\left({\phi }\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({z}\right)\in {z}\right)$
60 59 adantlr ${⊢}\left(\left({\phi }\wedge {X}\approx \mathrm{\omega }\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({z}\right)\in {z}\right)$
61 60 ex ${⊢}\left({\phi }\wedge {X}\approx \mathrm{\omega }\right)\to \left(\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({z}\right)\in {z}\right)\right)$
62 61 exlimdv ${⊢}\left({\phi }\wedge {X}\approx \mathrm{\omega }\right)\to \left(\exists {g}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {g}\left({z}\right)\in {z}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({z}\right)\in {z}\right)\right)$
63 24 62 mpd ${⊢}\left({\phi }\wedge {X}\approx \mathrm{\omega }\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({z}\right)\in {z}\right)$
64 13 63 syldan ${⊢}\left({\phi }\wedge ¬{X}\in \mathrm{Fin}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({z}\right)\in {z}\right)$
65 6 64 pm2.61dan ${⊢}{\phi }\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({z}\right)\in {z}\right)$