Metamath Proof Explorer

Theorem fnchoice

Description: For a finite set, a choice function exists, without using the axiom of choice. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Assertion fnchoice 
|- ( A e. Fin -> E. f ( f Fn A /\ A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) )

Proof

Step Hyp Ref Expression
1 fneq2 
 |-  ( w = (/) -> ( f Fn w <-> f Fn (/) ) )
2 raleq 
 |-  ( w = (/) -> ( A. x e. w ( x =/= (/) -> ( f ` x ) e. x ) <-> A. x e. (/) ( x =/= (/) -> ( f ` x ) e. x ) ) )
3 1 2 anbi12d 
 |-  ( w = (/) -> ( ( f Fn w /\ A. x e. w ( x =/= (/) -> ( f ` x ) e. x ) ) <-> ( f Fn (/) /\ A. x e. (/) ( x =/= (/) -> ( f ` x ) e. x ) ) ) )
4 3 exbidv 
 |-  ( w = (/) -> ( E. f ( f Fn w /\ A. x e. w ( x =/= (/) -> ( f ` x ) e. x ) ) <-> E. f ( f Fn (/) /\ A. x e. (/) ( x =/= (/) -> ( f ` x ) e. x ) ) ) )
5 fneq2 
 |-  ( w = y -> ( f Fn w <-> f Fn y ) )
6 raleq 
 |-  ( w = y -> ( A. x e. w ( x =/= (/) -> ( f ` x ) e. x ) <-> A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) )
7 5 6 anbi12d 
 |-  ( w = y -> ( ( f Fn w /\ A. x e. w ( x =/= (/) -> ( f ` x ) e. x ) ) <-> ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) )
8 7 exbidv 
 |-  ( w = y -> ( E. f ( f Fn w /\ A. x e. w ( x =/= (/) -> ( f ` x ) e. x ) ) <-> E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) )
9 fneq2 
 |-  ( w = ( y u. { z } ) -> ( f Fn w <-> f Fn ( y u. { z } ) ) )
10 raleq 
 |-  ( w = ( y u. { z } ) -> ( A. x e. w ( x =/= (/) -> ( f ` x ) e. x ) <-> A. x e. ( y u. { z } ) ( x =/= (/) -> ( f ` x ) e. x ) ) )
11 9 10 anbi12d 
 |-  ( w = ( y u. { z } ) -> ( ( f Fn w /\ A. x e. w ( x =/= (/) -> ( f ` x ) e. x ) ) <-> ( f Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( f ` x ) e. x ) ) ) )
12 11 exbidv 
 |-  ( w = ( y u. { z } ) -> ( E. f ( f Fn w /\ A. x e. w ( x =/= (/) -> ( f ` x ) e. x ) ) <-> E. f ( f Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( f ` x ) e. x ) ) ) )
13 fneq2 
 |-  ( w = A -> ( f Fn w <-> f Fn A ) )
14 raleq 
 |-  ( w = A -> ( A. x e. w ( x =/= (/) -> ( f ` x ) e. x ) <-> A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) )
15 13 14 anbi12d 
 |-  ( w = A -> ( ( f Fn w /\ A. x e. w ( x =/= (/) -> ( f ` x ) e. x ) ) <-> ( f Fn A /\ A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) ) )
16 15 exbidv 
 |-  ( w = A -> ( E. f ( f Fn w /\ A. x e. w ( x =/= (/) -> ( f ` x ) e. x ) ) <-> E. f ( f Fn A /\ A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) ) )
17 0ex 
 |-  (/) e. _V
18 fneq1 
 |-  ( f = (/) -> ( f Fn (/) <-> (/) Fn (/) ) )
19 eqid 
 |-  (/) = (/)
20 fn0 
 |-  ( (/) Fn (/) <-> (/) = (/) )
21 19 20 mpbir 
 |-  (/) Fn (/)
22 17 18 21 ceqsexv2d 
 |-  E. f f Fn (/)
23 ral0 
 |-  A. x e. (/) ( x =/= (/) -> ( f ` x ) e. x )
24 22 23 exan 
 |-  E. f ( f Fn (/) /\ A. x e. (/) ( x =/= (/) -> ( f ` x ) e. x ) )
25 dffn2 
 |-  ( f Fn y <-> f : y --> _V )
26 25 biimpi 
 |-  ( f Fn y -> f : y --> _V )
27 26 ad2antrl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ z = (/) ) /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) -> f : y --> _V )
28 vex 
 |-  z e. _V
