This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funopsn

Description: If a function is an ordered pair then it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020) (Proof shortened by AV, 15-Jul-2021) (Proof shortened by Eric Schmidt, 9-May-2026) 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
Hypotheses funopsn.x ⊢ 𝑋 ∈ V
funopsn.y ⊢ 𝑌 ∈ V
Assertion funopsn ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) → ∃ 𝑎 ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) )

Proof

Step Hyp Ref Expression
1 funopsn.x ⊢ 𝑋 ∈ V
2 funopsn.y ⊢ 𝑌 ∈ V
3 funiun ⊢ ( Fun 𝐹 → 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } )
4 eqeq1 ⊢ ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ↔ ⟨ 𝑋 , 𝑌 ⟩ = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ) )
5 eqcom ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ↔ ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = ⟨ 𝑋 , 𝑌 ⟩ )
6 4 5 bitrdi ⊢ ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ↔ ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = ⟨ 𝑋 , 𝑌 ⟩ ) )
7 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
8 7 1 2 iunopeqop ⊢ ( ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = ⟨ 𝑋 , 𝑌 ⟩ → ∃ 𝑎 dom 𝐹 = { 𝑎 } )
9 6 8 biimtrdi ⊢ ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } → ∃ 𝑎 dom 𝐹 = { 𝑎 } ) )
10 9 imp ⊢ ( ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ) → ∃ 𝑎 dom 𝐹 = { 𝑎 } )
11 iuneq1 ⊢ ( dom 𝐹 = { 𝑎 } → ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = ∪ 𝑥 ∈ { 𝑎 } { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } )
12 vex ⊢ 𝑎 ∈ V
13 id ⊢ ( 𝑥 = 𝑎 → 𝑥 = 𝑎 )
14 fveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑎 ) )
15 13 14 opeq12d ⊢ ( 𝑥 = 𝑎 → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ = ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ )
16 15 sneqd ⊢ ( 𝑥 = 𝑎 → { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } )
17 12 16 iunxsn ⊢ ∪ 𝑥 ∈ { 𝑎 } { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ }
18 11 17 eqtrdi ⊢ ( dom 𝐹 = { 𝑎 } → ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } )
19 18 eqeq2d ⊢ ( dom 𝐹 = { 𝑎 } → ( 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ↔ 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ) )
20 19 adantl ⊢ ( ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ∧ dom 𝐹 = { 𝑎 } ) → ( 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ↔ 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ) )
21 eqeq1 ⊢ ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ↔ ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ) )
22 eqcom ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ↔ { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } = ⟨ 𝑋 , 𝑌 ⟩ )
23 fvex ⊢ ( 𝐹 ‘ 𝑎 ) ∈ V
24 12 23 snopeqop ⊢ ( { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } = ⟨ 𝑋 , 𝑌 ⟩ ↔ ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) )
25 22 24 sylbb ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } → ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) )
26 21 25 biimtrdi ⊢ ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } → ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) ) )
27 simpr3 ⊢ ( ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ∧ ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) ) → 𝑋 = { 𝑎 } )
28 simp1 ⊢ ( ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) → 𝑎 = ( 𝐹 ‘ 𝑎 ) )
29 28 eqcomd ⊢ ( ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) → ( 𝐹 ‘ 𝑎 ) = 𝑎 )
30 29 opeq2d ⊢ ( ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) → ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ = ⟨ 𝑎 , 𝑎 ⟩ )
31 30 sneqd ⊢ ( ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) → { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } = { ⟨ 𝑎 , 𝑎 ⟩ } )
32 31 eqeq2d ⊢ ( ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) → ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ↔ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) )
33 32 biimpac ⊢ ( ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ∧ ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) ) → 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } )
34 27 33 jca ⊢ ( ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ∧ ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) ) → ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) )
35 34 ex ⊢ ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } → ( ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) → ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) )
36 26 35 sylcom ⊢ ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } → ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) )
37 36 adantr ⊢ ( ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ∧ dom 𝐹 = { 𝑎 } ) → ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } → ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) )
38 20 37 sylbid ⊢ ( ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ∧ dom 𝐹 = { 𝑎 } ) → ( 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } → ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) )
39 38 impancom ⊢ ( ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ) → ( dom 𝐹 = { 𝑎 } → ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) )
40 39 eximdv ⊢ ( ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ) → ( ∃ 𝑎 dom 𝐹 = { 𝑎 } → ∃ 𝑎 ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) )
41 10 40 mpd ⊢ ( ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ) → ∃ 𝑎 ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) )
42 3 41 sylan2 ⊢ ( ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ∧ Fun 𝐹 ) → ∃ 𝑎 ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) )
43 42 ancoms ⊢ ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) → ∃ 𝑎 ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) )