funopdmsn

Description: The domain of a function which is an ordered pair is a singleton. (Contributed by AV, 15-Nov-2021) (Avoid depending on this detail.)

	Ref	Expression
Hypotheses	funopdmsn.g	⊢ 𝐺 = ⟨ 𝑋 , 𝑌 ⟩
	funopdmsn.x	⊢ 𝑋 ∈ 𝑉
	funopdmsn.y	⊢ 𝑌 ∈ 𝑊
Assertion	funopdmsn	⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ∧ 𝐵 ∈ dom 𝐺 ) → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		funopdmsn.g	⊢ 𝐺 = ⟨ 𝑋 , 𝑌 ⟩
2		funopdmsn.x	⊢ 𝑋 ∈ 𝑉
3		funopdmsn.y	⊢ 𝑌 ∈ 𝑊
4	1	funeqi	⊢ ( Fun 𝐺 ↔ Fun ⟨ 𝑋 , 𝑌 ⟩ )
5	2	elexi	⊢ 𝑋 ∈ V
6	3	elexi	⊢ 𝑌 ∈ V
7	5 6	funop	⊢ ( Fun ⟨ 𝑋 , 𝑌 ⟩ ↔ ∃ 𝑥 ( 𝑋 = { 𝑥 } ∧ ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑥 , 𝑥 ⟩ } ) )
8	4 7	bitri	⊢ ( Fun 𝐺 ↔ ∃ 𝑥 ( 𝑋 = { 𝑥 } ∧ ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑥 , 𝑥 ⟩ } ) )
9	1	eqcomi	⊢ ⟨ 𝑋 , 𝑌 ⟩ = 𝐺
10	9	eqeq1i	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑥 , 𝑥 ⟩ } ↔ 𝐺 = { ⟨ 𝑥 , 𝑥 ⟩ } )
11		dmeq	⊢ ( 𝐺 = { ⟨ 𝑥 , 𝑥 ⟩ } → dom 𝐺 = dom { ⟨ 𝑥 , 𝑥 ⟩ } )
12		vex	⊢ 𝑥 ∈ V
13	12	dmsnop	⊢ dom { ⟨ 𝑥 , 𝑥 ⟩ } = { 𝑥 }
14	11 13	eqtrdi	⊢ ( 𝐺 = { ⟨ 𝑥 , 𝑥 ⟩ } → dom 𝐺 = { 𝑥 } )
15		eleq2	⊢ ( dom 𝐺 = { 𝑥 } → ( 𝐴 ∈ dom 𝐺 ↔ 𝐴 ∈ { 𝑥 } ) )
16		eleq2	⊢ ( dom 𝐺 = { 𝑥 } → ( 𝐵 ∈ dom 𝐺 ↔ 𝐵 ∈ { 𝑥 } ) )
17	15 16	anbi12d	⊢ ( dom 𝐺 = { 𝑥 } → ( ( 𝐴 ∈ dom 𝐺 ∧ 𝐵 ∈ dom 𝐺 ) ↔ ( 𝐴 ∈ { 𝑥 } ∧ 𝐵 ∈ { 𝑥 } ) ) )
18		elsni	⊢ ( 𝐴 ∈ { 𝑥 } → 𝐴 = 𝑥 )
19		elsni	⊢ ( 𝐵 ∈ { 𝑥 } → 𝐵 = 𝑥 )
20		eqtr3	⊢ ( ( 𝐴 = 𝑥 ∧ 𝐵 = 𝑥 ) → 𝐴 = 𝐵 )
21	18 19 20	syl2an	⊢ ( ( 𝐴 ∈ { 𝑥 } ∧ 𝐵 ∈ { 𝑥 } ) → 𝐴 = 𝐵 )
22	17 21	biimtrdi	⊢ ( dom 𝐺 = { 𝑥 } → ( ( 𝐴 ∈ dom 𝐺 ∧ 𝐵 ∈ dom 𝐺 ) → 𝐴 = 𝐵 ) )
23	14 22	syl	⊢ ( 𝐺 = { ⟨ 𝑥 , 𝑥 ⟩ } → ( ( 𝐴 ∈ dom 𝐺 ∧ 𝐵 ∈ dom 𝐺 ) → 𝐴 = 𝐵 ) )
24	10 23	sylbi	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑥 , 𝑥 ⟩ } → ( ( 𝐴 ∈ dom 𝐺 ∧ 𝐵 ∈ dom 𝐺 ) → 𝐴 = 𝐵 ) )
25	24	adantl	⊢ ( ( 𝑋 = { 𝑥 } ∧ ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑥 , 𝑥 ⟩ } ) → ( ( 𝐴 ∈ dom 𝐺 ∧ 𝐵 ∈ dom 𝐺 ) → 𝐴 = 𝐵 ) )
26	25	exlimiv	⊢ ( ∃ 𝑥 ( 𝑋 = { 𝑥 } ∧ ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑥 , 𝑥 ⟩ } ) → ( ( 𝐴 ∈ dom 𝐺 ∧ 𝐵 ∈ dom 𝐺 ) → 𝐴 = 𝐵 ) )
27	8 26	sylbi	⊢ ( Fun 𝐺 → ( ( 𝐴 ∈ dom 𝐺 ∧ 𝐵 ∈ dom 𝐺 ) → 𝐴 = 𝐵 ) )
28	27	3impib	⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ∧ 𝐵 ∈ dom 𝐺 ) → 𝐴 = 𝐵 )

Metamath Proof Explorer

Theorem funopdmsn

Proof