Theorem imasaddfnlemg 12756

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

Hypotheses

Ref	Expression
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 ) ) >. } )
imasaddfnlemg.v	|- ( ph -> V e. W )
imasaddfnlemg.x	|- ( ph -> .x. e. C )

Assertion

Ref	Expression
imasaddfnlemg	|- ( ph -> .xb Fn ( B X. B ) )

Distinct variable groups:   q, p, B   a, b, p, q, V   .x. , p, q   F, a, b, p, q   ph, a, b, p, q   .xb , a, b, p, q

Allowed substitution hints:   B( a, b)   C( q, p, a, b)   .x. ( a, b)   W( q, p, a, b)

Proof of Theorem imasaddfnlemg

Dummy variables w y z x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		imasaddf.f	. . . . . . . . . . . . 13 |- ( ph -> F : V -onto-> B )
2		fof 5452	. . . . . . . . . . . . 13 |- ( F : V -onto-> B -> F : V --> B )
3	1, 2	syl 14	. . . . . . . . . . . 12 |- ( ph -> F : V --> B )
4		imasaddfnlemg.v	. . . . . . . . . . . 12 |- ( ph -> V e. W )
5	3, 4	fexd 5761	. . . . . . . . . . 11 |- ( ph -> F e. _V )
6		vex 2754	. . . . . . . . . . 11 |- p e. _V
7		fvexg 5548	. . . . . . . . . . 11 |- ( ( F e. _V /\ p e. _V ) -> ( F ` p ) e. _V )
8	5, 6, 7	sylancl 413	. . . . . . . . . 10 |- ( ph -> ( F ` p ) e. _V )
9		vex 2754	. . . . . . . . . . 11 |- q e. _V
10		fvexg 5548	. . . . . . . . . . 11 |- ( ( F e. _V /\ q e. _V ) -> ( F ` q ) e. _V )
11	5, 9, 10	sylancl 413	. . . . . . . . . 10 |- ( ph -> ( F ` q ) e. _V )
12		opexg 4242	. . . . . . . . . 10 |- ( ( ( F ` p ) e. _V /\ ( F ` q ) e. _V ) -> <. ( F ` p ) , ( F ` q ) >. e. _V )
13	8, 11, 12	syl2anc 411	. . . . . . . . 9 |- ( ph -> <. ( F ` p ) , ( F ` q ) >. e. _V )
14		imasaddfnlemg.x	. . . . . . . . . . 11 |- ( ph -> .x. e. C )
15	9	a1i 9	. . . . . . . . . . 11 |- ( ph -> q e. _V )
16		ovexg 5924	. . . . . . . . . . 11 |- ( ( p e. _V /\ .x. e. C /\ q e. _V ) -> ( p .x. q ) e. _V )
17	6, 14, 15, 16	mp3an2i 1352	. . . . . . . . . 10 |- ( ph -> ( p .x. q ) e. _V )
18		fvexg 5548	. . . . . . . . . 10 |- ( ( F e. _V /\ ( p .x. q ) e. _V ) -> ( F ` ( p .x. q ) ) e. _V )
19	5, 17, 18	syl2anc 411	. . . . . . . . 9 |- ( ph -> ( F ` ( p .x. q ) ) e. _V )
20		relsnopg 4744	. . . . . . . . 9 |- ( ( <. ( F ` p ) , ( F ` q ) >. e. _V /\ ( F ` ( p .x. q ) ) e. _V ) -> Rel { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
21	13, 19, 20	syl2anc 411	. . . . . . . 8 |- ( ph -> Rel { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
22	21	ralrimivw 2563	. . . . . . 7 |- ( ph -> A. q e. V Rel { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
23		reliun 4761	. . . . . . 7 |- ( 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 ) ) >. } )
24	22, 23	sylibr 134	. . . . . 6 |- ( ph -> Rel U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
25	24	ralrimivw 2563	. . . . 5 |- ( ph -> A. p e. V Rel U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
26		reliun 4761	. . . . 5 |- ( 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 ) ) >. } )
27	25, 26	sylibr 134	. . . 4 |- ( ph -> Rel U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
28		imasaddflem.a	. . . . 5 |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
29	28	releqd 4724	. . . 4 |- ( ph -> ( Rel .xb <-> Rel U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } ) )
30	27, 29	mpbird 167	. . 3 |- ( ph -> Rel .xb )
31		ffvelcdm 5664	. . . . . . . . . . . . . . . 16 |- ( ( F : V --> B /\ p e. V ) -> ( F ` p ) e. B )
32		ffvelcdm 5664	. . . . . . . . . . . . . . . 16 |- ( ( F : V --> B /\ q e. V ) -> ( F ` q ) e. B )
33	31, 32	anim12dan 600	. . . . . . . . . . . . . . 15 |- ( ( F : V --> B /\ ( p e. V /\ q e. V ) ) -> ( ( F ` p ) e. B /\ ( F ` q ) e. B ) )
34	3, 33	sylan 283	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( ( F ` p ) e. B /\ ( F ` q ) e. B ) )
35		opelxpi 4672	. . . . . . . . . . . . . 14 |- ( ( ( F ` p ) e. B /\ ( F ` q ) e. B ) -> <. ( F ` p ) , ( F ` q ) >. e. ( B X. B ) )
36	34, 35	syl 14	. . . . . . . . . . . . 13 |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> <. ( F ` p ) , ( F ` q ) >. e. ( B X. B ) )
37	19	adantr 276	. . . . . . . . . . . . 13 |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( F ` ( p .x. q ) ) e. _V )
38	36, 37	opelxpd 4673	. . . . . . . . . . . 12 |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. ( ( B X. B ) X. _V ) )
39	38	snssd 3751	. . . . . . . . . . 11 |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ ( ( B X. B ) X. _V ) )
40	39	anassrs 400	. . . . . . . . . 10 |- ( ( ( ph /\ p e. V ) /\ q e. V ) -> { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ ( ( B X. B ) X. _V ) )
41	40	iunssd 3946	. . . . . . . . 9 |- ( ( ph /\ p e. V ) -> U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ ( ( B X. B ) X. _V ) )
42	41	iunssd 3946	. . . . . . . 8 |- ( ph -> U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ ( ( B X. B ) X. _V ) )
43	28, 42	eqsstrd 3205	. . . . . . 7 |- ( ph -> .xb C_ ( ( B X. B ) X. _V ) )
44		dmss 4840	. . . . . . 7 |- ( .xb C_ ( ( B X. B ) X. _V ) -> dom .xb C_ dom ( ( B X. B ) X. _V ) )
45	43, 44	syl 14	. . . . . 6 |- ( ph -> dom .xb C_ dom ( ( B X. B ) X. _V ) )
46		vn0m 3448	. . . . . . 7 |- E. w w e. _V
47		dmxpm 4861	. . . . . . 7 |- ( E. w w e. _V -> dom ( ( B X. B ) X. _V ) = ( B X. B ) )
48	46, 47	ax-mp 5	. . . . . 6 |- dom ( ( B X. B ) X. _V ) = ( B X. B )
49	45, 48	sseqtrdi 3217	. . . . 5 |- ( ph -> dom .xb C_ ( B X. B ) )
50		forn 5455	. . . . . . 7 |- ( F : V -onto-> B -> ran F = B )
51	1, 50	syl 14	. . . . . 6 |- ( ph -> ran F = B )
52	51	sqxpeqd 4666	. . . . 5 |- ( ph -> ( ran F X. ran F ) = ( B X. B ) )
53	49, 52	sseqtrrd 3208	. . . 4 |- ( ph -> dom .xb C_ ( ran F X. ran F ) )
54	28	eleq2d 2258	. . . . . . . . . . . . 13 |- ( 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 ) ) >. } ) )
55	54	adantr 276	. . . . . . . . . . . 12 |- ( ( 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 ) ) >. } ) )
56		df-br 4018	. . . . . . . . . . . 12 |- ( <. ( F ` a ) , ( F ` b ) >. .xb w <-> <. <. ( F ` a ) , ( F ` b ) >. , w >. e. .xb )
57		eliun 3904	. . . . . . . . . . . . 13 |- ( <. <. ( 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 ) ) >. } )
58		eliun 3904	. . . . . . . . . . . . . 14 |- ( <. <. ( 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 ) ) >. } )
59	58	rexbii 2496	. . . . . . . . . . . . 13 |- ( 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 ) ) >. } )
60	57, 59	bitr2i 185	. . . . . . . . . . . 12 |- ( 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 ) ) >. } )
61	55, 56, 60	3bitr4g 223	. . . . . . . . . . 11 |- ( ( 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 ) ) >. } ) )
62		vex 2754	. . . . . . . . . . . . . . . . . . 19 |- a e. _V
63		fvexg 5548	. . . . . . . . . . . . . . . . . . 19 |- ( ( F e. _V /\ a e. _V ) -> ( F ` a ) e. _V )
64	5, 62, 63	sylancl 413	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( F ` a ) e. _V )
65		vex 2754	. . . . . . . . . . . . . . . . . . 19 |- b e. _V
66		fvexg 5548	. . . . . . . . . . . . . . . . . . 19 |- ( ( F e. _V /\ b e. _V ) -> ( F ` b ) e. _V )
67	5, 65, 66	sylancl 413	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( F ` b ) e. _V )
68		opexg 4242	. . . . . . . . . . . . . . . . . 18 |- ( ( ( F ` a ) e. _V /\ ( F ` b ) e. _V ) -> <. ( F ` a ) , ( F ` b ) >. e. _V )
69	64, 67, 68	syl2anc 411	. . . . . . . . . . . . . . . . 17 |- ( ph -> <. ( F ` a ) , ( F ` b ) >. e. _V )
70		vex 2754	. . . . . . . . . . . . . . . . 17 |- w e. _V
71		opexg 4242	. . . . . . . . . . . . . . . . 17 |- ( ( <. ( F ` a ) , ( F ` b ) >. e. _V /\ w e. _V ) -> <. <. ( F ` a ) , ( F ` b ) >. , w >. e. _V )
72	69, 70, 71	sylancl 413	. . . . . . . . . . . . . . . 16 |- ( ph -> <. <. ( F ` a ) , ( F ` b ) >. , w >. e. _V )
73		elsng 3621	. . . . . . . . . . . . . . . 16 |- ( <. <. ( F ` a ) , ( F ` b ) >. , w >. e. _V -> ( <. <. ( 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 ) ) >. ) )
74	72, 73	syl 14	. . . . . . . . . . . . . . 15 |- ( ph -> ( <. <. ( 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 ) ) >. ) )
75	74	3ad2ant1 1019	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) >. } <-> <. <. ( F ` a ) , ( F ` b ) >. , w >. = <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. ) )
76		opthg 4252	. . . . . . . . . . . . . . . . 17 |- ( ( <. ( F ` a ) , ( F ` b ) >. e. _V /\ w e. _V ) -> ( <. <. ( 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 ) ) ) ) )
77	69, 70, 76	sylancl 413	. . . . . . . . . . . . . . . 16 |- ( ph -> ( <. <. ( 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 ) ) ) ) )
78	77	3ad2ant1 1019	. . . . . . . . . . . . . . 15 |- ( ( 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 ) ) >. <-> ( <. ( F ` a ) , ( F ` b ) >. = <. ( F ` p ) , ( F ` q ) >. /\ w = ( F ` ( p .x. q ) ) ) ) )
79		opthg 4252	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( F ` a ) e. _V /\ ( F ` b ) e. _V ) -> ( <. ( F ` a ) , ( F ` b ) >. = <. ( F ` p ) , ( F ` q ) >. <-> ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) ) )
80	64, 67, 79	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( <. ( F ` a ) , ( F ` b ) >. = <. ( F ` p ) , ( F ` q ) >. <-> ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) ) )
81	80	3ad2ant1 1019	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( <. ( F ` a ) , ( F ` b ) >. = <. ( F ` p ) , ( F ` q ) >. <-> ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) ) )
82		imasaddf.e	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) ) ) )
83	81, 82	sylbid 150	. . . . . . . . . . . . . . . . 17 |- ( ( 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 ) ) ) )
84		eqeq2 2198	. . . . . . . . . . . . . . . . . 18 |- ( ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) -> ( w = ( F ` ( a .x. b ) ) <-> w = ( F ` ( p .x. q ) ) ) )
85	84	biimprd 158	. . . . . . . . . . . . . . . . 17 |- ( ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) -> ( w = ( F ` ( p .x. q ) ) -> w = ( F ` ( a .x. b ) ) ) )
86	83, 85	syl6 33	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) ) ) )
87	86	impd 254	. . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) )
88	78, 87	sylbid 150	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) )
89	75, 88	sylbid 150	. . . . . . . . . . . . 13 |- ( ( 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 ) ) ) )
90	89	3expa 1204	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) ) )
91	90	rexlimdvva 2614	. . . . . . . . . . 11 |- ( ( 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 ) ) ) )
92	61, 91	sylbid 150	. . . . . . . . . 10 |- ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( <. ( F ` a ) , ( F ` b ) >. .xb w -> w = ( F ` ( a .x. b ) ) ) )
93	92	alrimiv 1884	. . . . . . . . 9 |- ( ( ph /\ ( a e. V /\ b e. V ) ) -> A. w ( <. ( F ` a ) , ( F ` b ) >. .xb w -> w = ( F ` ( a .x. b ) ) ) )
94		mo2icl 2930	. . . . . . . . 9 |- ( A. w ( <. ( F ` a ) , ( F ` b ) >. .xb w -> w = ( F ` ( a .x. b ) ) ) -> E* w <. ( F ` a ) , ( F ` b ) >. .xb w )
95	93, 94	syl 14	. . . . . . . 8 |- ( ( ph /\ ( a e. V /\ b e. V ) ) -> E* w <. ( F ` a ) , ( F ` b ) >. .xb w )
96	95	ralrimivva 2571	. . . . . . 7 |- ( ph -> A. a e. V A. b e. V E* w <. ( F ` a ) , ( F ` b ) >. .xb w )
97		fofn 5454	. . . . . . . . . 10 |- ( F : V -onto-> B -> F Fn V )
98	1, 97	syl 14	. . . . . . . . 9 |- ( ph -> F Fn V )
99		opeq2 3793	. . . . . . . . . . . 12 |- ( z = ( F ` b ) -> <. ( F ` a ) , z >. = <. ( F ` a ) , ( F ` b ) >. )
100	99	breq1d 4027	. . . . . . . . . . 11 |- ( z = ( F ` b ) -> ( <. ( F ` a ) , z >. .xb w <-> <. ( F ` a ) , ( F ` b ) >. .xb w ) )
101	100	mobidv 2073	. . . . . . . . . 10 |- ( z = ( F ` b ) -> ( E* w <. ( F ` a ) , z >. .xb w <-> E* w <. ( F ` a ) , ( F ` b ) >. .xb w ) )
102	101	ralrn 5669	. . . . . . . . 9 |- ( 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 ) )
103	98, 102	syl 14	. . . . . . . 8 |- ( 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 ) )
104	103	ralbidv 2489	. . . . . . 7 |- ( 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 ) )
105	96, 104	mpbird 167	. . . . . 6 |- ( ph -> A. a e. V A. z e. ran F E* w <. ( F ` a ) , z >. .xb w )
106		opeq1 3792	. . . . . . . . . . 11 |- ( y = ( F ` a ) -> <. y , z >. = <. ( F ` a ) , z >. )
107	106	breq1d 4027	. . . . . . . . . 10 |- ( y = ( F ` a ) -> ( <. y , z >. .xb w <-> <. ( F ` a ) , z >. .xb w ) )
108	107	mobidv 2073	. . . . . . . . 9 |- ( y = ( F ` a ) -> ( E* w <. y , z >. .xb w <-> E* w <. ( F ` a ) , z >. .xb w ) )
109	108	ralbidv 2489	. . . . . . . 8 |- ( 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 ) )
110	109	ralrn 5669	. . . . . . 7 |- ( 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 ) )
111	98, 110	syl 14	. . . . . 6 |- ( 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 ) )
112	105, 111	mpbird 167	. . . . 5 |- ( ph -> A. y e. ran F A. z e. ran F E* w <. y , z >. .xb w )
113		breq1 4020	. . . . . . 7 |- ( x = <. y , z >. -> ( x .xb w <-> <. y , z >. .xb w ) )
114	113	mobidv 2073	. . . . . 6 |- ( x = <. y , z >. -> ( E* w x .xb w <-> E* w <. y , z >. .xb w ) )
115	114	ralxp 4784	. . . . 5 |- ( 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 )
116	112, 115	sylibr 134	. . . 4 |- ( ph -> A. x e. ( ran F X. ran F ) E* w x .xb w )
117		ssralv 3233	. . . 4 |- ( 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 ) )
118	53, 116, 117	sylc 62	. . 3 |- ( ph -> A. x e. dom .xb E* w x .xb w )
119		dffun7 5257	. . 3 |- ( Fun .xb <-> ( Rel .xb /\ A. x e. dom .xb E* w x .xb w ) )
120	30, 118, 119	sylanbrc 417	. 2 |- ( ph -> Fun .xb )
121		eqimss2 3224	. . . . . . . . . . 11 |- ( .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 )
122	28, 121	syl 14	. . . . . . . . . 10 |- ( ph -> U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb )
123		iunss 3941	. . . . . . . . . 10 |- ( 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 )
124	122, 123	sylib 122	. . . . . . . . 9 |- ( ph -> A. p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb )
125		iunss 3941	. . . . . . . . . . 11 |- ( 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 )
126		opexg 4242	. . . . . . . . . . . . . . 15 |- ( ( <. ( F ` p ) , ( F ` q ) >. e. _V /\ ( F ` ( p .x. q ) ) e. _V ) -> <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. _V )
127	13, 19, 126	syl2anc 411	. . . . . . . . . . . . . 14 |- ( ph -> <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. _V )
128		snssg 3740	. . . . . . . . . . . . . 14 |- ( <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. _V -> ( <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. .xb <-> { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb ) )
129	127, 128	syl 14	. . . . . . . . . . . . 13 |- ( ph -> ( <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. .xb <-> { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb ) )
130		opeldmg 4846	. . . . . . . . . . . . . 14 |- ( ( <. ( F ` p ) , ( F ` q ) >. e. _V /\ ( F ` ( p .x. q ) ) e. _V ) -> ( <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. .xb -> <. ( F ` p ) , ( F ` q ) >. e. dom .xb ) )
131	13, 19, 130	syl2anc 411	. . . . . . . . . . . . 13 |- ( ph -> ( <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. .xb -> <. ( F ` p ) , ( F ` q ) >. e. dom .xb ) )
132	129, 131	sylbird 170	. . . . . . . . . . . 12 |- ( ph -> ( { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb -> <. ( F ` p ) , ( F ` q ) >. e. dom .xb ) )
133	132	ralimdv 2557	. . . . . . . . . . 11 |- ( ph -> ( 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 ) )
134	125, 133	biimtrid 152	. . . . . . . . . 10 |- ( ph -> ( 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 ) )
135	134	ralimdv 2557	. . . . . . . . 9 |- ( ph -> ( 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 ) )
136	124, 135	mpd 13	. . . . . . . 8 |- ( ph -> A. p e. V A. q e. V <. ( F ` p ) , ( F ` q ) >. e. dom .xb )
137		opeq2 3793	. . . . . . . . . . . 12 |- ( z = ( F ` q ) -> <. ( F ` p ) , z >. = <. ( F ` p ) , ( F ` q ) >. )
138	137	eleq1d 2257	. . . . . . . . . . 11 |- ( z = ( F ` q ) -> ( <. ( F ` p ) , z >. e. dom .xb <-> <. ( F ` p ) , ( F ` q ) >. e. dom .xb ) )
139	138	ralrn 5669	. . . . . . . . . 10 |- ( 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 ) )
140	98, 139	syl 14	. . . . . . . . 9 |- ( ph -> ( A. z e. ran F <. ( F ` p ) , z >. e. dom .xb <-> A. q e. V <. ( F ` p ) , ( F ` q ) >. e. dom .xb ) )
141	140	ralbidv 2489	. . . . . . . 8 |- ( 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 ) )
142	136, 141	mpbird 167	. . . . . . 7 |- ( ph -> A. p e. V A. z e. ran F <. ( F ` p ) , z >. e. dom .xb )
143		opeq1 3792	. . . . . . . . . . 11 |- ( y = ( F ` p ) -> <. y , z >. = <. ( F ` p ) , z >. )
144	143	eleq1d 2257	. . . . . . . . . 10 |- ( y = ( F ` p ) -> ( <. y , z >. e. dom .xb <-> <. ( F ` p ) , z >. e. dom .xb ) )
145	144	ralbidv 2489	. . . . . . . . 9 |- ( y = ( F ` p ) -> ( A. z e. ran F <. y , z >. e. dom .xb <-> A. z e. ran F <. ( F ` p ) , z >. e. dom .xb ) )
146	145	ralrn 5669	. . . . . . . 8 |- ( 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 ) )
147	98, 146	syl 14	. . . . . . 7 |- ( 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 ) )
148	142, 147	mpbird 167	. . . . . 6 |- ( ph -> A. y e. ran F A. z e. ran F <. y , z >. e. dom .xb )
149		eleq1 2251	. . . . . . 7 |- ( x = <. y , z >. -> ( x e. dom .xb <-> <. y , z >. e. dom .xb ) )
150	149	ralxp 4784	. . . . . 6 |- ( 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 )
151	148, 150	sylibr 134	. . . . 5 |- ( ph -> A. x e. ( ran F X. ran F ) x e. dom .xb )
152		dfss3 3159	. . . . 5 |- ( ( ran F X. ran F ) C_ dom .xb <-> A. x e. ( ran F X. ran F ) x e. dom .xb )
153	151, 152	sylibr 134	. . . 4 |- ( ph -> ( ran F X. ran F ) C_ dom .xb )
154	52, 153	eqsstrrd 3206	. . 3 |- ( ph -> ( B X. B ) C_ dom .xb )
155	49, 154	eqssd 3186	. 2 |- ( ph -> dom .xb = ( B X. B ) )
156		df-fn 5233	. 2 |- ( .xb Fn ( B X. B ) <-> ( Fun .xb /\ dom .xb = ( B X. B ) ) )
157	120, 155, 156	sylanbrc 417	1 |- ( ph -> .xb Fn ( B X. B ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 979   A.wal 1361   = wceq 1363   E.wex 1502   E*wmo 2038   e. wcel 2159   A.wral 2467   E.wrex 2468   _Vcvv 2751   C_ wss 3143   {csn 3606   <.cop 3609   U_ciun 3900   class class class wbr 4017   X. cxp 4638   dom cdm 4640   ran crn 4641   Rel wrel 4645   Fun wfun 5224   Fn wfn 5225   -->wf 5226   -onto->wfo 5228   ` cfv 5230  (class class class)co 5890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2161  ax-14 2162  ax-ext 2170  ax-coll 4132  ax-sep 4135  ax-pow 4188  ax-pr 4223  ax-un 4447

This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-eu 2040  df-mo 2041  df-clab 2175  df-cleq 2181  df-clel 2184  df-nfc 2320  df-ral 2472  df-rex 2473  df-reu 2474  df-rab 2476  df-v 2753  df-sbc 2977  df-csb 3072  df-un 3147  df-in 3149  df-ss 3156  df-pw 3591  df-sn 3612  df-pr 3613  df-op 3615  df-uni 3824  df-iun 3902  df-br 4018  df-opab 4079  df-mpt 4080  df-id 4307  df-xp 4646  df-rel 4647  df-cnv 4648  df-co 4649  df-dm 4650  df-rn 4651  df-res 4652  df-ima 4653  df-iota 5192  df-fun 5232  df-fn 5233  df-f 5234  df-f1 5235  df-fo 5236  df-f1o 5237  df-fv 5238  df-ov 5893

This theorem is referenced by:  imasaddvallemg  12757  imasaddflemg  12758  imasaddfn  12759  imasmulfn  12762