29 28 a1i 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ z = (/) ) /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) -> z e. _V )
30 simpllr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ z = (/) ) /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) -> -. z e. y )
31 vex 
 |-  w e. _V
32 31 a1i 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ z = (/) ) /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) -> w e. _V )
33 fsnunf 
 |-  ( ( f : y --> _V /\ ( z e. _V /\ -. z e. y ) /\ w e. _V ) -> ( f u. { <. z , w >. } ) : ( y u. { z } ) --> _V )
34 27 29 30 32 33 syl121anc 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ z = (/) ) /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) -> ( f u. { <. z , w >. } ) : ( y u. { z } ) --> _V )
35 dffn2 
 |-  ( ( f u. { <. z , w >. } ) Fn ( y u. { z } ) <-> ( f u. { <. z , w >. } ) : ( y u. { z } ) --> _V )
36 34 35 sylibr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ z = (/) ) /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) -> ( f u. { <. z , w >. } ) Fn ( y u. { z } ) )
37 simplr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ z = (/) ) /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) -> z = (/) )
38 simprr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ z = (/) ) /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) -> A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) )
39 nfv 
 |-  F/ x ( z = (/) /\ -. z e. y )
40 nfra1 
 |-  F/ x A. x e. y ( x =/= (/) -> ( f ` x ) e. x )
41 39 40 nfan 
 |-  F/ x ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) )
42 simpr 
 |-  ( ( ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. y ) -> x e. y )
43 simpllr 
 |-  ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) -> -. z e. y )
44 43 adantr 
 |-  ( ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) -> -. z e. y )
45 44 adantr 
 |-  ( ( ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. y ) -> -. z e. y )
46 42 45 jca 
 |-  ( ( ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. y ) -> ( x e. y /\ -. z e. y ) )
47 nelne2 
 |-  ( ( x e. y /\ -. z e. y ) -> x =/= z )
48 47 necomd 
 |-  ( ( x e. y /\ -. z e. y ) -> z =/= x )
49 46 48 syl 
 |-  ( ( ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. y ) -> z =/= x )
50 fvunsn 
 |-  ( z =/= x -> ( ( f u. { <. z , w >. } ) ` x ) = ( f ` x ) )
51 49 50 syl 
 |-  ( ( ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. y ) -> ( ( f u. { <. z , w >. } ) ` x ) = ( f ` x ) )
52 simpllr 
 |-  ( ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) -> A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) )
53 52 adantr 
 |-  ( ( ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. y ) -> A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) )
54 simplr 
 |-  ( ( ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. y ) -> x =/= (/) )
55 neeq1 
 |-  ( u = x -> ( u =/= (/) <-> x =/= (/) ) )
56 fveq2 
 |-  ( u = x -> ( f ` u ) = ( f ` x ) )
57 56 eleq1d 
 |-  ( u = x -> ( ( f ` u ) e. u <-> ( f ` x ) e. u ) )
58 eleq2w 
 |-  ( u = x -> ( ( f ` x ) e. u <-> ( f ` x ) e. x ) )
59 57 58 bitrd 
 |-  ( u = x -> ( ( f ` u ) e. u <-> ( f ` x ) e. x ) )
60 55 59 imbi12d 
 |-  ( u = x -> ( ( u =/= (/) -> ( f ` u ) e. u ) <-> ( x =/= (/) -> ( f ` x ) e. x ) ) )
61 60 cbvralvw 
 |-  ( A. u e. y ( u =/= (/) -> ( f ` u ) e. u ) <-> A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) )
62 60 rspcv 
 |-  ( x e. y -> ( A. u e. y ( u =/= (/) -> ( f ` u ) e. u ) -> ( x =/= (/) -> ( f ` x ) e. x ) ) )
