Metamath Proof Explorer


Theorem imasvscafn

Description: The image structure's scalar multiplication is a function. (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses imasvscaf.u
|- ( ph -> U = ( F "s R ) )
imasvscaf.v
|- ( ph -> V = ( Base ` R ) )
imasvscaf.f
|- ( ph -> F : V -onto-> B )
imasvscaf.r
|- ( ph -> R e. Z )
imasvscaf.g
|- G = ( Scalar ` R )
imasvscaf.k
|- K = ( Base ` G )
imasvscaf.q
|- .x. = ( .s ` R )
imasvscaf.s
|- .xb = ( .s ` U )
imasvscaf.e
|- ( ( ph /\ ( p e. K /\ a e. V /\ q e. V ) ) -> ( ( F ` a ) = ( F ` q ) -> ( F ` ( p .x. a ) ) = ( F ` ( p .x. q ) ) ) )
Assertion imasvscafn
|- ( ph -> .xb Fn ( K X. B ) )

Proof

Step Hyp Ref Expression
1 imasvscaf.u
 |-  ( ph -> U = ( F "s R ) )
2 imasvscaf.v
 |-  ( ph -> V = ( Base ` R ) )
3 imasvscaf.f
 |-  ( ph -> F : V -onto-> B )
4 imasvscaf.r
 |-  ( ph -> R e. Z )
5 imasvscaf.g
 |-  G = ( Scalar ` R )
6 imasvscaf.k
 |-  K = ( Base ` G )
7 imasvscaf.q
 |-  .x. = ( .s ` R )
8 imasvscaf.s
 |-  .xb = ( .s ` U )
9 imasvscaf.e
 |-  ( ( ph /\ ( p e. K /\ a e. V /\ q e. V ) ) -> ( ( F ` a ) = ( F ` q ) -> ( F ` ( p .x. a ) ) = ( F ` ( p .x. q ) ) ) )
10 eqid
 |-  ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) = ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) )
11 fvex
 |-  ( F ` ( p .x. q ) ) e. _V
12 10 11 fnmpoi
 |-  ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) Fn ( K X. { ( F ` q ) } )
13 fnrel
 |-  ( ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) Fn ( K X. { ( F ` q ) } ) -> Rel ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
14 12 13 ax-mp
 |-  Rel ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) )
15 14 rgenw
 |-  A. q e. V Rel ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) )
16 reliun
 |-  ( Rel U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) <-> A. q e. V Rel ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
17 15 16 mpbir
 |-  Rel U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) )
18 1 2 3 4 5 6 7 8 imasvsca
 |-  ( ph -> .xb = U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
19 18 releqd
 |-  ( ph -> ( Rel .xb <-> Rel U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ) )
20 17 19 mpbiri
 |-  ( ph -> Rel .xb )
21 dffn2
 |-  ( ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) Fn ( K X. { ( F ` q ) } ) <-> ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) : ( K X. { ( F ` q ) } ) --> _V )
22 12 21 mpbi
 |-  ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) : ( K X. { ( F ` q ) } ) --> _V
23 fssxp
 |-  ( ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) : ( K X. { ( F ` q ) } ) --> _V -> ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. { ( F ` q ) } ) X. _V ) )
24 22 23 ax-mp
 |-  ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. { ( F ` q ) } ) X. _V )
25 fof
 |-  ( F : V -onto-> B -> F : V --> B )
26 3 25 syl
 |-  ( ph -> F : V --> B )
27 26 ffvelrnda
 |-  ( ( ph /\ q e. V ) -> ( F ` q ) e. B )
28 27 snssd
 |-  ( ( ph /\ q e. V ) -> { ( F ` q ) } C_ B )
29 xpss2
 |-  ( { ( F ` q ) } C_ B -> ( K X. { ( F ` q ) } ) C_ ( K X. B ) )
30 xpss1
 |-  ( ( K X. { ( F ` q ) } ) C_ ( K X. B ) -> ( ( K X. { ( F ` q ) } ) X. _V ) C_ ( ( K X. B ) X. _V ) )
31 28 29 30 3syl
 |-  ( ( ph /\ q e. V ) -> ( ( K X. { ( F ` q ) } ) X. _V ) C_ ( ( K X. B ) X. _V ) )
32 24 31 sstrid
 |-  ( ( ph /\ q e. V ) -> ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. B ) X. _V ) )
33 32 ralrimiva
 |-  ( ph -> A. q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. B ) X. _V ) )
34 iunss
 |-  ( U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. B ) X. _V ) <-> A. q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. B ) X. _V ) )
35 33 34 sylibr
 |-  ( ph -> U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. B ) X. _V ) )
