Metamath Proof Explorer

Theorem fnpreimac

Description: Choose a set x containing a preimage of each element of a given set B . (Contributed by Thierry Arnoux, 7-May-2023)

Ref Expression
Assertion fnpreimac 
|- ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> E. x e. ~P A ( x ~~ B /\ ( F " x ) = B ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( y e. B |-> ( `' F " { y } ) ) = ( y e. B |-> ( `' F " { y } ) )
2 1 elrnmpt 
 |-  ( z e. _V -> ( z e. ran ( y e. B |-> ( `' F " { y } ) ) <-> E. y e. B z = ( `' F " { y } ) ) )
3 2 elv 
 |-  ( z e. ran ( y e. B |-> ( `' F " { y } ) ) <-> E. y e. B z = ( `' F " { y } ) )
4 simpr 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) /\ z = ( `' F " { y } ) ) -> z = ( `' F " { y } ) )
5 simpl3 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) -> B C_ ran F )
6 simpr 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) -> y e. B )
7 5 6 sseldd 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) -> y e. ran F )
8 inisegn0 
 |-  ( y e. ran F <-> ( `' F " { y } ) =/= (/) )
9 7 8 sylib 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) -> ( `' F " { y } ) =/= (/) )
10 9 adantr 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) /\ z = ( `' F " { y } ) ) -> ( `' F " { y } ) =/= (/) )
11 4 10 eqnetrd 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) /\ z = ( `' F " { y } ) ) -> z =/= (/) )
12 11 r19.29an 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ E. y e. B z = ( `' F " { y } ) ) -> z =/= (/) )
13 3 12 sylan2b 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ z e. ran ( y e. B |-> ( `' F " { y } ) ) ) -> z =/= (/) )
14 13 ralrimiva 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> A. z e. ran ( y e. B |-> ( `' F " { y } ) ) z =/= (/) )
15 simp2 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> F Fn A )
16 simp1 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> A e. V )
17 15 16 jca 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> ( F Fn A /\ A e. V ) )
18 fnex 
 |-  ( ( F Fn A /\ A e. V ) -> F e. _V )
19 rnexg 
 |-  ( F e. _V -> ran F e. _V )
20 17 18 19 3syl 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> ran F e. _V )
21 simp3 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> B C_ ran F )
22 20 21 ssexd 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> B e. _V )
23 mptexg 
 |-  ( B e. _V -> ( y e. B |-> ( `' F " { y } ) ) e. _V )
24 rnexg 
 |-  ( ( y e. B |-> ( `' F " { y } ) ) e. _V -> ran ( y e. B |-> ( `' F " { y } ) ) e. _V )
25 22 23 24 3syl 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> ran ( y e. B |-> ( `' F " { y } ) ) e. _V )
26 fvi 
 |-  ( ran ( y e. B |-> ( `' F " { y } ) ) e. _V -> ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) = ran ( y e. B |-> ( `' F " { y } ) ) )
27 25 26 syl 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) = ran ( y e. B |-> ( `' F " { y } ) ) )
28 27 raleqdv 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> ( A. z e. ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) z =/= (/) <-> A. z e. ran ( y e. B |-> ( `' F " { y } ) ) z =/= (/) ) )
29 14 28 mpbird 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> A. z e. ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) z =/= (/) )
30 fvex 
 |-  ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) e. _V
31 30 ac5b 
 |-  ( A. z e. ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) z =/= (/) -> E. f ( f : ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) --> U. ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) ( f ` z ) e. z ) )
32 29 31 syl 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> E. f ( f : ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) --> U. ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) ( f ` z ) e. z ) )
33 27 unieqd 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> U. ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) = U. ran ( y e. B |-> ( `' F " { y } ) ) )
34 27 33 feq23d 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> ( f : ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) --> U. ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) <-> f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) )
35 27 raleqdv 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> ( A. z e. ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) ( f ` z ) e. z <-> A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) )
36 34 35 anbi12d 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> ( ( f : ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) --> U. ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) ( f ` z ) e. z ) <-> ( f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) ) )
37 36 exbidv 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> ( E. f ( f : ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) --> U. ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) ( f ` z ) e. z ) <-> E. f ( f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) ) )
38 32 37 mpbid 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> E. f ( f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) )
39 vex 
 |-  f e. _V
40 39 rnex 
 |-  ran f e. _V