63 61 62 biimtrrid 
 |-  ( x e. y -> ( A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) -> ( x =/= (/) -> ( f ` x ) e. x ) ) )
64 42 53 54 63 syl3c 
 |-  ( ( ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. y ) -> ( f ` x ) e. x )
65 51 64 eqeltrd 
 |-  ( ( ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. y ) -> ( ( f u. { <. z , w >. } ) ` x ) e. x )
66 simp-4l 
 |-  ( ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) -> z = (/) )
67 66 adantr 
 |-  ( ( ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. { z } ) -> z = (/) )
68 simpr 
 |-  ( ( ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. { z } ) -> x e. { z } )
69 simplr 
 |-  ( ( ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. { z } ) -> x =/= (/) )
70 elsni 
 |-  ( x e. { z } -> x = z )
71 70 3ad2ant2 
 |-  ( ( z = (/) /\ x e. { z } /\ x =/= (/) ) -> x = z )
72 simp1 
 |-  ( ( z = (/) /\ x e. { z } /\ x =/= (/) ) -> z = (/) )
73 71 72 eqtrd 
 |-  ( ( z = (/) /\ x e. { z } /\ x =/= (/) ) -> x = (/) )
74 simp3 
 |-  ( ( z = (/) /\ x e. { z } /\ x =/= (/) ) -> x =/= (/) )
75 73 74 pm2.21ddne 
 |-  ( ( z = (/) /\ x e. { z } /\ x =/= (/) ) -> ( ( f u. { <. z , w >. } ) ` x ) e. x )
76 67 68 69 75 syl3anc 
 |-  ( ( ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. { z } ) -> ( ( f u. { <. z , w >. } ) ` x ) e. x )
77 simplr 
 |-  ( ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) -> x e. ( y u. { z } ) )
78 elun 
 |-  ( x e. ( y u. { z } ) <-> ( x e. y \/ x e. { z } ) )
79 77 78 sylib 
 |-  ( ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) -> ( x e. y \/ x e. { z } ) )
80 65 76 79 mpjaodan 
 |-  ( ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) -> ( ( f u. { <. z , w >. } ) ` x ) e. x )
81 80 ex 
 |-  ( ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. ( y u. { z } ) ) -> ( x =/= (/) -> ( ( f u. { <. z , w >. } ) ` x ) e. x ) )
82 81 ex 
 |-  ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) -> ( x e. ( y u. { z } ) -> ( x =/= (/) -> ( ( f u. { <. z , w >. } ) ` x ) e. x ) ) )
83 41 82 ralrimi 
 |-  ( ( ( z = (/) /\ -. z e. y ) /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) -> A. x e. ( y u. { z } ) ( x =/= (/) -> ( ( f u. { <. z , w >. } ) ` x ) e. x ) )
84 37 30 38 83 syl21anc 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ z = (/) ) /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) -> A. x e. ( y u. { z } ) ( x =/= (/) -> ( ( f u. { <. z , w >. } ) ` x ) e. x ) )
85 36 84 jca 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ z = (/) ) /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) -> ( ( f u. { <. z , w >. } ) Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( ( f u. { <. z , w >. } ) ` x ) e. x ) ) )
86 85 ex 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ z = (/) ) -> ( ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) -> ( ( f u. { <. z , w >. } ) Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( ( f u. { <. z , w >. } ) ` x ) e. x ) ) ) )
87 86 eximdv 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ z = (/) ) -> ( E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) -> E. f ( ( f u. { <. z , w >. } ) Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( ( f u. { <. z , w >. } ) ` x ) e. x ) ) ) )
88 vex 
 |-  f e. _V
89 snex 
 |-  { <. z , w >. } e. _V
90 88 89 unex 
 |-  ( f u. { <. z , w >. } ) e. _V
91 fneq1 
 |-  ( g = ( f u. { <. z , w >. } ) -> ( g Fn ( y u. { z } ) <-> ( f u. { <. z , w >. } ) Fn ( y u. { z } ) ) )
92 fveq1 
 |-  ( g = ( f u. { <. z , w >. } ) -> ( g ` x ) = ( ( f u. { <. z , w >. } ) ` x ) )
93 92 eleq1d 
 |-  ( g = ( f u. { <. z , w >. } ) -> ( ( g ` x ) e. x <-> ( ( f u. { <. z , w >. } ) ` x ) e. x ) )
94 93 imbi2d 
 |-  ( g = ( f u. { <. z , w >. } ) -> ( ( x =/= (/) -> ( g ` x ) e. x ) <-> ( x =/= (/) -> ( ( f u. { <. z , w >. } ) ` x ) e. x ) ) )
95 94 ralbidv 
 |-  ( g = ( f u. { <. z , w >. } ) -> ( A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) <-> A. x e. ( y u. { z } ) ( x =/= (/) -> ( ( f u. { <. z , w >. } ) ` x ) e. x ) ) )
96 91 95 anbi12d 
 |-  ( g = ( f u. { <. z , w >. } ) -> ( ( g Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) ) <-> ( ( f u. { <. z , w >. } ) Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( ( f u. { <. z , w >. } ) ` x ) e. x ) ) ) )
97 90 96 spcev 
 |-  ( ( ( f u. { <. z , w >. } ) Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( ( f u. { <. z , w >. } ) ` x ) e. x ) ) -> E. g ( g Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) ) )
