Theorem fliftfun 6210

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

Hypotheses

Ref	Expression
flift.1
flift.2
flift.3
fliftfun.4
fliftfun.5

Assertion

Ref	Expression
fliftfun

Distinct variable groups:   ,   ,   ,   ,,   ,   ,   ,,   ,,   ,S,

Proof of Theorem fliftfun

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1707	. . 3
2		flift.1	. . . . 5
3		nfmpt1 4541	. . . . . 6
4	3	nfrn 5250	. . . . 5
5	2, 4	nfcxfr 2617	. . . 4
6	5	nffun 5615	. . 3
7		fveq2 5871	. . . . . . 7
8		simplr 755	. . . . . . . . 9
9		flift.2	. . . . . . . . . . 11
10		flift.3	. . . . . . . . . . 11
11	2, 9, 10	fliftel1 6208	. . . . . . . . . 10
12	11	ad2ant2r 746	. . . . . . . . 9
13		funbrfv 5911	. . . . . . . . 9
14	8, 12, 13	sylc 60	. . . . . . . 8
15		simprr 757	. . . . . . . . . . 11
16		eqidd 2458	. . . . . . . . . . 11
17		eqidd 2458	. . . . . . . . . . 11
18		fliftfun.4	. . . . . . . . . . . . . 14
19	18	eqeq2d 2471	. . . . . . . . . . . . 13
20		fliftfun.5	. . . . . . . . . . . . . 14
21	20	eqeq2d 2471	. . . . . . . . . . . . 13
22	19, 21	anbi12d 710	. . . . . . . . . . . 12
23	22	rspcev 3210	. . . . . . . . . . 11
24	15, 16, 17, 23	syl12anc 1226	. . . . . . . . . 10
25	2, 9, 10	fliftel 6207	. . . . . . . . . . 11
26	25	ad2antrr 725	. . . . . . . . . 10
27	24, 26	mpbird 232	. . . . . . . . 9
28		funbrfv 5911	. . . . . . . . 9
29	8, 27, 28	sylc 60	. . . . . . . 8
30	14, 29	eqeq12d 2479	. . . . . . 7
31	7, 30	syl5ib 219	. . . . . 6
32	31	anassrs 648	. . . . 5
33	32	ralrimiva 2871	. . . 4
34	33	exp31 604	. . 3
35	1, 6, 34	ralrimd 2861	. 2
36	2, 9, 10	fliftel 6207	. . . . . . . . 9
37	2, 9, 10	fliftel 6207	. . . . . . . . . 10
38	18	eqeq2d 2471	. . . . . . . . . . . 12
39	20	eqeq2d 2471	. . . . . . . . . . . 12
40	38, 39	anbi12d 710	. . . . . . . . . . 11
41	40	cbvrexv 3085	. . . . . . . . . 10
42	37, 41	syl6bb 261	. . . . . . . . 9
43	36, 42	anbi12d 710	. . . . . . . 8
44	43	biimpd 207	. . . . . . 7
45		reeanv 3025	. . . . . . . 8
46		r19.29 2992	. . . . . . . . . 10
47		r19.29 2992	. . . . . . . . . . . 12
48		eqtr2 2484	. . . . . . . . . . . . . . . . 17
49	48	ad2ant2r 746	. . . . . . . . . . . . . . . 16
50	49	imim1i 58	. . . . . . . . . . . . . . 15
51	50	imp 429	. . . . . . . . . . . . . 14
52		simprlr 764	. . . . . . . . . . . . . 14
53		simprrr 766	. . . . . . . . . . . . . 14
54	51, 52, 53	3eqtr4d 2508	. . . . . . . . . . . . 13
55	54	rexlimivw 2946	. . . . . . . . . . . 12
56	47, 55	syl 16	. . . . . . . . . . 11
57	56	rexlimivw 2946	. . . . . . . . . 10
58	46, 57	syl 16	. . . . . . . . 9
59	58	ex 434	. . . . . . . 8
60	45, 59	syl5bir 218	. . . . . . 7
61	44, 60	syl9 71	. . . . . 6
62	61	alrimdv 1721	. . . . 5
63	62	alrimdv 1721	. . . 4
64	63	alrimdv 1721	. . 3
65	2, 9, 10	fliftrel 6206	. . . . 5
66		relxp 5115	. . . . 5
67		relss 5095	. . . . 5
68	65, 66, 67	mpisyl 18	. . . 4
69		dffun2 5603	. . . . 5
70	69	baib 903	. . . 4
71	68, 70	syl 16	. . 3
72	64, 71	sylibrd 234	. 2
73	35, 72	impbid 191	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  =wceq 1395  e.wcel 1818  A.wral 2807  E.wrex 2808  C_wss 3475  <.cop 4035   class class class wbr 4452  e.cmpt 4510  X.cxp 5002  rancrn 5005  Relwrel 5009  Funwfun 5587  `cfv 5593

This theorem is referenced by:  fliftfund  6211  fliftfuns  6212  qliftfun  7415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-fv 5601