Metamath Proof Explorer

Theorem imasaddfnlem

Description: The image structure operation is a function if the original operation is compatible with the function. (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses imasaddf.f 
|- ( ph -> F : V -onto-> B )
imasaddf.e 
|- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )
imasaddflem.a 
|- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
Assertion imasaddfnlem 
|- ( ph -> .xb Fn ( B X. B ) )

Proof

Step Hyp Ref Expression
1 imasaddf.f 
 |-  ( ph -> F : V -onto-> B )
2 imasaddf.e 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )
3 imasaddflem.a 
 |-  ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
4 opex 
 |-  <. ( F ` p ) , ( F ` q ) >. e. _V
5 fvex 
 |-  ( F ` ( p .x. q ) ) e. _V
6 4 5 relsnop 
 |-  Rel { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. }
7 6 rgenw 
 |-  A. q e. V Rel { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. }
8 reliun 
 |-  ( Rel U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } <-> A. q e. V Rel { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
9 7 8 mpbir 
 |-  Rel U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. }
10 9 rgenw 
 |-  A. p e. V Rel U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. }
11 reliun 
 |-  ( Rel U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } <-> A. p e. V Rel U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
12 10 11 mpbir 
 |-  Rel U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. }
13 3 releqd 
 |-  ( ph -> ( Rel .xb <-> Rel U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } ) )
14 12 13 mpbiri 
 |-  ( ph -> Rel .xb )
15 fof 
 |-  ( F : V -onto-> B -> F : V --> B )
16 1 15 syl 
 |-  ( ph -> F : V --> B )
17 ffvelrn 
 |-  ( ( F : V --> B /\ p e. V ) -> ( F ` p ) e. B )
18 ffvelrn 
 |-  ( ( F : V --> B /\ q e. V ) -> ( F ` q ) e. B )
19 17 18 anim12dan 
 |-  ( ( F : V --> B /\ ( p e. V /\ q e. V ) ) -> ( ( F ` p ) e. B /\ ( F ` q ) e. B ) )
20 16 19 sylan 
 |-  ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( ( F ` p ) e. B /\ ( F ` q ) e. B ) )
21 opelxpi 
 |-  ( ( ( F ` p ) e. B /\ ( F ` q ) e. B ) -> <. ( F ` p ) , ( F ` q ) >. e. ( B X. B ) )
22 20 21 syl 
 |-  ( ( ph /\ ( p e. V /\ q e. V ) ) -> <. ( F ` p ) , ( F ` q ) >. e. ( B X. B ) )
23 opelxpi 
 |-  ( ( <. ( F ` p ) , ( F ` q ) >. e. ( B X. B ) /\ ( F ` ( p .x. q ) ) e. _V ) -> <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. ( ( B X. B ) X. _V ) )
24 22 5 23 sylancl 
 |-  ( ( ph /\ ( p e. V /\ q e. V ) ) -> <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. ( ( B X. B ) X. _V ) )
25 24 snssd 
 |-  ( ( ph /\ ( p e. V /\ q e. V ) ) -> { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ ( ( B X. B ) X. _V ) )
26 25 anassrs 
 |-  ( ( ( ph /\ p e. V ) /\ q e. V ) -> { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ ( ( B X. B ) X. _V ) )
27 26 iunssd 
 |-  ( ( ph /\ p e. V ) -> U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ ( ( B X. B ) X. _V ) )
28 27 iunssd 
 |-  ( ph -> U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ ( ( B X. B ) X. _V ) )
29 3 28 eqsstrd 
 |-  ( ph -> .xb C_ ( ( B X. B ) X. _V ) )
30 dmss 
 |-  ( .xb C_ ( ( B X. B ) X. _V ) -> dom .xb C_ dom ( ( B X. B ) X. _V ) )
31 29 30 syl 
 |-  ( ph -> dom .xb C_ dom ( ( B X. B ) X. _V ) )
32 vn0 
 |-  _V =/= (/)
33 dmxp 
 |-  ( _V =/= (/) -> dom ( ( B X. B ) X. _V ) = ( B X. B ) )
34 32 33 ax-mp 
 |-  dom ( ( B X. B ) X. _V ) = ( B X. B )
35 31 34 sseqtrdi 
 |-  ( ph -> dom .xb C_ ( B X. B ) )
36 forn 
 |-  ( F : V -onto-> B -> ran F = B )
37 1 36 syl 
 |-  ( ph -> ran F = B )
38 37 sqxpeqd 
 |-  ( ph -> ( ran F X. ran F ) = ( B X. B ) )
39 35 38 sseqtrrd 
 |-  ( ph -> dom .xb C_ ( ran F X. ran F ) )
40 3 eleq2d 
 |-  ( ph -> ( <. <. ( F ` a ) , ( F ` b ) >. , w >. e. .xb <-> <. <. ( F ` a ) , ( F ` b ) >. , w >. e. U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } ) )
41 40 adantr 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( <. <. ( F ` a ) , ( F ` b ) >. , w >. e. .xb <-> <. <. ( F ` a ) , ( F ` b ) >. , w >. e. U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } ) )
42 df-br 
 |-  ( <. ( F ` a ) , ( F ` b ) >. .xb w <-> <. <. ( F ` a ) , ( F ` b ) >. , w >. e. .xb )