98 97 eximi 
 |-  ( E. f ( ( f u. { <. z , w >. } ) Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( ( f u. { <. z , w >. } ) ` x ) e. x ) ) -> E. f E. g ( g Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) ) )
99 87 98 syl6 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ z = (/) ) -> ( E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) -> E. f E. g ( g Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) ) ) )
100 ax5e 
 |-  ( E. f E. g ( g Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) ) -> E. g ( g Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) ) )
101 99 100 syl6 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ z = (/) ) -> ( E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) -> E. g ( g Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) ) ) )
102 101 imp 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ z = (/) ) /\ E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) -> E. g ( g Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) ) )
103 102 an32s 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) /\ z = (/) ) -> E. g ( g Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) ) )
104 fneq1 
 |-  ( f = g -> ( f Fn ( y u. { z } ) <-> g Fn ( y u. { z } ) ) )
105 fveq1 
 |-  ( f = g -> ( f ` x ) = ( g ` x ) )
106 105 eleq1d 
 |-  ( f = g -> ( ( f ` x ) e. x <-> ( g ` x ) e. x ) )
107 106 imbi2d 
 |-  ( f = g -> ( ( x =/= (/) -> ( f ` x ) e. x ) <-> ( x =/= (/) -> ( g ` x ) e. x ) ) )
108 107 ralbidv 
 |-  ( f = g -> ( A. x e. ( y u. { z } ) ( x =/= (/) -> ( f ` x ) e. x ) <-> A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) ) )
109 104 108 anbi12d 
 |-  ( f = g -> ( ( f Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( f ` x ) e. x ) ) <-> ( g Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) ) ) )
110 109 cbvexvw 
 |-  ( E. f ( f Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( f ` x ) e. x ) ) <-> E. g ( g Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) ) )
111 103 110 sylibr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) /\ z = (/) ) -> E. f ( f Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( f ` x ) e. x ) ) )
112 simpllr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) /\ -. z = (/) ) -> -. z e. y )
113 simpr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) /\ -. z = (/) ) -> -. z = (/) )
114 neq0 
 |-  ( -. z = (/) <-> E. w w e. z )
115 113 114 sylib 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) /\ -. z = (/) ) -> E. w w e. z )
116 simplr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) /\ -. z = (/) ) -> E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) )
117 115 116 jca 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) /\ -. z = (/) ) -> ( E. w w e. z /\ E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) )
118 112 117 jca 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) /\ -. z = (/) ) -> ( -. z e. y /\ ( E. w w e. z /\ E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) )
119 exdistrv 
 |-  ( E. w E. f ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) <-> ( E. w w e. z /\ E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) )
120 simprrl 
 |-  ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) -> f Fn y )
121 120 25 sylib 
 |-  ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) -> f : y --> _V )
122 28 a1i 
 |-  ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) -> z e. _V )
123 simpl 
 |-  ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) -> -. z e. y )
124 31 a1i 
 |-  ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) -> w e. _V )
125 121 122 123 124 33 syl121anc 
 |-  ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) -> ( f u. { <. z , w >. } ) : ( y u. { z } ) --> _V )
126 125 35 sylibr 
 |-  ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) -> ( f u. { <. z , w >. } ) Fn ( y u. { z } ) )
127 nfv 
 |-  F/ x -. z e. y
128 nfv 
 |-  F/ x w e. z
129 nfv 
 |-  F/ x f Fn y
130 129 40 nfan 
 |-  F/ x ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) )
131 128 130 nfan 
 |-  F/ x ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) )
132 127 131 nfan 
 |-  F/ x ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) )
133 simpr 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. y ) -> x e. y )
134 simp-4l 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. y ) -> -. z e. y )
135 133 134 jca 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. y ) -> ( x e. y /\ -. z e. y ) )
136 48 50 syl 
 |-  ( ( x e. y /\ -. z e. y ) -> ( ( f u. { <. z , w >. } ) ` x ) = ( f ` x ) )
137 135 136 syl 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. y ) -> ( ( f u. { <. z , w >. } ) ` x ) = ( f ` x ) )
138 simprrr 
 |-  ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) -> A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) )
139 138 ad5ant12 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. y ) -> A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) )
140 simplr 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. y ) -> x =/= (/) )
141 133 139 140 63 syl3c 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. y ) -> ( f ` x ) e. x )
142 137 141 eqeltrd 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. y ) -> ( ( f u. { <. z , w >. } ) ` x ) e. x )
143 simplrl 
 |-  ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) -> w e. z )
144 143 adantr 
 |-  ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) -> w e. z )
145 144 adantr 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. { z } ) -> w e. z )
146 simpr 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. { z } ) -> x e. { z } )
147 146 70 syl 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. { z } ) -> x = z )
148 fveq2 
 |-  ( x = z -> ( ( f u. { <. z , w >. } ) ` x ) = ( ( f u. { <. z , w >. } ) ` z ) )
149 147 148 syl 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. { z } ) -> ( ( f u. { <. z , w >. } ) ` x ) = ( ( f u. { <. z , w >. } ) ` z ) )
150 28 a1i 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. { z } ) -> z e. _V )
151 31 a1i 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. { z } ) -> w e. _V )
152 simp-4l 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. { z } ) -> -. z e. y )
153 120 ad5ant12 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. { z } ) -> f Fn y )
154 153 fndmd 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. { z } ) -> dom f = y )
155 152 154 neleqtrrd 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. { z } ) -> -. z e. dom f )
156 fsnunfv 
 |-  ( ( z e. _V /\ w e. _V /\ -. z e. dom f ) -> ( ( f u. { <. z , w >. } ) ` z ) = w )
