Theorem fnprb 7182

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 7139	. . . . 5 ⊢ (𝐹 Fn {𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩})
3		dfsn2 4602	. . . . . 6 ⊢ {𝐴} = {𝐴, 𝐴}
4	3	fneq2i 6616	. . . . 5 ⊢ (𝐹 Fn {𝐴} ↔ 𝐹 Fn {𝐴, 𝐴})
5		dfsn2 4602	. . . . . 6 ⊢ {⟨𝐴, (𝐹‘𝐴)⟩} = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩}
6	5	eqeq2i 2742	. . . . 5 ⊢ (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩})
7	2, 4, 6	3bitr3i 301	. . . 4 ⊢ (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩})
8	7	a1i 11	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩}))
9		preq2 4698	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵})
10	9	fneq2d 6612	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 Fn {𝐴, 𝐵}))
11		id 22	. . . . . 6 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
12		fveq2 6858	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
13	11, 12	opeq12d 4845	. . . . 5 ⊢ (𝐴 = 𝐵 → ⟨𝐴, (𝐹‘𝐴)⟩ = ⟨𝐵, (𝐹‘𝐵)⟩)
14	13	preq2d 4704	. . . 4 ⊢ (𝐴 = 𝐵 → {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩} = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})
15	14	eqeq2d 2740	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}))
16	8, 10, 15	3bitr3d 309	. 2 ⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}))
17		fndm 6621	. . . . . 6 ⊢ (𝐹 Fn {𝐴, 𝐵} → dom 𝐹 = {𝐴, 𝐵})
18		fvex 6871	. . . . . . 7 ⊢ (𝐹‘𝐴) ∈ V
19		fvex 6871	. . . . . . 7 ⊢ (𝐹‘𝐵) ∈ V
20	18, 19	dmprop 6190	. . . . . 6 ⊢ dom {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} = {𝐴, 𝐵}
21	17, 20	eqtr4di 2782	. . . . 5 ⊢ (𝐹 Fn {𝐴, 𝐵} → dom 𝐹 = dom {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})
22	21	adantl 481	. . . 4 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → dom 𝐹 = dom {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})
23	17	adantl 481	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → dom 𝐹 = {𝐴, 𝐵})
24	23	eleq2d 2814	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ {𝐴, 𝐵}))
25		vex 3451	. . . . . . . 8 ⊢ 𝑥 ∈ V
26	25	elpr 4614	. . . . . . 7 ⊢ (𝑥 ∈ {𝐴, 𝐵} ↔ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵))
27	1, 18	fvpr1 7166	. . . . . . . . . . 11 ⊢ (𝐴 ≠ 𝐵 → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴) = (𝐹‘𝐴))
28	27	adantr 480	. . . . . . . . . 10 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴) = (𝐹‘𝐴))
29	28	eqcomd 2735	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝐹‘𝐴) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴))
30		fveq2 6858	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴))
31		fveq2 6858	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴))
32	30, 31	eqeq12d 2745	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) ↔ (𝐹‘𝐴) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴)))
33	29, 32	syl5ibrcom 247	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 = 𝐴 → (𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥)))
34		fnprb.b	. . . . . . . . . . . 12 ⊢ 𝐵 ∈ V
35	34, 19	fvpr2 7167	. . . . . . . . . . 11 ⊢ (𝐴 ≠ 𝐵 → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵) = (𝐹‘𝐵))
36	35	adantr 480	. . . . . . . . . 10 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵) = (𝐹‘𝐵))
37	36	eqcomd 2735	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝐹‘𝐵) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵))
38		fveq2 6858	. . . . . . . . . 10 ⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵))
39		fveq2 6858	. . . . . . . . . 10 ⊢ (𝑥 = 𝐵 → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵))
40	38, 39	eqeq12d 2745	. . . . . . . . 9 ⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) ↔ (𝐹‘𝐵) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵)))
41	37, 40	syl5ibrcom 247	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 = 𝐵 → (𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥)))
42	33, 41	jaod 859	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → (𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥)))
43	26, 42	biimtrid 242	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 ∈ {𝐴, 𝐵} → (𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥)))
44	24, 43	sylbid 240	. . . . 5 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 ∈ dom 𝐹 → (𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥)))
45	44	ralrimiv 3124	. . . 4 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥))
46		fnfun 6618	. . . . 5 ⊢ (𝐹 Fn {𝐴, 𝐵} → Fun 𝐹)
47	1, 34, 18, 19	funpr 6572	. . . . 5 ⊢ (𝐴 ≠ 𝐵 → Fun {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})
48		eqfunfv 7008	. . . . 5 ⊢ ((Fun 𝐹 ∧ Fun {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}) → (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} ↔ (dom 𝐹 = dom {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} ∧ ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥))))
49	46, 47, 48	syl2anr 597	. . . 4 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} ↔ (dom 𝐹 = dom {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} ∧ ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥))))
50	22, 45, 49	mpbir2and 713	. . 3 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})
51		df-fn 6514	. . . . 5 ⊢ ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} Fn {𝐴, 𝐵} ↔ (Fun {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} ∧ dom {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} = {𝐴, 𝐵}))
52	47, 20, 51	sylanblrc 590	. . . 4 ⊢ (𝐴 ≠ 𝐵 → {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} Fn {𝐴, 𝐵})
53		fneq1 6609	. . . . 5 ⊢ (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} → (𝐹 Fn {𝐴, 𝐵} ↔ {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} Fn {𝐴, 𝐵}))
54	53	biimprd 248	. . . 4 ⊢ (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} Fn {𝐴, 𝐵} → 𝐹 Fn {𝐴, 𝐵}))
55	52, 54	mpan9 506	. . 3 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}) → 𝐹 Fn {𝐴, 𝐵})
56	50, 55	impbida 800	. 2 ⊢ (𝐴 ≠ 𝐵 → (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}))
57	16, 56	pm2.61ine 3008	1 ⊢ (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})

Syntax hints:   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  Vcvv 3447  {csn 4589  {cpr 4591  ⟨cop 4595  dom cdm 5638  Fun wfun 6505   Fn wfn 6506  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519

This theorem is referenced by:  fntpb  7183  fnpr2g  7184  wrd2pr2op  14909