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

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 fvi 
 |-  ( ran ( y e. B |-> ( `' F " { y } ) ) e. _V -> ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) = ran ( y e. B |-> ( `' F " { y } ) ) )
26 22 23 24 25 4syl 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) = ran ( y e. B |-> ( `' F " { y } ) ) )
27 14 26 raleqtrrdv 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> A. z e. ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) z =/= (/) )
28 fvex 
 |-  ( _I ` ran ( y e. B |-> ( `' F " { y } ) ) ) e. _V
29 28 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 ) )
30 27 29 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 ) )
31 26 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 } ) ) )
32 26 31 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 } ) ) ) )
33 26 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 ) )
34 32 33 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 ) ) )
35 34 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 ) ) )
36 30 35 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 ) )
37 vex 
 |-  f e. _V
38 37 rnex 
 |-  ran f e. _V
39 38 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 )
40 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 } ) ) )
41 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 } ) ) )
42 40 41 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 } ) ) )
43 nfv 
 |-  F/ y ( A e. V /\ F Fn A /\ B C_ ran F )
44 nfcv 
 |-  F/_ y f
45 nfmpt1 
 |-  F/_ y ( y e. B |-> ( `' F " { y } ) )
46 45 nfrn 
 |-  F/_ y ran ( y e. B |-> ( `' F " { y } ) )
47 46 nfuni 
 |-  F/_ y U. ran ( y e. B |-> ( `' F " { y } ) )
48 44 46 47 nff 
 |-  F/ y f : ran ( y e. B |-> ( `' F " { y } ) ) --> U. ran ( y e. B |-> ( `' F " { y } ) )
49 43 48 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 } ) ) )
50 nfv 
 |-  F/ y ( f ` z ) e. z
51 46 50 nfralw 
 |-  F/ y A. z e. ran ( y e. B |-> ( `' F " { y } ) ) ( f ` z ) e. z
52 49 51 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 )
53 17 18 syl 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> F e. _V )
54 53 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 )
55 cnvexg 
 |-  ( F e. _V -> `' F e. _V )
56 imaexg 
 |-  ( `' F e. _V -> ( `' F " { y } ) e. _V )
57 54 55 56 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 )
58 cnvimass 
 |-  ( `' F " { y } ) C_ dom F
59 58 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 )
60 15 fndmd 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> dom F = A )
61 60 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 )
62 59 61 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 )
63 57 62 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 )
64 63 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 ) )
65 52 64 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 )
66 1 rnmptss 
 |-  ( A. y e. B ( `' F " { y } ) e. ~P A -> ran ( y e. B |-> ( `' F " { y } ) ) C_ ~P A )
67 65 66 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 )
68 sspwuni 
 |-  ( ran ( y e. B |-> ( `' F " { y } ) ) C_ ~P A <-> U. ran ( y e. B |-> ( `' F " { y } ) ) C_ A )
69 67 68 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 )
70 42 69 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 )
71 39 70 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 )
72 fnfun 
 |-  ( F Fn A -> Fun F )
73 15 72 syl 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> Fun F )
74 73 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 )
75 sndisj 
 |-  Disj_ y e. B { y }
76 disjpreima 
 |-  ( ( Fun F /\ Disj_ y e. B { y } ) -> Disj_ y e. B ( `' F " { y } ) )
77 74 75 76 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 } ) )
78 disjrnmpt 
 |-  ( Disj_ y e. B ( `' F " { y } ) -> Disj_ z e. ran ( y e. B |-> ( `' F " { y } ) ) z )
79 77 78 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 )
80 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 } ) ) )
81 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 } ) ) )
82 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 )
83 fveq2 
 |-  ( z = u -> ( f ` z ) = ( f ` u ) )
84 id 
 |-  ( z = u -> z = u )
85 83 84 eleq12d 
 |-  ( z = u -> ( ( f ` z ) e. z <-> ( f ` u ) e. u ) )
86 85 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 ) )
87 86 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 )
88 80 82 87 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 )
89 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 ) )
90 fveq2 
 |-  ( z = v -> ( f ` z ) = ( f ` v ) )