43 eliun 
 |-  ( <. <. ( F ` a ) , ( F ` b ) >. , w >. e. U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } <-> E. p e. V <. <. ( F ` a ) , ( F ` b ) >. , w >. e. U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
44 eliun 
 |-  ( <. <. ( F ` a ) , ( F ` b ) >. , w >. e. U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } <-> E. q e. V <. <. ( F ` a ) , ( F ` b ) >. , w >. e. { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
45 44 rexbii 
 |-  ( E. p e. V <. <. ( F ` a ) , ( F ` b ) >. , w >. e. U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } <-> E. p e. V E. q e. V <. <. ( F ` a ) , ( F ` b ) >. , w >. e. { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
46 43 45 bitr2i 
 |-  ( E. p e. V E. q e. V <. <. ( F ` a ) , ( F ` b ) >. , w >. e. { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } <-> <. <. ( F ` a ) , ( F ` b ) >. , w >. e. U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
47 41 42 46 3bitr4g 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( <. ( F ` a ) , ( F ` b ) >. .xb w <-> E. p e. V E. q e. V <. <. ( F ` a ) , ( F ` b ) >. , w >. e. { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } ) )
48 opex 
 |-  <. <. ( F ` a ) , ( F ` b ) >. , w >. e. _V
49 48 elsn 
 |-  ( <. <. ( F ` a ) , ( F ` b ) >. , w >. e. { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } <-> <. <. ( F ` a ) , ( F ` b ) >. , w >. = <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. )
50 opex 
 |-  <. ( F ` a ) , ( F ` b ) >. e. _V
51 vex 
 |-  w e. _V
52 50 51 opth 
 |-  ( <. <. ( F ` a ) , ( F ` b ) >. , w >. = <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. <-> ( <. ( F ` a ) , ( F ` b ) >. = <. ( F ` p ) , ( F ` q ) >. /\ w = ( F ` ( p .x. q ) ) ) )
53 fvex 
 |-  ( F ` a ) e. _V
54 fvex 
 |-  ( F ` b ) e. _V
55 53 54 opth 
 |-  ( <. ( F ` a ) , ( F ` b ) >. = <. ( F ` p ) , ( F ` q ) >. <-> ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) )
56 55 2 syl5bi 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( <. ( F ` a ) , ( F ` b ) >. = <. ( F ` p ) , ( F ` q ) >. -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )
57 eqeq2 
 |-  ( ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) -> ( w = ( F ` ( a .x. b ) ) <-> w = ( F ` ( p .x. q ) ) ) )
58 57 biimprd 
 |-  ( ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) -> ( w = ( F ` ( p .x. q ) ) -> w = ( F ` ( a .x. b ) ) ) )
59 56 58 syl6 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( <. ( F ` a ) , ( F ` b ) >. = <. ( F ` p ) , ( F ` q ) >. -> ( w = ( F ` ( p .x. q ) ) -> w = ( F ` ( a .x. b ) ) ) ) )
60 59 impd 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( <. ( F ` a ) , ( F ` b ) >. = <. ( F ` p ) , ( F ` q ) >. /\ w = ( F ` ( p .x. q ) ) ) -> w = ( F ` ( a .x. b ) ) ) )
61 52 60 syl5bi 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( <. <. ( F ` a ) , ( F ` b ) >. , w >. = <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. -> w = ( F ` ( a .x. b ) ) ) )
62 49 61 syl5bi 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( <. <. ( F ` a ) , ( F ` b ) >. , w >. e. { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } -> w = ( F ` ( a .x. b ) ) ) )
63 62 3expa 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( p e. V /\ q e. V ) ) -> ( <. <. ( F ` a ) , ( F ` b ) >. , w >. e. { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } -> w = ( F ` ( a .x. b ) ) ) )
64 63 rexlimdvva 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( E. p e. V E. q e. V <. <. ( F ` a ) , ( F ` b ) >. , w >. e. { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } -> w = ( F ` ( a .x. b ) ) ) )
65 47 64 sylbid 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( <. ( F ` a ) , ( F ` b ) >. .xb w -> w = ( F ` ( a .x. b ) ) ) )
66 65 alrimiv 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> A. w ( <. ( F ` a ) , ( F ` b ) >. .xb w -> w = ( F ` ( a .x. b ) ) ) )
67 mo2icl 
 |-  ( A. w ( <. ( F ` a ) , ( F ` b ) >. .xb w -> w = ( F ` ( a .x. b ) ) ) -> E* w <. ( F ` a ) , ( F ` b ) >. .xb w )
