Theorem fnprb 7229

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 7186	. . . . 5 ⊢ (𝐹 Fn {𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩})
3		dfsn2 4638	. . . . . 6 ⊢ {𝐴} = {𝐴, 𝐴}
4	3	fneq2i 6665	. . . . 5 ⊢ (𝐹 Fn {𝐴} ↔ 𝐹 Fn {𝐴, 𝐴})
5		dfsn2 4638	. . . . . 6 ⊢ {⟨𝐴, (𝐹‘𝐴)⟩} = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩}
6	5	eqeq2i 2749	. . . . 5 ⊢ (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩})
7	2, 4, 6	3bitr3i 301	. . . 4 ⊢ (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩})
8	7	a1i 11	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩}))
9		preq2 4733	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵})
10	9	fneq2d 6661	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 Fn {𝐴, 𝐵}))
11		id 22	. . . . . 6 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
12		fveq2 6905	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
13	11, 12	opeq12d 4880	. . . . 5 ⊢ (𝐴 = 𝐵 → ⟨𝐴, (𝐹‘𝐴)⟩ = ⟨𝐵, (𝐹‘𝐵)⟩)
14	13	preq2d 4739	. . . 4 ⊢ (𝐴 = 𝐵 → {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩} = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})
15	14	eqeq2d 2747	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}))
16	8, 10, 15	3bitr3d 309	. 2 ⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}))
17		fndm 6670	. . . . . 6 ⊢ (𝐹 Fn {𝐴, 𝐵} → dom 𝐹 = {𝐴, 𝐵})
18		fvex 6918	. . . . . . 7 ⊢ (𝐹‘𝐴) ∈ V
19		fvex 6918	. . . . . . 7 ⊢ (𝐹‘𝐵) ∈ V
20	18, 19	dmprop 6236	. . . . . 6 ⊢ dom {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} = {𝐴, 𝐵}
21	17, 20	eqtr4di 2794	. . . . 5 ⊢ (𝐹 Fn {𝐴, 𝐵} → dom 𝐹 = dom {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})
22	21	adantl 481	. . . 4 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → dom 𝐹 = dom {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})
23	17	adantl 481	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → dom 𝐹 = {𝐴, 𝐵})
24	23	eleq2d 2826	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ {𝐴, 𝐵}))
25		vex 3483	. . . . . . . 8 ⊢ 𝑥 ∈ V
26	25	elpr 4649	. . . . . . 7 ⊢ (𝑥 ∈ {𝐴, 𝐵} ↔ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵))
27	1, 18	fvpr1 7213	. . . . . . . . . . 11 ⊢ (𝐴 ≠ 𝐵 → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴) = (𝐹‘𝐴))
28	27	adantr 480	. . . . . . . . . 10 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴) = (𝐹‘𝐴))
29	28	eqcomd 2742	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝐹‘𝐴) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴))
30		fveq2 6905	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴))
31		fveq2 6905	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴))
32	30, 31	eqeq12d 2752	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) ↔ (𝐹‘𝐴) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴)))
33	29, 32	syl5ibrcom 247	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 = 𝐴 → (𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥)))
34		fnprb.b	. . . . . . . . . . . 12 ⊢ 𝐵 ∈ V
35	34, 19	fvpr2 7214	. . . . . . . . . . 11 ⊢ (𝐴 ≠ 𝐵 → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵) = (𝐹‘𝐵))
36	35	adantr 480	. . . . . . . . . 10 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵) = (𝐹‘𝐵))
37	36	eqcomd 2742	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝐹‘𝐵) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵))
38		fveq2 6905	. . . . . . . . . 10 ⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵))
39		fveq2 6905	. . . . . . . . . 10 ⊢ (𝑥 = 𝐵 → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵))
40	38, 39	eqeq12d 2752	. . . . . . . . 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 3144	. . . 4 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥))
46		fnfun 6667	. . . . 5 ⊢ (𝐹 Fn {𝐴, 𝐵} → Fun 𝐹)
47	1, 34, 18, 19	funpr 6621	. . . . 5 ⊢ (𝐴 ≠ 𝐵 → Fun {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})
48		eqfunfv 7055	. . . . 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 6563	. . . . 5 ⊢ ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} Fn {𝐴, 𝐵} ↔ (Fun {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} ∧ dom {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} = {𝐴, 𝐵}))
52	47, 20, 51	sylanblrc 590	. . . 4 ⊢ (𝐴 ≠ 𝐵 → {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} Fn {𝐴, 𝐵})
53		fneq1 6658	. . . . 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 3024	1 ⊢ (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})

Syntax hints:   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1539   ∈ wcel 2107   ≠ wne 2939  ∀wral 3060  Vcvv 3479  {csn 4625  {cpr 4627  ⟨cop 4631  dom cdm 5684  Fun wfun 6554   Fn wfn 6555  ‘cfv 6560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568

This theorem is referenced by:  fntpb  7230  fnpr2g  7231  wrd2pr2op  14983