91 id 
 |-  ( z = v -> z = v )
92 90 91 eleq12d 
 |-  ( z = v -> ( ( f ` z ) e. z <-> ( f ` v ) e. v ) )
93 92 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 ) )
94 93 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 )
95 81 82 94 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 )
96 89 95 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 )
97 84 91 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 )
98 79 80 81 88 96 97 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 )
99 98 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 ) )
100 99 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 ) )
101 100 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 ) )
102 40 101 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 ) ) )
103 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 ) ) )
104 102 103 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 } ) ) )
105 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 )
106 104 105 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 )
107 f1oen3g 
 |-  ( ( f e. _V /\ f : ran ( y e. B |-> ( `' F " { y } ) ) -1-1-onto-> ran f ) -> ran ( y e. B |-> ( `' F " { y } ) ) ~~ ran f )
108 37 106 107 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 )
109 108 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 } ) ) )
110 22 23 syl 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> ( y e. B |-> ( `' F " { y } ) ) e. _V )
111 110 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 )
112 57 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 ) )
113 52 112 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 )
114 73 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 )
115 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 )
116 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 )
117 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 )
118 116 117 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 )
119 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 )
120 116 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 ) -> t e. ran F )
121 114 115 118 120 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 } ) )
122 121 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 } ) ) )
123 122 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 ) )
124 123 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 ) )
125 124 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 ) ) )
126 52 125 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 ) )
127 113 126 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 ) ) )
128 sneq 
 |-  ( y = t -> { y } = { t } )
129 128 imaeq2d 
 |-  ( y = t -> ( `' F " { y } ) = ( `' F " { t } ) )
130 1 129 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 ) ) )
131 127 130 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 )
132 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 } ) ) )
133 131 132 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 } ) ) )
134 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 } ) ) )
135 111 133 134 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 } ) ) )
136 135 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 )
137 entr 
 |-  ( ( ran f ~~ ran ( y e. B |-> ( `' F " { y } ) ) /\ ran ( y e. B |-> ( `' F " { y } ) ) ~~ B ) -> ran f ~~ B )
138 109 136 137 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 )
139 imass2 
 |-  ( ran f C_ U. ran ( y e. B |-> ( `' F " { y } ) ) -> ( F " ran f ) C_ ( F " U. ran ( y e. B |-> ( `' F " { y } ) ) ) )
140 41 139 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 } ) ) ) )
141 40 140 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 } ) ) ) )
142 imauni 
 |-  ( F " U. ran ( y e. B |-> ( `' F " { y } ) ) ) = U_ z e. ran ( y e. B |-> ( `' F " { y } ) ) ( F " z )
143 imaeq2 
 |-  ( z = ( `' F " { y } ) -> ( F " z ) = ( F " ( `' F " { y } ) ) )
144 53 adantr 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) -> F e. _V )
145 144 55 56 3syl 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) -> ( `' F " { y } ) e. _V )
146 143 145 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 } ) ) )
147 funimacnv 
 |-  ( Fun F -> ( F " ( `' F " { y } ) ) = ( { y } i^i ran F ) )
148 73 147 syl 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> ( F " ( `' F " { y } ) ) = ( { y } i^i ran F ) )
149 148 adantr 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) -> ( F " ( `' F " { y } ) ) = ( { y } i^i ran F ) )
150 6 snssd 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) -> { y } C_ B )
151 150 5 sstrd 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) -> { y } C_ ran F )
152 dfss2 
 |-  ( { y } C_ ran F <-> ( { y } i^i ran F ) = { y } )
153 151 152 sylib 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) -> ( { y } i^i ran F ) = { y } )
154 149 153 eqtrd 
 |-  ( ( ( A e. V /\ F Fn A /\ B C_ ran F ) /\ y e. B ) -> ( F " ( `' F " { y } ) ) = { y } )
155 154 iuneq2dv 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> U_ y e. B ( F " ( `' F " { y } ) ) = U_ y e. B { y } )
156 iunid 
 |-  U_ y e. B { y } = B
