# Metamath Proof Explorer

## Theorem ac6sfi

Description: A version of ac6s for finite sets. (Contributed by Jeff Hankins, 26-Jun-2009) (Proof shortened by Mario Carneiro, 29-Jan-2014)

Ref Expression
Hypothesis ac6sfi.1 ${⊢}{y}={f}\left({x}\right)\to \left({\phi }↔{\psi }\right)$
Assertion ac6sfi ${⊢}\left({A}\in \mathrm{Fin}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 ac6sfi.1 ${⊢}{y}={f}\left({x}\right)\to \left({\phi }↔{\psi }\right)$
2 raleq ${⊢}{u}=\varnothing \to \left(\forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
3 feq2 ${⊢}{u}=\varnothing \to \left({f}:{u}⟶{B}↔{f}:\varnothing ⟶{B}\right)$
4 raleq ${⊢}{u}=\varnothing \to \left(\forall {x}\in {u}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{\psi }\right)$
5 3 4 anbi12d ${⊢}{u}=\varnothing \to \left(\left({f}:{u}⟶{B}\wedge \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}{\psi }\right)↔\left({f}:\varnothing ⟶{B}\wedge \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$
6 5 exbidv ${⊢}{u}=\varnothing \to \left(\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{u}⟶{B}\wedge \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}{\psi }\right)↔\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:\varnothing ⟶{B}\wedge \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$
7 2 6 imbi12d ${⊢}{u}=\varnothing \to \left(\left(\forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{u}⟶{B}\wedge \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)↔\left(\forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:\varnothing ⟶{B}\wedge \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{\psi }\right)\right)\right)$
8 raleq ${⊢}{u}={w}\to \left(\forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
9 feq2 ${⊢}{u}={w}\to \left({f}:{u}⟶{B}↔{f}:{w}⟶{B}\right)$
10 raleq ${⊢}{u}={w}\to \left(\forall {x}\in {u}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
11 9 10 anbi12d ${⊢}{u}={w}\to \left(\left({f}:{u}⟶{B}\wedge \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}{\psi }\right)↔\left({f}:{w}⟶{B}\wedge \forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$
12 11 exbidv ${⊢}{u}={w}\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{u}⟶{B}\wedge \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}{\psi }\right)↔\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{w}⟶{B}\wedge \forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$
13 8 12 imbi12d ${⊢}{u}={w}\to \left(\left(\forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{u}⟶{B}\wedge \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)↔\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{w}⟶{B}\wedge \forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)\right)$
14 raleq ${⊢}{u}={w}\cup \left\{{z}\right\}\to \left(\forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\in \left({w}\cup \left\{{z}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
15 feq2 ${⊢}{u}={w}\cup \left\{{z}\right\}\to \left({f}:{u}⟶{B}↔{f}:{w}\cup \left\{{z}\right\}⟶{B}\right)$
16 raleq ${⊢}{u}={w}\cup \left\{{z}\right\}\to \left(\forall {x}\in {u}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {x}\in \left({w}\cup \left\{{z}\right\}\right)\phantom{\rule{.4em}{0ex}}{\psi }\right)$
17 15 16 anbi12d ${⊢}{u}={w}\cup \left\{{z}\right\}\to \left(\left({f}:{u}⟶{B}\wedge \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}{\psi }\right)↔\left({f}:{w}\cup \left\{{z}\right\}⟶{B}\wedge \forall {x}\in \left({w}\cup \left\{{z}\right\}\right)\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$
18 17 exbidv ${⊢}{u}={w}\cup \left\{{z}\right\}\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{u}⟶{B}\wedge \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}{\psi }\right)↔\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{w}\cup \left\{{z}\right\}⟶{B}\wedge \forall {x}\in \left({w}\cup \left\{{z}\right\}\right)\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$
19 feq1 ${⊢}{f}={g}\to \left({f}:{w}\cup \left\{{z}\right\}⟶{B}↔{g}:{w}\cup \left\{{z}\right\}⟶{B}\right)$
20 fvex ${⊢}{f}\left({x}\right)\in \mathrm{V}$
21 20 1 sbcie
22 fveq1 ${⊢}{f}={g}\to {f}\left({x}\right)={g}\left({x}\right)$
23 22 sbceq1d
24 21 23 bitr3id
25 24 ralbidv
26 19 25 anbi12d
27 26 cbvexvw
28 18 27 syl6bb
29 14 28 imbi12d
30 raleq ${⊢}{u}={A}\to \left(\forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
31 feq2 ${⊢}{u}={A}\to \left({f}:{u}⟶{B}↔{f}:{A}⟶{B}\right)$
32 raleq ${⊢}{u}={A}\to \left(\forall {x}\in {u}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
33 31 32 anbi12d ${⊢}{u}={A}\to \left(\left({f}:{u}⟶{B}\wedge \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}{\psi }\right)↔\left({f}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$
34 33 exbidv ${⊢}{u}={A}\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{u}⟶{B}\wedge \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}{\psi }\right)↔\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$
35 30 34 imbi12d ${⊢}{u}={A}\to \left(\left(\forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{u}⟶{B}\wedge \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)\right)$
36 f0 ${⊢}\varnothing :\varnothing ⟶{B}$
37 0ex ${⊢}\varnothing \in \mathrm{V}$
38 ral0 ${⊢}\forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{\psi }$
39 38 biantru ${⊢}{f}:\varnothing ⟶{B}↔\left({f}:\varnothing ⟶{B}\wedge \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{\psi }\right)$
40 feq1 ${⊢}{f}=\varnothing \to \left({f}:\varnothing ⟶{B}↔\varnothing :\varnothing ⟶{B}\right)$
41 39 40 bitr3id ${⊢}{f}=\varnothing \to \left(\left({f}:\varnothing ⟶{B}\wedge \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{\psi }\right)↔\varnothing :\varnothing ⟶{B}\right)$
42 37 41 spcev ${⊢}\varnothing :\varnothing ⟶{B}\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:\varnothing ⟶{B}\wedge \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{\psi }\right)$
43 36 42 mp1i ${⊢}\forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:\varnothing ⟶{B}\wedge \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{\psi }\right)$
44 ssun1 ${⊢}{w}\subseteq {w}\cup \left\{{z}\right\}$
45 ssralv ${⊢}{w}\subseteq {w}\cup \left\{{z}\right\}\to \left(\forall {x}\in \left({w}\cup \left\{{z}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\in {w}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
46 44 45 ax-mp ${⊢}\forall {x}\in \left({w}\cup \left\{{z}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\in {w}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }$
47 46 imim1i ${⊢}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{w}⟶{B}\wedge \forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)\to \left(\forall {x}\in \left({w}\cup \left\{{z}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{w}⟶{B}\wedge \forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$
48 ssun2 ${⊢}\left\{{z}\right\}\subseteq {w}\cup \left\{{z}\right\}$
49 ssralv ${⊢}\left\{{z}\right\}\subseteq {w}\cup \left\{{z}\right\}\to \left(\forall {x}\in \left({w}\cup \left\{{z}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\in \left\{{z}\right\}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
50 48 49 ax-mp ${⊢}\forall {x}\in \left({w}\cup \left\{{z}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\in \left\{{z}\right\}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }$
51 ralsnsg
52 51 elv
53 sbcrex
54 52 53 bitri
55 50 54 sylib
56 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}¬{z}\in {w}$
57 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{w}⟶{B}\wedge \forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
58 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{g}:{w}\cup \left\{{z}\right\}⟶{B}$
59 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left({w}\cup \left\{{z}\right\}\right)$
60 nfsbc1v
61 59 60 nfralw
62 58 61 nfan
63 62 nfex
64 57 63 nfim
65 simprl
66 vex ${⊢}{z}\in \mathrm{V}$
67 vex ${⊢}{y}\in \mathrm{V}$
68 66 67 f1osn ${⊢}\left\{⟨{z},{y}⟩\right\}:\left\{{z}\right\}\underset{1-1 onto}{⟶}\left\{{y}\right\}$
69 f1of ${⊢}\left\{⟨{z},{y}⟩\right\}:\left\{{z}\right\}\underset{1-1 onto}{⟶}\left\{{y}\right\}\to \left\{⟨{z},{y}⟩\right\}:\left\{{z}\right\}⟶\left\{{y}\right\}$
70 68 69 mp1i
71 simpl2
72 71 snssd
73 70 72 fssd
74 simpl1
75 disjsn ${⊢}{w}\cap \left\{{z}\right\}=\varnothing ↔¬{z}\in {w}$
76 74 75 sylibr
77 65 73 76 fun2d
78 simprr
79 eleq1a ${⊢}{x}\in {w}\to \left({z}={x}\to {z}\in {w}\right)$
80 79 necon3bd ${⊢}{x}\in {w}\to \left(¬{z}\in {w}\to {z}\ne {x}\right)$
81 80 impcom ${⊢}\left(¬{z}\in {w}\wedge {x}\in {w}\right)\to {z}\ne {x}$
82 fvunsn ${⊢}{z}\ne {x}\to \left({f}\cup \left\{⟨{z},{y}⟩\right\}\right)\left({x}\right)={f}\left({x}\right)$
83 dfsbcq
84 83 21 syl6rbb
85 81 82 84 3syl
86 85 ralbidva
87 74 86 syl
88 78 87 mpbid
89 simpl3
90 ffun ${⊢}\left({f}\cup \left\{⟨{z},{y}⟩\right\}\right):{w}\cup \left\{{z}\right\}⟶{B}\to \mathrm{Fun}\left({f}\cup \left\{⟨{z},{y}⟩\right\}\right)$
91 ssun2 ${⊢}\left\{⟨{z},{y}⟩\right\}\subseteq {f}\cup \left\{⟨{z},{y}⟩\right\}$
92 vsnid ${⊢}{z}\in \left\{{z}\right\}$
93 67 dmsnop ${⊢}\mathrm{dom}\left\{⟨{z},{y}⟩\right\}=\left\{{z}\right\}$
94 92 93 eleqtrri ${⊢}{z}\in \mathrm{dom}\left\{⟨{z},{y}⟩\right\}$
95 funssfv ${⊢}\left(\mathrm{Fun}\left({f}\cup \left\{⟨{z},{y}⟩\right\}\right)\wedge \left\{⟨{z},{y}⟩\right\}\subseteq {f}\cup \left\{⟨{z},{y}⟩\right\}\wedge {z}\in \mathrm{dom}\left\{⟨{z},{y}⟩\right\}\right)\to \left({f}\cup \left\{⟨{z},{y}⟩\right\}\right)\left({z}\right)=\left\{⟨{z},{y}⟩\right\}\left({z}\right)$
96 91 94 95 mp3an23 ${⊢}\mathrm{Fun}\left({f}\cup \left\{⟨{z},{y}⟩\right\}\right)\to \left({f}\cup \left\{⟨{z},{y}⟩\right\}\right)\left({z}\right)=\left\{⟨{z},{y}⟩\right\}\left({z}\right)$
97 77 90 96 3syl
98 66 67 fvsn ${⊢}\left\{⟨{z},{y}⟩\right\}\left({z}\right)={y}$
99 97 98 syl6req
100 ralsnsg
101 100 elv
102 elsni ${⊢}{x}\in \left\{{z}\right\}\to {x}={z}$
103 102 fveq2d ${⊢}{x}\in \left\{{z}\right\}\to \left({f}\cup \left\{⟨{z},{y}⟩\right\}\right)\left({x}\right)=\left({f}\cup \left\{⟨{z},{y}⟩\right\}\right)\left({z}\right)$
104 103 eqeq2d ${⊢}{x}\in \left\{{z}\right\}\to \left({y}=\left({f}\cup \left\{⟨{z},{y}⟩\right\}\right)\left({x}\right)↔{y}=\left({f}\cup \left\{⟨{z},{y}⟩\right\}\right)\left({z}\right)\right)$
105 104 biimparc ${⊢}\left({y}=\left({f}\cup \left\{⟨{z},{y}⟩\right\}\right)\left({z}\right)\wedge {x}\in \left\{{z}\right\}\right)\to {y}=\left({f}\cup \left\{⟨{z},{y}⟩\right\}\right)\left({x}\right)$
106 sbceq1a
107 105 106 syl
108 107 ralbidva
109 101 108 bitr3id
110 99 109 syl
111 89 110 mpbid
112 ralun
113 88 111 112 syl2anc
114 vex ${⊢}{f}\in \mathrm{V}$
115 snex ${⊢}\left\{⟨{z},{y}⟩\right\}\in \mathrm{V}$
116 114 115 unex ${⊢}{f}\cup \left\{⟨{z},{y}⟩\right\}\in \mathrm{V}$
117 feq1 ${⊢}{g}={f}\cup \left\{⟨{z},{y}⟩\right\}\to \left({g}:{w}\cup \left\{{z}\right\}⟶{B}↔\left({f}\cup \left\{⟨{z},{y}⟩\right\}\right):{w}\cup \left\{{z}\right\}⟶{B}\right)$
118 fveq1 ${⊢}{g}={f}\cup \left\{⟨{z},{y}⟩\right\}\to {g}\left({x}\right)=\left({f}\cup \left\{⟨{z},{y}⟩\right\}\right)\left({x}\right)$
119 118 sbceq1d
120 119 ralbidv
121 117 120 anbi12d
122 116 121 spcev
123 77 113 122 syl2anc
124 123 ex
125 124 exlimdv
126 125 3exp
127 56 64 126 rexlimd
128 55 127 syl5
129 128 a2d
130 47 129 syl5
132 7 13 29 35 43 131 findcard2s ${⊢}{A}\in \mathrm{Fin}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$
133 132 imp ${⊢}\left({A}\in \mathrm{Fin}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$