41 40 a1i 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ran f e. _V )
42 simplr 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) )
43 frn 
 |-  ( f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) -> ran f C_ U. ran ( y e. B |-> ( `' F " { y } ) ) )
44 42 43 syl 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ran f C_ U. ran ( y e. B |-> ( `' F " { y } ) ) )
45 nfv 
 |-  F/ y ( A e. V /\ F Fn A /\ B C_ ran F )
46 nfcv 
 |-  F/_ y f
47 nfmpt1 
 |-  F/_ y ( y e. B |-> ( `' F " { y } ) )
48 47 nfrn 
 |-  F/_ y ran ( y e. B |-> ( `' F " { y } ) )
49 48 nfuni 
 |-  F/_ y U. ran ( y e. B |-> ( `' F " { y } ) )
50 46 48 49 nff 
 |-  F/ y f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) )
51 45 50 nfan 
 |-  F/ y ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) )
52 nfv 
 |-  F/ y ( f ` z ) e. z
53 48 52 nfralw 
 |-  F/ y A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z
54 51 53 nfan 
 |-  F/ y ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z )
55 17 18 syl 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> F e. _V )
56 55 ad3antrrr 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ y e. B ) -> F e. _V )
57 cnvexg 
 |-  ( F e. _V -> `' F e. _V )
58 imaexg 
 |-  ( `' F e. _V -> ( `' F " { y } ) e. _V )
59 56 57 58 3syl 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ y e. B ) -> ( `' F " { y } ) e. _V )
60 cnvimass 
 |-  ( `' F " { y } ) C_ dom F
61 60 a1i 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ y e. B ) -> ( `' F " { y } ) C_ dom F )
62 15 fndmd 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> dom F = A )
63 62 ad3antrrr 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ y e. B ) -> dom F = A )
64 61 63 sseqtrd 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ y e. B ) -> ( `' F " { y } ) C_ A )
65 59 64 elpwd 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ y e. B ) -> ( `' F " { y } ) e. ~P A )
66 65 ex 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ( y e. B -> ( `' F " { y } ) e. ~P A ) )
67 54 66 ralrimi 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> A. y e. B ( `' F " { y } ) e. ~P A )
68 1 rnmptss 
 |-  ( A. y e. B ( `' F " { y } ) e. ~P A -> ran ( y e. B |-> ( `' F " { y } ) ) C_ ~P A )
69 67 68 syl 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ran ( y e. B |-> ( `' F " { y } ) ) C_ ~P A )
70 sspwuni 
 |-  ( ran ( y e. B |-> ( `' F " { y } ) ) C_ ~P A <-> U. ran ( y e. B |-> ( `' F " { y } ) ) C_ A )
71 69 70 sylib 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> U. ran ( y e. B |-> ( `' F " { y } ) ) C_ A )
72 44 71 sstrd 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ran f C_ A )
73 41 72 elpwd 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ran f e. ~P A )
74 fnfun 
 |-  ( F Fn A -> Fun F )
75 15 74 syl 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> Fun F )
76 75 ad5antr 
 |-  ( ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ u e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ v e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ ( f ` u ) = ( f ` v ) ) -> Fun F )
77 sndisj 
 |-  Disj_ y e. B { y }
78 disjpreima 
 |-  ( ( Fun F /\ Disj_ y e. B { y } ) -> Disj_ y e. B ( `' F " { y } ) )
79 76 77 78 sylancl 
 |-  ( ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ u e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ v e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ ( f ` u ) = ( f ` v ) ) -> Disj_ y e. B ( `' F " { y } ) )
80 disjrnmpt 
 |-  ( Disj_ y e. B ( `' F " { y } ) -> Disj_ z e. ran ( y e. B |-> ( `' F " { y } ) ) z )
81 79 80 syl 
 |-  ( ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ u e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ v e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ ( f ` u ) = ( f ` v ) ) -> Disj_ z e. ran ( y e. B |-> ( `' F " { y } ) ) z )
82 simpllr 
 |-  ( ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ u e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ v e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ ( f ` u ) = ( f ` v ) ) -> u e. ran ( y e. B |-> ( `' F " { y } ) ) )
83 simplr 
 |-  ( ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ u e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ v e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ ( f ` u ) = ( f ` v ) ) -> v e. ran ( y e. B |-> ( `' F " { y } ) ) )
84 simp-4r 
 |-  ( ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ u e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ v e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ ( f ` u ) = ( f ` v ) ) -> A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z )
85 fveq2 
 |-  ( z = u -> ( f ` z ) = ( f ` u ) )
86 id 
 |-  ( z = u -> z = u )
87 85 86 eleq12d 
 |-  ( z = u -> ( ( f ` z ) e. z <-> ( f ` u ) e. u ) )
88 87 rspcv 
 |-  ( u e. ran ( y e. B |-> ( `' F " { y } ) ) -> ( A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z -> ( f ` u ) e. u ) )
89 88 imp 
 |-  ( ( u e. ran ( y e. B |-> ( `' F " { y } ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ( f ` u ) e. u )
90 82 84 89 syl2anc 
 |-  ( ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ u e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ v e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ ( f ` u ) = ( f ` v ) ) -> ( f ` u ) e. u )
91 simpr 
 |-  ( ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ u e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ v e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ ( f ` u ) = ( f ` v ) ) -> ( f ` u ) = ( f ` v ) )
92 fveq2 
 |-  ( z = v -> ( f ` z ) = ( f ` v ) )
93 id 
 |-  ( z = v -> z = v )
94 92 93 eleq12d 
 |-  ( z = v -> ( ( f ` z ) e. z <-> ( f ` v ) e. v ) )
95 94 rspcv 
 |-  ( v e. ran ( y e. B |-> ( `' F " { y } ) ) -> ( A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z -> ( f ` v ) e. v ) )
96 95 imp 
 |-  ( ( v e. ran ( y e. B |-> ( `' F " { y } ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ( f ` v ) e. v )
97 83 84 96 syl2anc 
 |-  ( ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ u e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ v e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ ( f ` u ) = ( f ` v ) ) -> ( f ` v ) e. v )
98 91 97 eqeltrd 
 |-  ( ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ u e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ v e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ ( f ` u ) = ( f ` v ) ) -> ( f ` u ) e. v )
99 86 93 disji 
 |-  ( ( Disj_ z e. ran ( y e. B |-> ( `' F " { y } ) ) z /\ ( u e. ran ( y e. B |-> ( `' F " { y } ) ) /\ v e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ ( ( f ` u ) e. u /\ ( f ` u ) e. v ) ) -> u = v )
100 81 82 83 90 98 99 syl122anc 
 |-  ( ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ u e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ v e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ ( f ` u ) = ( f ` v ) ) -> u = v )
101 100 ex 
 |-  ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ u e. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ v e. ran ( y e. B |-> ( `' F " { y } ) ) ) -> ( ( f ` u ) = ( f ` v ) -> u = v ) )
102 101 anasss 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ ( u e. ran ( y e. B |-> ( `' F " { y } ) ) /\ v e. ran ( y e. B |-> ( `' F " { y } ) ) ) ) -> ( ( f ` u ) = ( f ` v ) -> u = v ) )
103 102 ralrimivva 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> A. u e. ran ( y e. B |-> ( `' F " { y } ) ) A. v e. ran ( y e. B |-> ( `' F " { y } ) ) ( ( f ` u ) = ( f ` v ) -> u = v ) )
104 42 103 jca 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ( f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) /\ A. u e. ran ( y e. B |-> ( `' F " { y } ) ) A. v e. ran ( y e. B |-> ( `' F " { y } ) ) ( ( f ` u ) = ( f ` v ) -> u = v ) ) )
105 dff13 
 |-  ( f : ran ( y e. B |-> ( `' F " { y } ) ) -1-1-> U. ran ( y e. B |-> ( `' F " { y } ) ) <-> ( f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) /\ A. u e. ran ( y e. B |-> ( `' F " { y } ) ) A. v e. ran ( y e. B |-> ( `' F " { y } ) ) ( ( f ` u ) = ( f ` v ) -> u = v ) ) )
106 104 105 sylibr 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> f : ran ( y e. B |-> ( `' F " { y } ) ) -1-1-> U. ran ( y e. B |-> ( `' F " { y } ) ) )
107 f1f1orn 
 |-  ( f : ran ( y e. B |-> ( `' F " { y } ) ) -1-1-> U. ran ( y e. B |-> ( `' F " { y } ) ) -> f : ran ( y e. B |-> ( `' F " { y } ) ) -1-1-onto-> ran f )
108 106 107 syl 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> f : ran ( y e. B |-> ( `' F " { y } ) ) -1-1-onto-> ran f )
109 f1oen3g 
 |-  ( ( f e. _V /\ f : ran ( y e. B |-> ( `' F " { y } ) ) -1-1-onto-> ran f ) -> ran ( y e. B |-> ( `' F " { y } ) ) ~~ ran f )
110 39 108 109 sylancr 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ran ( y e. B |-> ( `' F " { y } ) ) ~~ ran f )
111 110 ensymd 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ran f ~~ ran ( y e. B |-> ( `' F " { y } ) ) )
112 22 23 syl 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> ( y e. B |-> ( `' F " { y } ) ) e. _V )
113 112 ad2antrr 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ( y e. B |-> ( `' F " { y } ) ) e. _V )
114 59 ex 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ( y e. B -> ( `' F " { y } ) e. _V ) )
115 54 114 ralrimi 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> A. y e. B ( `' F " { y } ) e. _V )
116 75 ad5antr 
 |-  ( ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ y e. B ) /\ t e. B ) /\ y =/= t ) -> Fun F )
117 simpr 
 |-  ( ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ y e. B ) /\ t e. B ) /\ y =/= t ) -> y =/= t )
118 21 ad5antr 
 |-  ( ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ y e. B ) /\ t e. B ) /\ y =/= t ) -> B C_ ran F )
119 simpllr 
 |-  ( ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ y e. B ) /\ t e. B ) /\ y =/= t ) -> y e. B )
120 118 119 sseldd 
 |-  ( ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ y e. B ) /\ t e. B ) /\ y =/= t ) -> y e. ran F )
121 simplr 
 |-  ( ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ y e. B ) /\ t e. B ) /\ y =/= t ) -> t e. B )
122 118 121 sseldd 
 |-  ( ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ y e. B ) /\ t e. B ) /\ y =/= t ) -> t e. ran F )
123 116 117 120 122 preimane 
 |-  ( ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ y e. B ) /\ t e. B ) /\ y =/= t ) -> ( `' F " { y } ) =/= ( `' F " { t } ) )
124 123 ex 
 |-  ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ y e. B ) /\ t e. B ) -> ( y =/= t -> ( `' F " { y } ) =/= ( `' F " { t } ) ) )
125 124 necon4d 
 |-  ( ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ y e. B ) /\ t e. B ) -> ( ( `' F " { y } ) = ( `' F " { t } ) -> y = t ) )
126 125 ralrimiva 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ y e. B ) -> A. t e. B ( ( `' F " { y } ) = ( `' F " { t } ) -> y = t ) )
127 126 ex 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ( y e. B -> A. t e. B ( ( `' F " { y } ) = ( `' F " { t } ) -> y = t ) ) )
128 54 127 ralrimi 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> A. y e. B A. t e. B ( ( `' F " { y } ) = ( `' F " { t } ) -> y = t ) )
129 115 128 jca 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ( A. y e. B ( `' F " { y } ) e. _V /\ A. y e. B A. t e. B ( ( `' F " { y } ) = ( `' F " { t } ) -> y = t ) ) )
130 sneq 
 |-  ( y = t -> { y } = { t } )
131 130 imaeq2d 
 |-  ( y = t -> ( `' F " { y } ) = ( `' F " { t } ) )
132 1 131 f1mpt 
 |-  ( ( y e. B |-> ( `' F " { y } ) ) : B -1-1-> _V <-> ( A. y e. B ( `' F " { y } ) e. _V /\ A. y e. B A. t e. B ( ( `' F " { y } ) = ( `' F " { t } ) -> y = t ) ) )
133 129 132 sylibr 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ( y e. B |-> ( `' F " { y } ) ) : B -1-1-> _V )
134 f1f1orn 
 |-  ( ( y e. B |-> ( `' F " { y } ) ) : B -1-1-> _V -> ( y e. B |-> ( `' F " { y } ) ) : B -1-1-onto-> ran ( y e. B |-> ( `' F " { y } ) ) )
135 133 134 syl 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ( y e. B |-> ( `' F " { y } ) ) : B -1-1-onto-> ran ( y e. B |-> ( `' F " { y } ) ) )
136 f1oen3g 
 |-  ( ( ( y e. B |-> ( `' F " { y } ) ) e. _V /\ ( y e. B |-> ( `' F " { y } ) ) : B -1-1-onto-> ran ( y e. B |-> ( `' F " { y } ) ) ) -> B ~~ ran ( y e. B |-> ( `' F " { y } ) ) )
137 113 135 136 syl2anc 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> B ~~ ran ( y e. B |-> ( `' F " { y } ) ) )
138 137 ensymd 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ran ( y e. B |-> ( `' F " { y } ) ) ~~ B )
139 entr 
 |-  ( ( ran f ~~ ran ( y e. B |-> ( `' F " { y } ) ) /\ ran ( y e. B |-> ( `' F " { y } ) ) ~~ B ) -> ran f ~~ B )
140 111 138 139 syl2anc 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ran f ~~ B )
141 imass2 
 |-  ( ran f C_ U. ran ( y e. B |-> ( `' F " { y } ) ) -> ( F " ran f ) C_ ( F " U. ran ( y e. B |-> ( `' F " { y } ) ) ) )
142 43 141 syl 
 |-  ( f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) -> ( F " ran f ) C_ ( F " U. ran ( y e. B |-> ( `' F " { y } ) ) ) )
143 42 142 syl 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ( F " ran f ) C_ ( F " U. ran ( y e. B |-> ( `' F " { y } ) ) ) )
144 imauni 
 |-  ( F " U. ran ( y e. B |-> ( `' F " { y } ) ) ) = U_ z e. ran ( y e. B |-> ( `' F " { y } ) ) ( F " z )
145 imaeq2 
 |-  ( z = ( `' F " { y } ) -> ( F " z ) = ( F " ( `' F " { y } ) ) )
146 55 adantr 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) -> F e. _V )
147 146 57 58 3syl 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) -> ( `' F " { y } ) e. _V )
148 145 147 iunrnmptss 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> U_ z e. ran ( y e. B |-> ( `' F " { y } ) ) ( F " z ) C_ U_ y e. B ( F " ( `' F " { y } ) ) )
149 funimacnv 
 |-  ( Fun F -> ( F " ( `' F " { y } ) ) = ( { y } i^i ran F ) )
150 75 149 syl 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> ( F " ( `' F " { y } ) ) = ( { y } i^i ran F ) )
151 150 adantr 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) -> ( F " ( `' F " { y } ) ) = ( { y } i^i ran F ) )
152 6 snssd 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) -> { y } C_ B )
153 152 5 sstrd 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) -> { y } C_ ran F )
154 df-ss 
 |-  ( { y } C_ ran F <-> ( { y } i^i ran F ) = { y } )
155 153 154 sylib 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) -> ( { y } i^i ran F ) = { y } )
156 151 155 eqtrd 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) -> ( F " ( `' F " { y } ) ) = { y } )
157 156 iuneq2dv 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> U_ y e. B ( F " ( `' F " { y } ) ) = U_ y e. B { y } )
158 iunid 
 |-  U_ y e. B { y } = B
159 157 158 eqtrdi 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> U_ y e. B ( F " ( `' F " { y } ) ) = B )
160 148 159 sseqtrd 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> U_ z e. ran ( y e. B |-> ( `' F " { y } ) ) ( F " z ) C_ B )
161 160 ad2antrr 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> U_ z e. ran ( y e. B |-> ( `' F " { y } ) ) ( F " z ) C_ B )
162 144 161 eqsstrid 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ( F " U. ran ( y e. B |-> ( `' F " { y } ) ) ) C_ B )
163 143 162 sstrd 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ( F " ran f ) C_ B )
164 42 adantr 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ t e. B ) -> f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) )
165 164 ffund 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ t e. B ) -> Fun f )
166 simpr 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ t e. B ) -> t e. B )
167 55 57 syl 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> `' F e. _V )
168 167 ad3antrrr 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ t e. B ) -> `' F e. _V )
169 imaexg 
 |-  ( `' F e. _V -> ( `' F " { t } ) e. _V )
170 168 169 syl 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ t e. B ) -> ( `' F " { t } ) e. _V )
171 1 131 elrnmpt1s 
 |-  ( ( t e. B /\ ( `' F " { t } ) e. _V ) -> ( `' F " { t } ) e. ran ( y e. B |-> ( `' F " { y } ) ) )
172 166 170 171 syl2anc 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ t e. B ) -> ( `' F " { t } ) e. ran ( y e. B |-> ( `' F " { y } ) ) )
173 164 fdmd 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ t e. B ) -> dom f = ran ( y e. B |-> ( `' F " { y } ) ) )
174 172 173 eleqtrrd 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ t e. B ) -> ( `' F " { t } ) e. dom f )
175 fvelrn 
 |-  ( ( Fun f /\ ( `' F " { t } ) e. dom f ) -> ( f ` ( `' F " { t } ) ) e. ran f )
176 165 174 175 syl2anc 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ t e. B ) -> ( f ` ( `' F " { t } ) ) e. ran f )
177 15 ad3antrrr 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ t e. B ) -> F Fn A )
178 simplr 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ t e. B ) -> A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z )
179 fveq2 
 |-  ( z = ( `' F " { t } ) -> ( f ` z ) = ( f ` ( `' F " { t } ) ) )
180 id 
 |-  ( z = ( `' F " { t } ) -> z = ( `' F " { t } ) )
181 179 180 eleq12d 
 |-  ( z = ( `' F " { t } ) -> ( ( f ` z ) e. z <-> ( f ` ( `' F " { t } ) ) e. ( `' F " { t } ) ) )
182 181 rspcv 
 |-  ( ( `' F " { t } ) e. ran ( y e. B |-> ( `' F " { y } ) ) -> ( A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z -> ( f ` ( `' F " { t } ) ) e. ( `' F " { t } ) ) )
183 182 imp 
 |-  ( ( ( `' F " { t } ) e. ran ( y e. B |-> ( `' F " { y } ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ( f ` ( `' F " { t } ) ) e. ( `' F " { t } ) )
184 172 178 183 syl2anc 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ t e. B ) -> ( f ` ( `' F " { t } ) ) e. ( `' F " { t } ) )
185 fniniseg 
 |-  ( F Fn A -> ( ( f ` ( `' F " { t } ) ) e. ( `' F " { t } ) <-> ( ( f ` ( `' F " { t } ) ) e. A /\ ( F ` ( f ` ( `' F " { t } ) ) ) = t ) ) )
186 185 simplbda 
 |-  ( ( F Fn A /\ ( f ` ( `' F " { t } ) ) e. ( `' F " { t } ) ) -> ( F ` ( f ` ( `' F " { t } ) ) ) = t )
187 177 184 186 syl2anc 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ t e. B ) -> ( F ` ( f ` ( `' F " { t } ) ) ) = t )
188 fveqeq2 
 |-  ( k = ( f ` ( `' F " { t } ) ) -> ( ( F ` k ) = t <-> ( F ` ( f ` ( `' F " { t } ) ) ) = t ) )
189 188 rspcev 
 |-  ( ( ( f ` ( `' F " { t } ) ) e. ran f /\ ( F ` ( f ` ( `' F " { t } ) ) ) = t ) -> E. k e. ran f ( F ` k ) = t )
190 176 187 189 syl2anc 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ t e. B ) -> E. k e. ran f ( F ` k ) = t )
191 72 adantr 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ t e. B ) -> ran f C_ A )
192 177 191 fvelimabd 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ t e. B ) -> ( t e. ( F " ran f ) <-> E. k e. ran f ( F ` k ) = t ) )
193 190 192 mpbird 
 |-  ( ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) /\ t e. B ) -> t e. ( F " ran f ) )
194 193 ex 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ( t e. B -> t e. ( F " ran f ) ) )
195 194 ssrdv 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> B C_ ( F " ran f ) )
196 163 195 eqssd 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ( F " ran f ) = B )
197 140 196 jca 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> ( ran f ~~ B /\ ( F " ran f ) = B ) )
198 breq1 
 |-  ( x = ran f -> ( x ~~ B <-> ran f ~~ B ) )
199 imaeq2 
 |-  ( x = ran f -> ( F " x ) = ( F " ran f ) )
200 199 eqeq1d 
 |-  ( x = ran f -> ( ( F " x ) = B <-> ( F " ran f ) = B ) )
201 198 200 anbi12d 
 |-  ( x = ran f -> ( ( x ~~ B /\ ( F " x ) = B ) <-> ( ran f ~~ B /\ ( F " ran f ) = B ) ) )
202 201 rspcev 
 |-  ( ( ran f e. ~P A /\ ( ran f ~~ B /\ ( F " ran f ) = B ) ) -> E. x e. ~P A ( x ~~ B /\ ( F " x ) = B ) )
203 73 197 202 syl2anc 
 |-  ( ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> E. x e. ~P A ( x ~~ B /\ ( F " x ) = B ) )
204 203 anasss 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ ( f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) ) -> E. x e. ~P A ( x ~~ B /\ ( F " x ) = B ) )
205 204 ex 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> ( ( f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> E. x e. ~P A ( x ~~ B /\ ( F " x ) = B ) ) )
206 205 exlimdv 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> ( E. f ( f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) ) /\ A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z ) -> E. x e. ~P A ( x ~~ B /\ ( F " x ) = B ) ) )
207 38 206 mpd 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> E. x e. ~P A ( x ~~ B /\ ( F " x ) = B ) )