Theorem fliftfun 5379

Description: The function F is the unique function defined by F ` A = B, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)

Hypotheses

Ref	Expression
flift.1	|- F = ran (x e. X |-> <.A , B >.)
flift.2	|- ((ph /\ x e. X) -> A e. R)
flift.3	|- ((ph /\ x e. X) -> B e. S)
fliftfun.4	|- (x = y -> A = C)
fliftfun.5	|- (x = y -> B = D)

Assertion

Ref	Expression
fliftfun	|- (ph -> ( Fun F <-> A.x e. X A.y e. X (A = C -> B = D)))

Distinct variable groups:   y,A   y,B   x, C   x,y, R   x, D   y, F   ph,x,y   x, X,y   x, S,y

Allowed substitution hints:   A(x)   B(x)   C(y)   D(y)   F(x)

Proof of Theorem fliftfun

Dummy variables v u z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1418	. . 3 |- F/xph
2		flift.1	. . . . 5 |- F = ran (x e. X |-> <.A , B >.)
3		nfmpt1 3841	. . . . . 6 |- F/_x(x e. X |-> <.A , B >.)
4	3	nfrn 4522	. . . . 5 |- F/_x ran (x e. X |-> <.A , B >.)
5	2, 4	nfcxfr 2172	. . . 4 |- F/_x F
6	5	nffun 4867	. . 3 |- F/x Fun F
7		fveq2 5121	. . . . . . 7 |- (A = C -> ( F ` A) = ( F ` C))
8		simplr 482	. . . . . . . . 9 |- (((ph /\ Fun F) /\ (x e. X /\ y e. X)) -> Fun F)
9		flift.2	. . . . . . . . . . 11 |- ((ph /\ x e. X) -> A e. R)
10		flift.3	. . . . . . . . . . 11 |- ((ph /\ x e. X) -> B e. S)
11	2, 9, 10	fliftel1 5377	. . . . . . . . . 10 |- ((ph /\ x e. X) -> A FB)
12	11	ad2ant2r 478	. . . . . . . . 9 |- (((ph /\ Fun F) /\ (x e. X /\ y e. X)) -> A FB)
13		funbrfv 5155	. . . . . . . . 9 |- ( Fun F -> (A FB -> ( F ` A) = B))
14	8, 12, 13	sylc 56	. . . . . . . 8 |- (((ph /\ Fun F) /\ (x e. X /\ y e. X)) -> ( F ` A) = B)
15		simprr 484	. . . . . . . . . . 11 |- (((ph /\ Fun F) /\ (x e. X /\ y e. X)) -> y e. X)
16		eqidd 2038	. . . . . . . . . . 11 |- (((ph /\ Fun F) /\ (x e. X /\ y e. X)) -> C = C)
17		eqidd 2038	. . . . . . . . . . 11 |- (((ph /\ Fun F) /\ (x e. X /\ y e. X)) -> D = D)
18		fliftfun.4	. . . . . . . . . . . . . 14 |- (x = y -> A = C)
19	18	eqeq2d 2048	. . . . . . . . . . . . 13 |- (x = y -> ( C = A <-> C = C))
20		fliftfun.5	. . . . . . . . . . . . . 14 |- (x = y -> B = D)
21	20	eqeq2d 2048	. . . . . . . . . . . . 13 |- (x = y -> ( D = B <-> D = D))
22	19, 21	anbi12d 442	. . . . . . . . . . . 12 |- (x = y -> (( C = A /\ D = B) <-> ( C = C /\ D = D)))
23	22	rspcev 2650	. . . . . . . . . . 11 |- ((y e. X /\ ( C = C /\ D = D)) -> E.x e. X ( C = A /\ D = B))
24	15, 16, 17, 23	syl12anc 1132	. . . . . . . . . 10 |- (((ph /\ Fun F) /\ (x e. X /\ y e. X)) -> E.x e. X ( C = A /\ D = B))
25	2, 9, 10	fliftel 5376	. . . . . . . . . . 11 |- (ph -> ( C F D <-> E.x e. X ( C = A /\ D = B)))
26	25	ad2antrr 457	. . . . . . . . . 10 |- (((ph /\ Fun F) /\ (x e. X /\ y e. X)) -> ( C F D <-> E.x e. X ( C = A /\ D = B)))
27	24, 26	mpbird 156	. . . . . . . . 9 |- (((ph /\ Fun F) /\ (x e. X /\ y e. X)) -> C F D)
28		funbrfv 5155	. . . . . . . . 9 |- ( Fun F -> ( C F D -> ( F ` C) = D))
29	8, 27, 28	sylc 56	. . . . . . . 8 |- (((ph /\ Fun F) /\ (x e. X /\ y e. X)) -> ( F ` C) = D)
30	14, 29	eqeq12d 2051	. . . . . . 7 |- (((ph /\ Fun F) /\ (x e. X /\ y e. X)) -> (( F ` A) = ( F ` C) <-> B = D))
31	7, 30	syl5ib 143	. . . . . 6 |- (((ph /\ Fun F) /\ (x e. X /\ y e. X)) -> (A = C -> B = D))
32	31	anassrs 380	. . . . 5 |- ((((ph /\ Fun F) /\ x e. X) /\ y e. X) -> (A = C -> B = D))
33	32	ralrimiva 2386	. . . 4 |- (((ph /\ Fun F) /\ x e. X) -> A.y e. X (A = C -> B = D))
34	33	exp31 346	. . 3 |- (ph -> ( Fun F -> (x e. X -> A.y e. X (A = C -> B = D))))
35	1, 6, 34	ralrimd 2391	. 2 |- (ph -> ( Fun F -> A.x e. X A.y e. X (A = C -> B = D)))
36	2, 9, 10	fliftel 5376	. . . . . . . . 9 |- (ph -> (z Fu <-> E.x e. X (z = A /\ u = B)))
37	2, 9, 10	fliftel 5376	. . . . . . . . . 10 |- (ph -> (z Fv <-> E.x e. X (z = A /\ v = B)))
38	18	eqeq2d 2048	. . . . . . . . . . . 12 |- (x = y -> (z = A <-> z = C))
39	20	eqeq2d 2048	. . . . . . . . . . . 12 |- (x = y -> (v = B <-> v = D))
40	38, 39	anbi12d 442	. . . . . . . . . . 11 |- (x = y -> ((z = A /\ v = B) <-> (z = C /\ v = D)))
41	40	cbvrexv 2528	. . . . . . . . . 10 |- (E.x e. X (z = A /\ v = B) <-> E.y e. X (z = C /\ v = D))
42	37, 41	syl6bb 185	. . . . . . . . 9 |- (ph -> (z Fv <-> E.y e. X (z = C /\ v = D)))
43	36, 42	anbi12d 442	. . . . . . . 8 |- (ph -> ((z Fu /\ z Fv) <-> (E.x e. X (z = A /\ u = B) /\ E.y e. X (z = C /\ v = D))))
44	43	biimpd 132	. . . . . . 7 |- (ph -> ((z Fu /\ z Fv) -> (E.x e. X (z = A /\ u = B) /\ E.y e. X (z = C /\ v = D))))
45		reeanv 2473	. . . . . . . 8 |- (E.x e. X E.y e. X ((z = A /\ u = B) /\ (z = C /\ v = D)) <-> (E.x e. X (z = A /\ u = B) /\ E.y e. X (z = C /\ v = D)))
46		r19.29 2444	. . . . . . . . . 10 |- ((A.x e. X A.y e. X (A = C -> B = D) /\ E.x e. X E.y e. X ((z = A /\ u = B) /\ (z = C /\ v = D))) -> E.x e. X (A.y e. X (A = C -> B = D) /\ E.y e. X ((z = A /\ u = B) /\ (z = C /\ v = D))))
47		r19.29 2444	. . . . . . . . . . . 12 |- ((A.y e. X (A = C -> B = D) /\ E.y e. X ((z = A /\ u = B) /\ (z = C /\ v = D))) -> E.y e. X ((A = C -> B = D) /\ ((z = A /\ u = B) /\ (z = C /\ v = D))))
48		eqtr2 2055	. . . . . . . . . . . . . . . . 17 |- ((z = A /\ z = C) -> A = C)
49	48	ad2ant2r 478	. . . . . . . . . . . . . . . 16 |- (((z = A /\ u = B) /\ (z = C /\ v = D)) -> A = C)
50	49	imim1i 54	. . . . . . . . . . . . . . 15 |- ((A = C -> B = D) -> (((z = A /\ u = B) /\ (z = C /\ v = D)) -> B = D))
51	50	imp 115	. . . . . . . . . . . . . 14 |- (((A = C -> B = D) /\ ((z = A /\ u = B) /\ (z = C /\ v = D))) -> B = D)
52		simprlr 490	. . . . . . . . . . . . . 14 |- (((A = C -> B = D) /\ ((z = A /\ u = B) /\ (z = C /\ v = D))) -> u = B)
53		simprrr 492	. . . . . . . . . . . . . 14 |- (((A = C -> B = D) /\ ((z = A /\ u = B) /\ (z = C /\ v = D))) -> v = D)
54	51, 52, 53	3eqtr4d 2079	. . . . . . . . . . . . 13 |- (((A = C -> B = D) /\ ((z = A /\ u = B) /\ (z = C /\ v = D))) -> u = v)
55	54	rexlimivw 2423	. . . . . . . . . . . 12 |- (E.y e. X ((A = C -> B = D) /\ ((z = A /\ u = B) /\ (z = C /\ v = D))) -> u = v)
56	47, 55	syl 14	. . . . . . . . . . 11 |- ((A.y e. X (A = C -> B = D) /\ E.y e. X ((z = A /\ u = B) /\ (z = C /\ v = D))) -> u = v)
57	56	rexlimivw 2423	. . . . . . . . . 10 |- (E.x e. X (A.y e. X (A = C -> B = D) /\ E.y e. X ((z = A /\ u = B) /\ (z = C /\ v = D))) -> u = v)
58	46, 57	syl 14	. . . . . . . . 9 |- ((A.x e. X A.y e. X (A = C -> B = D) /\ E.x e. X E.y e. X ((z = A /\ u = B) /\ (z = C /\ v = D))) -> u = v)
59	58	ex 108	. . . . . . . 8 |- (A.x e. X A.y e. X (A = C -> B = D) -> (E.x e. X E.y e. X ((z = A /\ u = B) /\ (z = C /\ v = D)) -> u = v))
60	45, 59	syl5bir 142	. . . . . . 7 |- (A.x e. X A.y e. X (A = C -> B = D) -> ((E.x e. X (z = A /\ u = B) /\ E.y e. X (z = C /\ v = D)) -> u = v))
61	44, 60	syl9 66	. . . . . 6 |- (ph -> (A.x e. X A.y e. X (A = C -> B = D) -> ((z Fu /\ z Fv) -> u = v)))
62	61	alrimdv 1753	. . . . 5 |- (ph -> (A.x e. X A.y e. X (A = C -> B = D) -> A.v((z Fu /\ z Fv) -> u = v)))
63	62	alrimdv 1753	. . . 4 |- (ph -> (A.x e. X A.y e. X (A = C -> B = D) -> A.uA.v((z Fu /\ z Fv) -> u = v)))
64	63	alrimdv 1753	. . 3 |- (ph -> (A.x e. X A.y e. X (A = C -> B = D) -> A.zA.uA.v((z Fu /\ z Fv) -> u = v)))
65	2, 9, 10	fliftrel 5375	. . . . 5 |- (ph -> F C_ ( R X. S))
66		relxp 4390	. . . . 5 |- Rel ( R X. S)
67		relss 4370	. . . . 5 |- ( F C_ ( R X. S) -> ( Rel ( R X. S) -> Rel F))
68	65, 66, 67	mpisyl 1332	. . . 4 |- (ph -> Rel F)
69		dffun2 4855	. . . . 5 |- ( Fun F <-> ( Rel F /\ A.zA.uA.v((z Fu /\ z Fv) -> u = v)))
70	69	baib 827	. . . 4 |- ( Rel F -> ( Fun F <-> A.zA.uA.v((z Fu /\ z Fv) -> u = v)))
71	68, 70	syl 14	. . 3 |- (ph -> ( Fun F <-> A.zA.uA.v((z Fu /\ z Fv) -> u = v)))
72	64, 71	sylibrd 158	. 2 |- (ph -> (A.x e. X A.y e. X (A = C -> B = D) -> Fun F))
73	35, 72	impbid 120	1 |- (ph -> ( Fun F <-> A.x e. X A.y e. X (A = C -> B = D)))

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98  A.wal 1240   = wceq 1242   e. wcel 1390  A.wral 2300  E.wrex 2301   C_ wss 2911   <.cop 3370   class class class wbr 3755   |-> cmpt 3809   X. cxp 4286   ran crn 4289   Rel wrel 4293   Fun wfun 4839   ` cfv 4845

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-fv 4853

This theorem is referenced by:  fliftfund  5380  fliftfuns  5381  qliftfun  6124