68 66 67 syl 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> E* w <. ( F ` a ) , ( F ` b ) >. .xb w )
69 68 ralrimivva 
 |-  ( ph -> A. a e. V A. b e. V E* w <. ( F ` a ) , ( F ` b ) >. .xb w )
70 fofn 
 |-  ( F : V -onto-> B -> F Fn V )
71 1 70 syl 
 |-  ( ph -> F Fn V )
72 opeq2 
 |-  ( z = ( F ` b ) -> <. ( F ` a ) , z >. = <. ( F ` a ) , ( F ` b ) >. )
73 72 breq1d 
 |-  ( z = ( F ` b ) -> ( <. ( F ` a ) , z >. .xb w <-> <. ( F ` a ) , ( F ` b ) >. .xb w ) )
74 73 mobidv 
 |-  ( z = ( F ` b ) -> ( E* w <. ( F ` a ) , z >. .xb w <-> E* w <. ( F ` a ) , ( F ` b ) >. .xb w ) )
75 74 ralrn 
 |-  ( F Fn V -> ( A. z e. ran F E* w <. ( F ` a ) , z >. .xb w <-> A. b e. V E* w <. ( F ` a ) , ( F ` b ) >. .xb w ) )
76 71 75 syl 
 |-  ( ph -> ( A. z e. ran F E* w <. ( F ` a ) , z >. .xb w <-> A. b e. V E* w <. ( F ` a ) , ( F ` b ) >. .xb w ) )
77 76 ralbidv 
 |-  ( ph -> ( A. a e. V A. z e. ran F E* w <. ( F ` a ) , z >. .xb w <-> A. a e. V A. b e. V E* w <. ( F ` a ) , ( F ` b ) >. .xb w ) )
78 69 77 mpbird 
 |-  ( ph -> A. a e. V A. z e. ran F E* w <. ( F ` a ) , z >. .xb w )
79 opeq1 
 |-  ( y = ( F ` a ) -> <. y , z >. = <. ( F ` a ) , z >. )
80 79 breq1d 
 |-  ( y = ( F ` a ) -> ( <. y , z >. .xb w <-> <. ( F ` a ) , z >. .xb w ) )
81 80 mobidv 
 |-  ( y = ( F ` a ) -> ( E* w <. y , z >. .xb w <-> E* w <. ( F ` a ) , z >. .xb w ) )
82 81 ralbidv 
 |-  ( y = ( F ` a ) -> ( A. z e. ran F E* w <. y , z >. .xb w <-> A. z e. ran F E* w <. ( F ` a ) , z >. .xb w ) )
83 82 ralrn 
 |-  ( F Fn V -> ( A. y e. ran F A. z e. ran F E* w <. y , z >. .xb w <-> A. a e. V A. z e. ran F E* w <. ( F ` a ) , z >. .xb w ) )
84 71 83 syl 
 |-  ( ph -> ( A. y e. ran F A. z e. ran F E* w <. y , z >. .xb w <-> A. a e. V A. z e. ran F E* w <. ( F ` a ) , z >. .xb w ) )
85 78 84 mpbird 
 |-  ( ph -> A. y e. ran F A. z e. ran F E* w <. y , z >. .xb w )
86 breq1 
 |-  ( x = <. y , z >. -> ( x .xb w <-> <. y , z >. .xb w ) )
87 86 mobidv 
 |-  ( x = <. y , z >. -> ( E* w x .xb w <-> E* w <. y , z >. .xb w ) )
88 87 ralxp 
 |-  ( A. x e. ( ran F X. ran F ) E* w x .xb w <-> A. y e. ran F A. z e. ran F E* w <. y , z >. .xb w )
89 85 88 sylibr 
 |-  ( ph -> A. x e. ( ran F X. ran F ) E* w x .xb w )
90 ssralv 
 |-  ( dom .xb C_ ( ran F X. ran F ) -> ( A. x e. ( ran F X. ran F ) E* w x .xb w -> A. x e. dom .xb E* w x .xb w ) )
91 39 89 90 sylc 
 |-  ( ph -> A. x e. dom .xb E* w x .xb w )
92 dffun7 
 |-  ( Fun .xb <-> ( Rel .xb /\ A. x e. dom .xb E* w x .xb w ) )
93 14 91 92 sylanbrc 
 |-  ( ph -> Fun .xb )
94 eqimss2 
 |-  ( .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } -> U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb )
95 3 94 syl 
 |-  ( ph -> U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb )
96 iunss 
 |-  ( U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb <-> A. p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb )
97 95 96 sylib 
 |-  ( ph -> A. p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb )
98 iunss 
 |-  ( U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb <-> A. q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb )
99 opex 
 |-  <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. _V
100 99 snss 
 |-  ( <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. .xb <-> { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb )
101 4 5 opeldm 
 |-  ( <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. .xb -> <. ( F ` p ) , ( F ` q ) >. e. dom .xb )
102 100 101 sylbir 
 |-  ( { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb -> <. ( F ` p ) , ( F ` q ) >. e. dom .xb )
103 102 ralimi 
 |-  ( A. q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb -> A. q e. V <. ( F ` p ) , ( F ` q ) >. e. dom .xb )
104 98 103 sylbi 
 |-  ( U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb -> A. q e. V <. ( F ` p ) , ( F ` q ) >. e. dom .xb )
105 104 ralimi 
 |-  ( A. p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb -> A. p e. V A. q e. V <. ( F ` p ) , ( F ` q ) >. e. dom .xb )
106 97 105 syl 
 |-  ( ph -> A. p e. V A. q e. V <. ( F ` p ) , ( F ` q ) >. e. dom .xb )
107 opeq2 
 |-  ( z = ( F ` q ) -> <. ( F ` p ) , z >. = <. ( F ` p ) , ( F ` q ) >. )
108 107 eleq1d 
 |-  ( z = ( F ` q ) -> ( <. ( F ` p ) , z >. e. dom .xb <-> <. ( F ` p ) , ( F ` q ) >. e. dom .xb ) )
109 108 ralrn 
 |-  ( F Fn V -> ( A. z e. ran F <. ( F ` p ) , z >. e. dom .xb <-> A. q e. V <. ( F ` p ) , ( F ` q ) >. e. dom .xb ) )
110 71 109 syl 
 |-  ( ph -> ( A. z e. ran F <. ( F ` p ) , z >. e. dom .xb <-> A. q e. V <. ( F ` p ) , ( F ` q ) >. e. dom .xb ) )
111 110 ralbidv 
 |-  ( ph -> ( A. p e. V A. z e. ran F <. ( F ` p ) , z >. e. dom .xb <-> A. p e. V A. q e. V <. ( F ` p ) , ( F ` q ) >. e. dom .xb ) )
112 106 111 mpbird 
 |-  ( ph -> A. p e. V A. z e. ran F <. ( F ` p ) , z >. e. dom .xb )
113 opeq1 
 |-  ( y = ( F ` p ) -> <. y , z >. = <. ( F ` p ) , z >. )
114 113 eleq1d 
 |-  ( y = ( F ` p ) -> ( <. y , z >. e. dom .xb <-> <. ( F ` p ) , z >. e. dom .xb ) )
115 114 ralbidv 
 |-  ( y = ( F ` p ) -> ( A. z e. ran F <. y , z >. e. dom .xb <-> A. z e. ran F <. ( F ` p ) , z >. e. dom .xb ) )
116 115 ralrn 
 |-  ( F Fn V -> ( A. y e. ran F A. z e. ran F <. y , z >. e. dom .xb <-> A. p e. V A. z e. ran F <. ( F ` p ) , z >. e. dom .xb ) )
117 71 116 syl 
 |-  ( ph -> ( A. y e. ran F A. z e. ran F <. y , z >. e. dom .xb <-> A. p e. V A. z e. ran F <. ( F ` p ) , z >. e. dom .xb ) )
118 112 117 mpbird 
 |-  ( ph -> A. y e. ran F A. z e. ran F <. y , z >. e. dom .xb )
119 eleq1 
 |-  ( x = <. y , z >. -> ( x e. dom .xb <-> <. y , z >. e. dom .xb ) )
120 119 ralxp 
 |-  ( A. x e. ( ran F X. ran F ) x e. dom .xb <-> A. y e. ran F A. z e. ran F <. y , z >. e. dom .xb )
121 118 120 sylibr 
 |-  ( ph -> A. x e. ( ran F X. ran F ) x e. dom .xb )
122 dfss3 
 |-  ( ( ran F X. ran F ) C_ dom .xb <-> A. x e. ( ran F X. ran F ) x e. dom .xb )
123 121 122 sylibr 
 |-  ( ph -> ( ran F X. ran F ) C_ dom .xb )
124 38 123 eqsstrrd 
 |-  ( ph -> ( B X. B ) C_ dom .xb )
125 35 124 eqssd 
 |-  ( ph -> dom .xb = ( B X. B ) )
126 df-fn 
 |-  ( .xb Fn ( B X. B ) <-> ( Fun .xb /\ dom .xb = ( B X. B ) ) )
127 93 125 126 sylanbrc 
 |-  ( ph -> .xb Fn ( B X. B ) )