36 18 35 eqsstrd
 |-  ( ph -> .xb C_ ( ( K X. B ) X. _V ) )
37 dmss
 |-  ( .xb C_ ( ( K X. B ) X. _V ) -> dom .xb C_ dom ( ( K X. B ) X. _V ) )
38 36 37 syl
 |-  ( ph -> dom .xb C_ dom ( ( K X. B ) X. _V ) )
39 vn0
 |-  _V =/= (/)
40 dmxp
 |-  ( _V =/= (/) -> dom ( ( K X. B ) X. _V ) = ( K X. B ) )
41 39 40 ax-mp
 |-  dom ( ( K X. B ) X. _V ) = ( K X. B )
42 38 41 sseqtrdi
 |-  ( ph -> dom .xb C_ ( K X. B ) )
43 forn
 |-  ( F : V -onto-> B -> ran F = B )
44 3 43 syl
 |-  ( ph -> ran F = B )
45 44 xpeq2d
 |-  ( ph -> ( K X. ran F ) = ( K X. B ) )
46 42 45 sseqtrrd
 |-  ( ph -> dom .xb C_ ( K X. ran F ) )
47 df-br
 |-  ( <. p , ( F ` a ) >. .xb w <-> <. <. p , ( F ` a ) >. , w >. e. .xb )
48 18 eleq2d
 |-  ( ph -> ( <. <. p , ( F ` a ) >. , w >. e. .xb <-> <. <. p , ( F ` a ) >. , w >. e. U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ) )
49 48 adantr
 |-  ( ( ph /\ ( p e. K /\ a e. V ) ) -> ( <. <. p , ( F ` a ) >. , w >. e. .xb <-> <. <. p , ( F ` a ) >. , w >. e. U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ) )
