This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) -> ( ph <-> ps ) )
Assertion ac6sfi 
|- ( ( A e. Fin /\ A. x e. A E. y e. B ph ) -> E. f ( f : A --> B /\ A. x e. A ps ) )

Proof

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