Theorem fnprb 6129

Description: A function whose domain has at most two elements can be represented as a set of at most two ordered pairs. (Contributed by FL, 26-Jun-2011.) (Proof shortened by Scott Fenton, 12-Oct-2017.) Revised to eliminate unnecessary antecedent . (Revised by NM, 29-Dec-2018.)

Hypotheses

Ref	Expression
fnprb.1
fnprb.2

Assertion

Ref	Expression
fnprb

Proof of Theorem fnprb

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fnprb.1	. . . . . 6
2	1	fnsnb 6090	. . . . 5
3		dfsn2 4042	. . . . . 6
4	3	fneq2i 5681	. . . . 5
5		dfsn2 4042	. . . . . 6
6	5	eqeq2i 2475	. . . . 5
7	2, 4, 6	3bitr3i 275	. . . 4
8	7	a1i 11	. . 3
9		preq2 4110	. . . 4
10	9	fneq2d 5677	. . 3
11		id 22	. . . . . 6
12		fveq2 5871	. . . . . 6
13	11, 12	opeq12d 4225	. . . . 5
14	13	preq2d 4116	. . . 4
15	14	eqeq2d 2471	. . 3
16	8, 10, 15	3bitr3d 283	. 2
17		fndm 5685	. . . . . 6
18		fvex 5881	. . . . . . 7
19		fvex 5881	. . . . . . 7
20	18, 19	dmprop 5488	. . . . . 6
21	17, 20	syl6eqr 2516	. . . . 5
22	21	adantl 466	. . . 4
23	17	adantl 466	. . . . . . 7
24	23	eleq2d 2527	. . . . . 6
25		vex 3112	. . . . . . . 8
26	25	elpr 4047	. . . . . . 7
27	1, 18	fvpr1 6114	. . . . . . . . . . 11
28	27	adantr 465	. . . . . . . . . 10
29	28	eqcomd 2465	. . . . . . . . 9
30		fveq2 5871	. . . . . . . . . 10
31		fveq2 5871	. . . . . . . . . 10
32	30, 31	eqeq12d 2479	. . . . . . . . 9
33	29, 32	syl5ibrcom 222	. . . . . . . 8
34		fnprb.2	. . . . . . . . . . . 12
35	34, 19	fvpr2 6115	. . . . . . . . . . 11
36	35	adantr 465	. . . . . . . . . 10
37	36	eqcomd 2465	. . . . . . . . 9
38		fveq2 5871	. . . . . . . . . 10
39		fveq2 5871	. . . . . . . . . 10
40	38, 39	eqeq12d 2479	. . . . . . . . 9
41	37, 40	syl5ibrcom 222	. . . . . . . 8
42	33, 41	jaod 380	. . . . . . 7
43	26, 42	syl5bi 217	. . . . . 6
44	24, 43	sylbid 215	. . . . 5
45	44	ralrimiv 2869	. . . 4
46		fnfun 5683	. . . . 5
47	1, 34, 18, 19	funpr 5644	. . . . 5
48		eqfunfv 5986	. . . . 5
49	46, 47, 48	syl2anr 478	. . . 4
50	22, 45, 49	mpbir2and 922	. . 3
51	20	a1i 11	. . . . 5
52		df-fn 5596	. . . . 5
53	47, 51, 52	sylanbrc 664	. . . 4
54		fneq1 5674	. . . . 5
55	54	biimprd 223	. . . 4
56	53, 55	mpan9 469	. . 3
57	50, 56	impbida 832	. 2
58	16, 57	pm2.61ine 2770	1

Syntax hints:  <->wb 184  \/wo 368  /\wa 369  =wceq 1395  e.wcel 1818  =/=wne 2652  A.wral 2807  cvv 3109  {csn 4029  {cpr 4031  <.cop 4035  domcdm 5004  Funwfun 5587  Fnwfn 5588  `cfv 5593

This theorem is referenced by:  wrd2pr2op  12885

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-8 1820  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-pow 4630  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-reu 2814  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-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601