Theorem fnprb 7240

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.) Eliminate unnecessary antecedent 𝐴 ≠ 𝐵. (Revised by NM, 29-Dec-2018.)

Hypotheses

Ref	Expression
fnprb.a	⊢ 𝐴 ∈ V
fnprb.b	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
fnprb	⊢ (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})

Proof of Theorem fnprb

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fnprb.a	. . . . . 6 ⊢ 𝐴 ∈ V
2	1	fnsnb 7197	. . . . 5 ⊢ (𝐹 Fn {𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩})
3		dfsn2 4597	. . . . . 6 ⊢ {𝐴} = {𝐴, 𝐴}
4	3	fneq2i 6662	. . . . 5 ⊢ (𝐹 Fn {𝐴} ↔ 𝐹 Fn {𝐴, 𝐴})
5		dfsn2 4597	. . . . . 6 ⊢ {⟨𝐴, (𝐹‘𝐴)⟩} = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩}
6	5	eqeq2i 2776	. . . . 5 ⊢ (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩})
7	2, 4, 6	3bitr3i 304	. . . 4 ⊢ (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩})
8	7	a1i 11	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩}))
9		preq2 4695	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵})
10	9	fneq2d 6658	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 Fn {𝐴, 𝐵}))
11		id 23	. . . . . 6 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
12		fveq2 6911	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
13	11, 12	opeq12d 4851	. . . . 5 ⊢ (𝐴 = 𝐵 → ⟨𝐴, (𝐹‘𝐴)⟩ = ⟨𝐵, (𝐹‘𝐵)⟩)
14	13	preq2d 4701	. . . 4 ⊢ (𝐴 = 𝐵 → {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩} = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})
15	14	eqeq2d 2774	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}))
16	8, 10, 15	3bitr3d 312	. 2 ⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}))
17		fndm 6667	. . . . . 6 ⊢ (𝐹 Fn {𝐴, 𝐵} → dom 𝐹 = {𝐴, 𝐵})
18		fvex 6924	. . . . . . 7 ⊢ (𝐹‘𝐴) ∈ V
19		fvex 6924	. . . . . . 7 ⊢ (𝐹‘𝐵) ∈ V
20	18, 19	dmprop 6232	. . . . . 6 ⊢ dom {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} = {𝐴, 𝐵}
21	17, 20	eqtr4di 2816	. . . . 5 ⊢ (𝐹 Fn {𝐴, 𝐵} → dom 𝐹 = dom {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})
22	21	adantl 487	. . . 4 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → dom 𝐹 = dom {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})
23	17	adantl 487	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → dom 𝐹 = {𝐴, 𝐵})
24	23	eleq2d 2850	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ {𝐴, 𝐵}))
25		vex 3458	. . . . . . . 8 ⊢ 𝑥 ∈ V
26	25	elpr 4609	. . . . . . 7 ⊢ (𝑥 ∈ {𝐴, 𝐵} ↔ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵))
27	1, 18	fvpr1 7223	. . . . . . . . . . 11 ⊢ (𝐴 ≠ 𝐵 → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴) = (𝐹‘𝐴))
28	27	adantr 486	. . . . . . . . . 10 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴) = (𝐹‘𝐴))
29	28	eqcomd 2769	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝐹‘𝐴) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴))
30		fveq2 6911	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴))
31		fveq2 6911	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴))
32	30, 31	eqeq12d 2779	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) ↔ (𝐹‘𝐴) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴)))
33	29, 32	syl5ibrcom 250	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 = 𝐴 → (𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥)))
34		fnprb.b	. . . . . . . . . . . 12 ⊢ 𝐵 ∈ V
35	34, 19	fvpr2 7224	. . . . . . . . . . 11 ⊢ (𝐴 ≠ 𝐵 → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵) = (𝐹‘𝐵))
36	35	adantr 486	. . . . . . . . . 10 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵) = (𝐹‘𝐵))
37	36	eqcomd 2769	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝐹‘𝐵) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵))
38		fveq2 6911	. . . . . . . . . 10 ⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵))
39		fveq2 6911	. . . . . . . . . 10 ⊢ (𝑥 = 𝐵 → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵))
40	38, 39	eqeq12d 2779	. . . . . . . . 9 ⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) ↔ (𝐹‘𝐵) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵)))
41	37, 40	syl5ibrcom 250	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 = 𝐵 → (𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥)))
42	33, 41	jaod 873	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → (𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥)))
43	26, 42	biimtrid 245	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 ∈ {𝐴, 𝐵} → (𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥)))
44	24, 43	sylbid 243	. . . . 5 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 ∈ dom 𝐹 → (𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥)))
45	44	ralrimiv 3157	. . . 4 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥))
46		fnfun 6664	. . . . 5 ⊢ (𝐹 Fn {𝐴, 𝐵} → Fun 𝐹)
47	1, 34, 18, 19	funpr 6621	. . . . 5 ⊢ (𝐴 ≠ 𝐵 → Fun {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})
48		eqfunfv 7061	. . . . 5 ⊢ ((Fun 𝐹 ∧ Fun {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}) → (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} ↔ (dom 𝐹 = dom {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} ∧ ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥))))
49	46, 47, 48	syl2anr 609	. . . 4 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} ↔ (dom 𝐹 = dom {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} ∧ ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥))))
50	22, 45, 49	mpbir2and 726	. . 3 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})
51		df-fn 6564	. . . . 5 ⊢ ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} Fn {𝐴, 𝐵} ↔ (Fun {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} ∧ dom {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} = {𝐴, 𝐵}))
52	47, 20, 51	sylanblrc 602	. . . 4 ⊢ (𝐴 ≠ 𝐵 → {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} Fn {𝐴, 𝐵})
53		fneq1 6655	. . . . 5 ⊢ (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} → (𝐹 Fn {𝐴, 𝐵} ↔ {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} Fn {𝐴, 𝐵}))
54	53	biimprd 251	. . . 4 ⊢ (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} Fn {𝐴, 𝐵} → 𝐹 Fn {𝐴, 𝐵}))
55	52, 54	mpan9 516	. . 3 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}) → 𝐹 Fn {𝐴, 𝐵})
56	50, 55	impbida 813	. 2 ⊢ (𝐴 ≠ 𝐵 → (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}))
57	16, 56	pm2.61ine 3042	1 ⊢ (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  Vcvv 3454  {csn 4588  {cpr 4590  ⟨cop 4838  dom cdm 5656  Fun wfun 6555   Fn wfn 6556  ‘cfv 6561

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pr 5396

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569

This theorem is used by:  fntpb  7241  fnpr2g  7242  wrd2pr2op  15126