50 eliun
 |-  ( <. <. p , ( F ` a ) >. , w >. e. U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) <-> E. q e. V <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
51 df-3an
 |-  ( ( p e. K /\ a e. V /\ q e. V ) <-> ( ( p e. K /\ a e. V ) /\ q e. V ) )
52 10 mpofun
 |-  Fun ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) )
53 funopfv
 |-  ( Fun ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> ( ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ` <. p , ( F ` a ) >. ) = w ) )
54 52 53 ax-mp
 |-  ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> ( ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ` <. p , ( F ` a ) >. ) = w )
55 df-ov
 |-  ( p ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ( F ` a ) ) = ( ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ` <. p , ( F ` a ) >. )
56 opex
 |-  <. p , ( F ` a ) >. e. _V
57 vex
 |-  w e. _V
58 56 57 opeldm
 |-  ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> <. p , ( F ` a ) >. e. dom ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
59 10 11 dmmpo
 |-  dom ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) = ( K X. { ( F ` q ) } )
60 58 59 eleqtrdi
 |-  ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> <. p , ( F ` a ) >. e. ( K X. { ( F ` q ) } ) )
61 opelxp
 |-  ( <. p , ( F ` a ) >. e. ( K X. { ( F ` q ) } ) <-> ( p e. K /\ ( F ` a ) e. { ( F ` q ) } ) )
62 60 61 sylib
 |-  ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> ( p e. K /\ ( F ` a ) e. { ( F ` q ) } ) )
63 fvoveq1
 |-  ( z = p -> ( F ` ( z .x. q ) ) = ( F ` ( p .x. q ) ) )
64 eqidd
 |-  ( y = ( F ` a ) -> ( F ` ( p .x. q ) ) = ( F ` ( p .x. q ) ) )
65 fvoveq1
 |-  ( p = z -> ( F ` ( p .x. q ) ) = ( F ` ( z .x. q ) ) )
66 eqidd
 |-  ( x = y -> ( F ` ( z .x. q ) ) = ( F ` ( z .x. q ) ) )
67 65 66 cbvmpov
 |-  ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) = ( z e. K , y e. { ( F ` q ) } |-> ( F ` ( z .x. q ) ) )
68 63 64 67 11 ovmpo
 |-  ( ( p e. K /\ ( F ` a ) e. { ( F ` q ) } ) -> ( p ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ( F ` a ) ) = ( F ` ( p .x. q ) ) )
69 62 68 syl
 |-  ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> ( p ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ( F ` a ) ) = ( F ` ( p .x. q ) ) )
70 55 69 eqtr3id
 |-  ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> ( ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ` <. p , ( F ` a ) >. ) = ( F ` ( p .x. q ) ) )
71 54 70 eqtr3d
 |-  ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> w = ( F ` ( p .x. q ) ) )
72 71 adantl
 |-  ( ( ( ph /\ ( p e. K /\ a e. V /\ q e. V ) ) /\ <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ) -> w = ( F ` ( p .x. q ) ) )
73 elsni
 |-  ( ( F ` a ) e. { ( F ` q ) } -> ( F ` a ) = ( F ` q ) )
74 62 73 simpl2im
 |-  ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> ( F ` a ) = ( F ` q ) )
75 9 74 impel
 |-  ( ( ( ph /\ ( p e. K /\ a e. V /\ q e. V ) ) /\ <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ) -> ( F ` ( p .x. a ) ) = ( F ` ( p .x. q ) ) )
76 72 75 eqtr4d
 |-  ( ( ( ph /\ ( p e. K /\ a e. V /\ q e. V ) ) /\ <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ) -> w = ( F ` ( p .x. a ) ) )
77 76 ex
 |-  ( ( ph /\ ( p e. K /\ a e. V /\ q e. V ) ) -> ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> w = ( F ` ( p .x. a ) ) ) )
78 51 77 sylan2br
 |-  ( ( ph /\ ( ( p e. K /\ a e. V ) /\ q e. V ) ) -> ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> w = ( F ` ( p .x. a ) ) ) )
79 78 anassrs
 |-  ( ( ( ph /\ ( p e. K /\ a e. V ) ) /\ q e. V ) -> ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> w = ( F ` ( p .x. a ) ) ) )
80 79 rexlimdva
 |-  ( ( ph /\ ( p e. K /\ a e. V ) ) -> ( E. q e. V <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> w = ( F ` ( p .x. a ) ) ) )
81 50 80 syl5bi
 |-  ( ( ph /\ ( p e. K /\ a e. V ) ) -> ( <. <. p , ( F ` a ) >. , w >. e. U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> w = ( F ` ( p .x. a ) ) ) )
82 49 81 sylbid
 |-  ( ( ph /\ ( p e. K /\ a e. V ) ) -> ( <. <. p , ( F ` a ) >. , w >. e. .xb -> w = ( F ` ( p .x. a ) ) ) )
83 47 82 syl5bi
 |-  ( ( ph /\ ( p e. K /\ a e. V ) ) -> ( <. p , ( F ` a ) >. .xb w -> w = ( F ` ( p .x. a ) ) ) )
84 83 alrimiv
 |-  ( ( ph /\ ( p e. K /\ a e. V ) ) -> A. w ( <. p , ( F ` a ) >. .xb w -> w = ( F ` ( p .x. a ) ) ) )
85 mo2icl
 |-  ( A. w ( <. p , ( F ` a ) >. .xb w -> w = ( F ` ( p .x. a ) ) ) -> E* w <. p , ( F ` a ) >. .xb w )
86 84 85 syl
 |-  ( ( ph /\ ( p e. K /\ a e. V ) ) -> E* w <. p , ( F ` a ) >. .xb w )
87 86 ralrimivva
 |-  ( ph -> A. p e. K A. a e. V E* w <. p , ( F ` a ) >. .xb w )
88 fofn
 |-  ( F : V -onto-> B -> F Fn V )
89 opeq2
 |-  ( y = ( F ` a ) -> <. p , y >. = <. p , ( F ` a ) >. )
90 89 breq1d
 |-  ( y = ( F ` a ) -> ( <. p , y >. .xb w <-> <. p , ( F ` a ) >. .xb w ) )
91 90 mobidv
 |-  ( y = ( F ` a ) -> ( E* w <. p , y >. .xb w <-> E* w <. p , ( F ` a ) >. .xb w ) )
92 91 ralrn
 |-  ( F Fn V -> ( A. y e. ran F E* w <. p , y >. .xb w <-> A. a e. V E* w <. p , ( F ` a ) >. .xb w ) )
93 3 88 92 3syl
 |-  ( ph -> ( A. y e. ran F E* w <. p , y >. .xb w <-> A. a e. V E* w <. p , ( F ` a ) >. .xb w ) )
94 93 ralbidv
 |-  ( ph -> ( A. p e. K A. y e. ran F E* w <. p , y >. .xb w <-> A. p e. K A. a e. V E* w <. p , ( F ` a ) >. .xb w ) )
95 87 94 mpbird
 |-  ( ph -> A. p e. K A. y e. ran F E* w <. p , y >. .xb w )
96 breq1
 |-  ( x = <. p , y >. -> ( x .xb w <-> <. p , y >. .xb w ) )
97 96 mobidv
 |-  ( x = <. p , y >. -> ( E* w x .xb w <-> E* w <. p , y >. .xb w ) )
98 97 ralxp
 |-  ( A. x e. ( K X. ran F ) E* w x .xb w <-> A. p e. K A. y e. ran F E* w <. p , y >. .xb w )
99 95 98 sylibr
 |-  ( ph -> A. x e. ( K X. ran F ) E* w x .xb w )
100 ssralv
 |-  ( dom .xb C_ ( K X. ran F ) -> ( A. x e. ( K X. ran F ) E* w x .xb w -> A. x e. dom .xb E* w x .xb w ) )
101 46 99 100 sylc
 |-  ( ph -> A. x e. dom .xb E* w x .xb w )
102 dffun7
 |-  ( Fun .xb <-> ( Rel .xb /\ A. x e. dom .xb E* w x .xb w ) )
103 20 101 102 sylanbrc
 |-  ( ph -> Fun .xb )
104 eqimss2
 |-  ( .xb = U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ .xb )
105 18 104 syl
 |-  ( ph -> U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ .xb )
106 iunss
 |-  ( U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ .xb <-> A. q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ .xb )
107 105 106 sylib
 |-  ( ph -> A. q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ .xb )
108 107 r19.21bi
 |-  ( ( ph /\ q e. V ) -> ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ .xb )
109 108 adantrl
 |-  ( ( ph /\ ( p e. K /\ q e. V ) ) -> ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ .xb )
110 dmss
 |-  ( ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ .xb -> dom ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ dom .xb )
111 109 110 syl
 |-  ( ( ph /\ ( p e. K /\ q e. V ) ) -> dom ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ dom .xb )
112 59 111 eqsstrrid
 |-  ( ( ph /\ ( p e. K /\ q e. V ) ) -> ( K X. { ( F ` q ) } ) C_ dom .xb )
113 simprl
 |-  ( ( ph /\ ( p e. K /\ q e. V ) ) -> p e. K )
114 fvex
 |-  ( F ` q ) e. _V
115 114 snid
 |-  ( F ` q ) e. { ( F ` q ) }
116 opelxpi
 |-  ( ( p e. K /\ ( F ` q ) e. { ( F ` q ) } ) -> <. p , ( F ` q ) >. e. ( K X. { ( F ` q ) } ) )
117 113 115 116 sylancl
 |-  ( ( ph /\ ( p e. K /\ q e. V ) ) -> <. p , ( F ` q ) >. e. ( K X. { ( F ` q ) } ) )
118 112 117 sseldd
 |-  ( ( ph /\ ( p e. K /\ q e. V ) ) -> <. p , ( F ` q ) >. e. dom .xb )
119 118 ralrimivva
 |-  ( ph -> A. p e. K A. q e. V <. p , ( F ` q ) >. e. dom .xb )
120 opeq2
 |-  ( y = ( F ` q ) -> <. p , y >. = <. p , ( F ` q ) >. )
121 120 eleq1d
 |-  ( y = ( F ` q ) -> ( <. p , y >. e. dom .xb <-> <. p , ( F ` q ) >. e. dom .xb ) )
122 121 ralrn
 |-  ( F Fn V -> ( A. y e. ran F <. p , y >. e. dom .xb <-> A. q e. V <. p , ( F ` q ) >. e. dom .xb ) )
123 3 88 122 3syl
 |-  ( ph -> ( A. y e. ran F <. p , y >. e. dom .xb <-> A. q e. V <. p , ( F ` q ) >. e. dom .xb ) )
124 123 ralbidv
 |-  ( ph -> ( A. p e. K A. y e. ran F <. p , y >. e. dom .xb <-> A. p e. K A. q e. V <. p , ( F ` q ) >. e. dom .xb ) )
125 119 124 mpbird
 |-  ( ph -> A. p e. K A. y e. ran F <. p , y >. e. dom .xb )
126 eleq1
 |-  ( x = <. p , y >. -> ( x e. dom .xb <-> <. p , y >. e. dom .xb ) )
127 126 ralxp
 |-  ( A. x e. ( K X. ran F ) x e. dom .xb <-> A. p e. K A. y e. ran F <. p , y >. e. dom .xb )
128 125 127 sylibr
 |-  ( ph -> A. x e. ( K X. ran F ) x e. dom .xb )
129 dfss3
 |-  ( ( K X. ran F ) C_ dom .xb <-> A. x e. ( K X. ran F ) x e. dom .xb )
130 128 129 sylibr
 |-  ( ph -> ( K X. ran F ) C_ dom .xb )
131 45 130 eqsstrrd
 |-  ( ph -> ( K X. B ) C_ dom .xb )
132 42 131 eqssd
 |-  ( ph -> dom .xb = ( K X. B ) )
133 df-fn
 |-  ( .xb Fn ( K X. B ) <-> ( Fun .xb /\ dom .xb = ( K X. B ) ) )
134 103 132 133 sylanbrc
 |-  ( ph -> .xb Fn ( K X. B ) )