157 150 151 155 156 syl3anc 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. { z } ) -> ( ( f u. { <. z , w >. } ) ` z ) = w )
158 149 157 eqtrd 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. { z } ) -> ( ( f u. { <. z , w >. } ) ` x ) = w )
159 145 158 147 3eltr4d 
 |-  ( ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) /\ x e. { z } ) -> ( ( f u. { <. z , w >. } ) ` x ) e. x )
160 simplr 
 |-  ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) -> x e. ( y u. { z } ) )
161 160 78 sylib 
 |-  ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) -> ( x e. y \/ x e. { z } ) )
162 142 159 161 mpjaodan 
 |-  ( ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) /\ x =/= (/) ) -> ( ( f u. { <. z , w >. } ) ` x ) e. x )
163 162 ex 
 |-  ( ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) /\ x e. ( y u. { z } ) ) -> ( x =/= (/) -> ( ( f u. { <. z , w >. } ) ` x ) e. x ) )
164 163 ex 
 |-  ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) -> ( x e. ( y u. { z } ) -> ( x =/= (/) -> ( ( f u. { <. z , w >. } ) ` x ) e. x ) ) )
165 132 164 ralrimi 
 |-  ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) -> A. x e. ( y u. { z } ) ( x =/= (/) -> ( ( f u. { <. z , w >. } ) ` x ) e. x ) )
166 126 165 jca 
 |-  ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) -> ( ( f u. { <. z , w >. } ) Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( ( f u. { <. z , w >. } ) ` x ) e. x ) ) )
167 166 97 syl 
 |-  ( ( -. z e. y /\ ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) -> E. g ( g Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) ) )
168 167 ex 
 |-  ( -. z e. y -> ( ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) -> E. g ( g Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) ) ) )
169 168 2eximdv 
 |-  ( -. z e. y -> ( E. w E. f ( w e. z /\ ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) -> E. w E. f E. g ( g Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) ) ) )
170 119 169 biimtrrid 
 |-  ( -. z e. y -> ( ( E. w w e. z /\ E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) -> E. w E. f E. g ( g Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) ) ) )
171 170 imp 
 |-  ( ( -. z e. y /\ ( E. w w e. z /\ E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) -> E. w E. f E. g ( g Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) ) )
172 100 exlimiv 
 |-  ( E. w E. f E. g ( g Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) ) -> E. g ( g Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) ) )
173 171 172 syl 
 |-  ( ( -. z e. y /\ ( E. w w e. z /\ E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) -> E. g ( g Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( g ` x ) e. x ) ) )
174 173 110 sylibr 
 |-  ( ( -. z e. y /\ ( E. w w e. z /\ E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) ) -> E. f ( f Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( f ` x ) e. x ) ) )
175 118 174 syl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) /\ -. z = (/) ) -> E. f ( f Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( f ` x ) e. x ) ) )
176 111 175 pm2.61dan 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) ) -> E. f ( f Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( f ` x ) e. x ) ) )
177 176 ex 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) -> E. f ( f Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( x =/= (/) -> ( f ` x ) e. x ) ) ) )
178 4 8 12 16 24 177 findcard2s 
 |-  ( A e. Fin -> E. f ( f Fn A /\ A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) )