Theorem fnprb 7211

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 7167	. . . . 5 ⊢ (𝐹 Fn {𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩})
3		dfsn2 4600	. . . . . 6 ⊢ {𝐴} = {𝐴, 𝐴}
4	3	fneq2i 6634	. . . . 5 ⊢ (𝐹 Fn {𝐴} ↔ 𝐹 Fn {𝐴, 𝐴})
5		dfsn2 4600	. . . . . 6 ⊢ {⟨𝐴, (𝐹‘𝐴)⟩} = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩}
6	5	eqeq2i 2775	. . . . 5 ⊢ (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩})
7	2, 4, 6	3bitr3i 304	. . . 4 ⊢ (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩})
8	7	a1i 11	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩}))
9		preq2 4698	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵})
10	9	fneq2d 6630	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 Fn {𝐴, 𝐵}))
11		id 23	. . . . . 6 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
12		fveq2 6882	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
13	11, 12	opeq12d 4844	. . . . 5 ⊢ (𝐴 = 𝐵 → ⟨𝐴, (𝐹‘𝐴)⟩ = ⟨𝐵, (𝐹‘𝐵)⟩)
14	13	preq2d 4704	. . . 4 ⊢ (𝐴 = 𝐵 → {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩} = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})
15	14	eqeq2d 2773	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐴, (𝐹‘𝐴)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}))
16	8, 10, 15	3bitr3d 312	. 2 ⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}))
17		fndm 6639	. . . . . 6 ⊢ (𝐹 Fn {𝐴, 𝐵} → dom 𝐹 = {𝐴, 𝐵})
18		fvex 6895	. . . . . . 7 ⊢ (𝐹‘𝐴) ∈ V
19		fvex 6895	. . . . . . 7 ⊢ (𝐹‘𝐵) ∈ V
20	18, 19	dmprop 6217	. . . . . 6 ⊢ dom {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} = {𝐴, 𝐵}
21	17, 20	eqtr4di 2815	. . . . 5 ⊢ (𝐹 Fn {𝐴, 𝐵} → dom 𝐹 = dom {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})
22	21	adantl 487	. . . 4 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → dom 𝐹 = dom {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})
23	17	adantl 487	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → dom 𝐹 = {𝐴, 𝐵})
24	23	eleq2d 2848	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ {𝐴, 𝐵}))
25		vex 3457	. . . . . . . 8 ⊢ 𝑥 ∈ V
26	25	elpr 4612	. . . . . . 7 ⊢ (𝑥 ∈ {𝐴, 𝐵} ↔ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵))
27	1, 18	fvpr1 7194	. . . . . . . . . . 11 ⊢ (𝐴 ≠ 𝐵 → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴) = (𝐹‘𝐴))
28	27	adantr 486	. . . . . . . . . 10 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴) = (𝐹‘𝐴))
29	28	eqcomd 2768	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝐹‘𝐴) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴))
30		fveq2 6882	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴))
31		fveq2 6882	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴))
32	30, 31	eqeq12d 2778	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) ↔ (𝐹‘𝐴) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴)))
33	29, 32	syl5ibrcom 250	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 = 𝐴 → (𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥)))
34		fnprb.b	. . . . . . . . . . . 12 ⊢ 𝐵 ∈ V
35	34, 19	fvpr2 7195	. . . . . . . . . . 11 ⊢ (𝐴 ≠ 𝐵 → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵) = (𝐹‘𝐵))
36	35	adantr 486	. . . . . . . . . 10 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵) = (𝐹‘𝐵))
37	36	eqcomd 2768	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝐹‘𝐵) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵))
38		fveq2 6882	. . . . . . . . . 10 ⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵))
39		fveq2 6882	. . . . . . . . . 10 ⊢ (𝑥 = 𝐵 → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵))
40	38, 39	eqeq12d 2778	. . . . . . . . 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 3155	. . . 4 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥))
46		fnfun 6636	. . . . 5 ⊢ (𝐹 Fn {𝐴, 𝐵} → Fun 𝐹)
47	1, 34, 18, 19	funpr 6593	. . . . 5 ⊢ (𝐴 ≠ 𝐵 → Fun {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})
48		eqfunfv 7032	. . . . 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 6540	. . . . 5 ⊢ ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} Fn {𝐴, 𝐵} ↔ (Fun {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} ∧ dom {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} = {𝐴, 𝐵}))
52	47, 20, 51	sylanblrc 602	. . . 4 ⊢ (𝐴 ≠ 𝐵 → {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} Fn {𝐴, 𝐵})
53		fneq1 6627	. . . . 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 3040	1 ⊢ (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2145   ≠ wne 2957  ∀wral 3078  Vcvv 3453  {csn 4587  {cpr 4589  ⟨cop 4593  dom cdm 5659  Fun wfun 6531   Fn wfn 6532  ‘cfv 6537

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545

This theorem is used by:  fntpb  7212  fnpr2g  7213  wrd2pr2op  15018