Theorem funopg

Description: A Kuratowski ordered pair of sets is a function only if its components are equal. (Contributed by NM, 5-Jun-2008) (Revised by Mario Carneiro, 26-Apr-2015) A function is a class of ordered pairs, so the fact that an ordered pair may sometimes be itself a function is an "accident" depending on the specific encoding of ordered pairs as classes (in set.mm, the Kuratowski encoding). A more meaningful statement is funsng , as relsnopg is to relop . (New usage is discouraged.)

	Ref	Expression
Assertion	funopg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ Fun ⟨ 𝐴 , 𝐵 ⟩ ) → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		opeq1	⊢ ( 𝑢 = 𝐴 → ⟨ 𝑢 , 𝑡 ⟩ = ⟨ 𝐴 , 𝑡 ⟩ )
2	1	funeqd	⊢ ( 𝑢 = 𝐴 → ( Fun ⟨ 𝑢 , 𝑡 ⟩ ↔ Fun ⟨ 𝐴 , 𝑡 ⟩ ) )
3		eqeq1	⊢ ( 𝑢 = 𝐴 → ( 𝑢 = 𝑡 ↔ 𝐴 = 𝑡 ) )
4	2 3	imbi12d	⊢ ( 𝑢 = 𝐴 → ( ( Fun ⟨ 𝑢 , 𝑡 ⟩ → 𝑢 = 𝑡 ) ↔ ( Fun ⟨ 𝐴 , 𝑡 ⟩ → 𝐴 = 𝑡 ) ) )
5		opeq2	⊢ ( 𝑡 = 𝐵 → ⟨ 𝐴 , 𝑡 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
6	5	funeqd	⊢ ( 𝑡 = 𝐵 → ( Fun ⟨ 𝐴 , 𝑡 ⟩ ↔ Fun ⟨ 𝐴 , 𝐵 ⟩ ) )
7		eqeq2	⊢ ( 𝑡 = 𝐵 → ( 𝐴 = 𝑡 ↔ 𝐴 = 𝐵 ) )
8	6 7	imbi12d	⊢ ( 𝑡 = 𝐵 → ( ( Fun ⟨ 𝐴 , 𝑡 ⟩ → 𝐴 = 𝑡 ) ↔ ( Fun ⟨ 𝐴 , 𝐵 ⟩ → 𝐴 = 𝐵 ) ) )
9		funrel	⊢ ( Fun ⟨ 𝑢 , 𝑡 ⟩ → Rel ⟨ 𝑢 , 𝑡 ⟩ )
10		vex	⊢ 𝑢 ∈ V
11		vex	⊢ 𝑡 ∈ V
12	10 11	relop	⊢ ( Rel ⟨ 𝑢 , 𝑡 ⟩ ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑢 = { 𝑥 } ∧ 𝑡 = { 𝑥 , 𝑦 } ) )
13	9 12	sylib	⊢ ( Fun ⟨ 𝑢 , 𝑡 ⟩ → ∃ 𝑥 ∃ 𝑦 ( 𝑢 = { 𝑥 } ∧ 𝑡 = { 𝑥 , 𝑦 } ) )
14	10 11	opth	⊢ ( ⟨ 𝑢 , 𝑡 ⟩ = ⟨ { 𝑥 } , { 𝑥 , 𝑦 } ⟩ ↔ ( 𝑢 = { 𝑥 } ∧ 𝑡 = { 𝑥 , 𝑦 } ) )
15		vex	⊢ 𝑥 ∈ V
16	15	opid	⊢ ⟨ 𝑥 , 𝑥 ⟩ = { { 𝑥 } }
17	16	preq1i	⊢ { ⟨ 𝑥 , 𝑥 ⟩ , { { 𝑥 } , { 𝑥 , 𝑦 } } } = { { { 𝑥 } } , { { 𝑥 } , { 𝑥 , 𝑦 } } }
18		vex	⊢ 𝑦 ∈ V
19	15 18	dfop	⊢ ⟨ 𝑥 , 𝑦 ⟩ = { { 𝑥 } , { 𝑥 , 𝑦 } }
20	19	preq2i	⊢ { ⟨ 𝑥 , 𝑥 ⟩ , ⟨ 𝑥 , 𝑦 ⟩ } = { ⟨ 𝑥 , 𝑥 ⟩ , { { 𝑥 } , { 𝑥 , 𝑦 } } }
21		vsnex	⊢ { 𝑥 } ∈ V
22		zfpair2	⊢ { 𝑥 , 𝑦 } ∈ V
23	21 22	dfop	⊢ ⟨ { 𝑥 } , { 𝑥 , 𝑦 } ⟩ = { { { 𝑥 } } , { { 𝑥 } , { 𝑥 , 𝑦 } } }
24	17 20 23	3eqtr4ri	⊢ ⟨ { 𝑥 } , { 𝑥 , 𝑦 } ⟩ = { ⟨ 𝑥 , 𝑥 ⟩ , ⟨ 𝑥 , 𝑦 ⟩ }
25	24	eqeq2i	⊢ ( ⟨ 𝑢 , 𝑡 ⟩ = ⟨ { 𝑥 } , { 𝑥 , 𝑦 } ⟩ ↔ ⟨ 𝑢 , 𝑡 ⟩ = { ⟨ 𝑥 , 𝑥 ⟩ , ⟨ 𝑥 , 𝑦 ⟩ } )
26	14 25	bitr3i	⊢ ( ( 𝑢 = { 𝑥 } ∧ 𝑡 = { 𝑥 , 𝑦 } ) ↔ ⟨ 𝑢 , 𝑡 ⟩ = { ⟨ 𝑥 , 𝑥 ⟩ , ⟨ 𝑥 , 𝑦 ⟩ } )
27		dffun4	⊢ ( Fun ⟨ 𝑢 , 𝑡 ⟩ ↔ ( Rel ⟨ 𝑢 , 𝑡 ⟩ ∧ ∀ 𝑧 ∀ 𝑤 ∀ 𝑣 ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ∧ ⟨ 𝑧 , 𝑣 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ) → 𝑤 = 𝑣 ) ) )
28	27	simprbi	⊢ ( Fun ⟨ 𝑢 , 𝑡 ⟩ → ∀ 𝑧 ∀ 𝑤 ∀ 𝑣 ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ∧ ⟨ 𝑧 , 𝑣 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ) → 𝑤 = 𝑣 ) )
29		opex	⊢ ⟨ 𝑥 , 𝑥 ⟩ ∈ V
30	29	prid1	⊢ ⟨ 𝑥 , 𝑥 ⟩ ∈ { ⟨ 𝑥 , 𝑥 ⟩ , ⟨ 𝑥 , 𝑦 ⟩ }
31		eleq2	⊢ ( ⟨ 𝑢 , 𝑡 ⟩ = { ⟨ 𝑥 , 𝑥 ⟩ , ⟨ 𝑥 , 𝑦 ⟩ } → ( ⟨ 𝑥 , 𝑥 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ↔ ⟨ 𝑥 , 𝑥 ⟩ ∈ { ⟨ 𝑥 , 𝑥 ⟩ , ⟨ 𝑥 , 𝑦 ⟩ } ) )
32	30 31	mpbiri	⊢ ( ⟨ 𝑢 , 𝑡 ⟩ = { ⟨ 𝑥 , 𝑥 ⟩ , ⟨ 𝑥 , 𝑦 ⟩ } → ⟨ 𝑥 , 𝑥 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ )
33		opex	⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
34	33	prid2	⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑥 ⟩ , ⟨ 𝑥 , 𝑦 ⟩ }
35		eleq2	⊢ ( ⟨ 𝑢 , 𝑡 ⟩ = { ⟨ 𝑥 , 𝑥 ⟩ , ⟨ 𝑥 , 𝑦 ⟩ } → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑥 ⟩ , ⟨ 𝑥 , 𝑦 ⟩ } ) )
36	34 35	mpbiri	⊢ ( ⟨ 𝑢 , 𝑡 ⟩ = { ⟨ 𝑥 , 𝑥 ⟩ , ⟨ 𝑥 , 𝑦 ⟩ } → ⟨ 𝑥 , 𝑦 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ )
37	32 36	jca	⊢ ( ⟨ 𝑢 , 𝑡 ⟩ = { ⟨ 𝑥 , 𝑥 ⟩ , ⟨ 𝑥 , 𝑦 ⟩ } → ( ⟨ 𝑥 , 𝑥 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ) )
38		opeq12	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ) → ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑥 ⟩ )
39	38	3adant3	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦 ) → ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑥 ⟩ )
40	39	eleq1d	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦 ) → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ↔ ⟨ 𝑥 , 𝑥 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ) )
41		opeq12	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑣 = 𝑦 ) → ⟨ 𝑧 , 𝑣 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
42	41	3adant2	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦 ) → ⟨ 𝑧 , 𝑣 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
43	42	eleq1d	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦 ) → ( ⟨ 𝑧 , 𝑣 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ) )
44	40 43	anbi12d	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦 ) → ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ∧ ⟨ 𝑧 , 𝑣 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ) ↔ ( ⟨ 𝑥 , 𝑥 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ) ) )
45		eqeq12	⊢ ( ( 𝑤 = 𝑥 ∧ 𝑣 = 𝑦 ) → ( 𝑤 = 𝑣 ↔ 𝑥 = 𝑦 ) )
46	45	3adant1	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦 ) → ( 𝑤 = 𝑣 ↔ 𝑥 = 𝑦 ) )
47	44 46	imbi12d	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦 ) → ( ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ∧ ⟨ 𝑧 , 𝑣 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ) → 𝑤 = 𝑣 ) ↔ ( ( ⟨ 𝑥 , 𝑥 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ) → 𝑥 = 𝑦 ) ) )
48	47	spc3gv	⊢ ( ( 𝑥 ∈ V ∧ 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( ∀ 𝑧 ∀ 𝑤 ∀ 𝑣 ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ∧ ⟨ 𝑧 , 𝑣 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ) → 𝑤 = 𝑣 ) → ( ( ⟨ 𝑥 , 𝑥 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ) → 𝑥 = 𝑦 ) ) )
49	15 15 18 48	mp3an	⊢ ( ∀ 𝑧 ∀ 𝑤 ∀ 𝑣 ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ∧ ⟨ 𝑧 , 𝑣 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ) → 𝑤 = 𝑣 ) → ( ( ⟨ 𝑥 , 𝑥 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ⟨ 𝑢 , 𝑡 ⟩ ) → 𝑥 = 𝑦 ) )
50	28 37 49	syl2im	⊢ ( Fun ⟨ 𝑢 , 𝑡 ⟩ → ( ⟨ 𝑢 , 𝑡 ⟩ = { ⟨ 𝑥 , 𝑥 ⟩ , ⟨ 𝑥 , 𝑦 ⟩ } → 𝑥 = 𝑦 ) )
51	26 50	biimtrid	⊢ ( Fun ⟨ 𝑢 , 𝑡 ⟩ → ( ( 𝑢 = { 𝑥 } ∧ 𝑡 = { 𝑥 , 𝑦 } ) → 𝑥 = 𝑦 ) )
52		dfsn2	⊢ { 𝑥 } = { 𝑥 , 𝑥 }
53		preq2	⊢ ( 𝑥 = 𝑦 → { 𝑥 , 𝑥 } = { 𝑥 , 𝑦 } )
54	52 53	eqtr2id	⊢ ( 𝑥 = 𝑦 → { 𝑥 , 𝑦 } = { 𝑥 } )
55	54	eqeq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑡 = { 𝑥 , 𝑦 } ↔ 𝑡 = { 𝑥 } ) )
56		eqtr3	⊢ ( ( 𝑢 = { 𝑥 } ∧ 𝑡 = { 𝑥 } ) → 𝑢 = 𝑡 )
57	56	expcom	⊢ ( 𝑡 = { 𝑥 } → ( 𝑢 = { 𝑥 } → 𝑢 = 𝑡 ) )
58	55 57	biimtrdi	⊢ ( 𝑥 = 𝑦 → ( 𝑡 = { 𝑥 , 𝑦 } → ( 𝑢 = { 𝑥 } → 𝑢 = 𝑡 ) ) )
59	58	com13	⊢ ( 𝑢 = { 𝑥 } → ( 𝑡 = { 𝑥 , 𝑦 } → ( 𝑥 = 𝑦 → 𝑢 = 𝑡 ) ) )
60	59	imp	⊢ ( ( 𝑢 = { 𝑥 } ∧ 𝑡 = { 𝑥 , 𝑦 } ) → ( 𝑥 = 𝑦 → 𝑢 = 𝑡 ) )
61	51 60	sylcom	⊢ ( Fun ⟨ 𝑢 , 𝑡 ⟩ → ( ( 𝑢 = { 𝑥 } ∧ 𝑡 = { 𝑥 , 𝑦 } ) → 𝑢 = 𝑡 ) )
62	61	exlimdvv	⊢ ( Fun ⟨ 𝑢 , 𝑡 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ( 𝑢 = { 𝑥 } ∧ 𝑡 = { 𝑥 , 𝑦 } ) → 𝑢 = 𝑡 ) )
63	13 62	mpd	⊢ ( Fun ⟨ 𝑢 , 𝑡 ⟩ → 𝑢 = 𝑡 )
64	4 8 63	vtocl2g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( Fun ⟨ 𝐴 , 𝐵 ⟩ → 𝐴 = 𝐵 ) )
65	64	3impia	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ Fun ⟨ 𝐴 , 𝐵 ⟩ ) → 𝐴 = 𝐵 )