157 155 156 eqtrdi 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> U_ y e. B ( F " ( `' F " { y } ) ) = B )
158 146 157 sseqtrd 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> U_ z e. ran ( y e. B |-> ( `' F " { y } ) ) ( F " z ) C_ B )
159 158 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 )
160 142 159 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 )
161 141 160 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 )
162 40 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 } ) ) )
163 162 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 )
164 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 )
165 53 55 syl 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> `' F e. _V )
166 165 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 )
167 imaexg 
 |-  ( `' F e. _V -> ( `' F " { t } ) e. _V )
168 166 167 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 )
169 1 129 elrnmpt1s 
 |-  ( ( t e. B /\ ( `' F " { t } ) e. _V ) -> ( `' F " { t } ) e. ran ( y e. B |-> ( `' F " { y } ) ) )
170 164 168 169 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 } ) ) )
171 162 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 } ) ) )
172 170 171 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 )
173 fvelrn 
 |-  ( ( Fun f /\ ( `' F " { t } ) e. dom f ) -> ( f ` ( `' F " { t } ) ) e. ran f )
174 163 172 173 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 )
175 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 )
176 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 )
177 fveq2 
 |-  ( z = ( `' F " { t } ) -> ( f ` z ) = ( f ` ( `' F " { t } ) ) )
178 id 
 |-  ( z = ( `' F " { t } ) -> z = ( `' F " { t } ) )
179 177 178 eleq12d 
 |-  ( z = ( `' F " { t } ) -> ( ( f ` z ) e. z <-> ( f ` ( `' F " { t } ) ) e. ( `' F " { t } ) ) )
180 179 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 } ) ) )
181 180 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 } ) )
182 170 176 181 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 } ) )
183 fniniseg 
 |-  ( F Fn A -> ( ( f ` ( `' F " { t } ) ) e. ( `' F " { t } ) <-> ( ( f ` ( `' F " { t } ) ) e. A /\ ( F ` ( f ` ( `' F " { t } ) ) ) = t ) ) )
184 183 simplbda 
 |-  ( ( F Fn A /\ ( f ` ( `' F " { t } ) ) e. ( `' F " { t } ) ) -> ( F ` ( f ` ( `' F " { t } ) ) ) = t )
185 175 182 184 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 )
186 fveqeq2 
 |-  ( k = ( f ` ( `' F " { t } ) ) -> ( ( F ` k ) = t <-> ( F ` ( f ` ( `' F " { t } ) ) ) = t ) )
187 186 rspcev 
 |-  ( ( ( f ` ( `' F " { t } ) ) e. ran f /\ ( F ` ( f ` ( `' F " { t } ) ) ) = t ) -> E. k e. ran f ( F ` k ) = t )
188 174 185 187 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 )
189 70 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 )
190 175 189 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 ) )
191 188 190 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 ) )
192 191 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 ) ) )
193 192 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 ) )
194 161 193 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 )
195 138 194 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 ) )
196 breq1 
 |-  ( x = ran f -> ( x ~~ B <-> ran f ~~ B ) )
197 imaeq2 
 |-  ( x = ran f -> ( F " x ) = ( F " ran f ) )
198 197 eqeq1d 
 |-  ( x = ran f -> ( ( F " x ) = B <-> ( F " ran f ) = B ) )
199 196 198 anbi12d 
 |-  ( x = ran f -> ( ( x ~~ B /\ ( F " x ) = B ) <-> ( ran f ~~ B /\ ( F " ran f ) = B ) ) )
200 199 rspcev 
 |-  ( ( ran f e. ~P A /\ ( ran f ~~ B /\ ( F " ran f ) = B ) ) -> E. x e. ~P A ( x ~~ B /\ ( F " x ) = B ) )
201 71 195 200 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 ) )
202 201 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 ) )
203 202 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 ) ) )
204 203 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 ) ) )
205 36 204 mpd 
 |-  ( ( A e. V /\ F Fn A /\ B C_ ran F ) -> E. x e. ~P A ( x ~~ B /\ ( F " x ) = B ) )