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⁡x→φ↔ψ
Assertion ac6sfi ⊢A∈Fin∧∀x∈A∃y∈Bφ→∃ff:A⟶B∧∀x∈Aψ

Proof

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