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) 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 6 adantl ⊢ ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ↔ ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = ⟨ 𝑋 , 𝑌 ⟩ ) )
8 1 2 opnzi ⊢ ⟨ 𝑋 , 𝑌 ⟩ ≠ ∅
9 neeq1 ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = 𝐹 → ( ⟨ 𝑋 , 𝑌 ⟩ ≠ ∅ ↔ 𝐹 ≠ ∅ ) )
10 9 eqcoms ⊢ ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ → ( ⟨ 𝑋 , 𝑌 ⟩ ≠ ∅ ↔ 𝐹 ≠ ∅ ) )
11 funrel ⊢ ( Fun 𝐹 → Rel 𝐹 )
12 reldm0 ⊢ ( Rel 𝐹 → ( 𝐹 = ∅ ↔ dom 𝐹 = ∅ ) )
13 11 12 syl ⊢ ( Fun 𝐹 → ( 𝐹 = ∅ ↔ dom 𝐹 = ∅ ) )
14 13 biimprd ⊢ ( Fun 𝐹 → ( dom 𝐹 = ∅ → 𝐹 = ∅ ) )
15 14 necon3d ⊢ ( Fun 𝐹 → ( 𝐹 ≠ ∅ → dom 𝐹 ≠ ∅ ) )
16 15 com12 ⊢ ( 𝐹 ≠ ∅ → ( Fun 𝐹 → dom 𝐹 ≠ ∅ ) )
17 10 16 syl6bi ⊢ ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ → ( ⟨ 𝑋 , 𝑌 ⟩ ≠ ∅ → ( Fun 𝐹 → dom 𝐹 ≠ ∅ ) ) )
18 17 com3l ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ≠ ∅ → ( Fun 𝐹 → ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ → dom 𝐹 ≠ ∅ ) ) )
19 18 impd ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ≠ ∅ → ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) → dom 𝐹 ≠ ∅ ) )
20 8 19 ax-mp ⊢ ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) → dom 𝐹 ≠ ∅ )
21 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
22 21 1 2 iunopeqop ⊢ ( dom 𝐹 ≠ ∅ → ( ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = ⟨ 𝑋 , 𝑌 ⟩ → ∃ 𝑎 dom 𝐹 = { 𝑎 } ) )
23 20 22 syl ⊢ ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = ⟨ 𝑋 , 𝑌 ⟩ → ∃ 𝑎 dom 𝐹 = { 𝑎 } ) )
24 7 23 sylbid ⊢ ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } → ∃ 𝑎 dom 𝐹 = { 𝑎 } ) )
25 24 imp ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) ∧ 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ) → ∃ 𝑎 dom 𝐹 = { 𝑎 } )
26 iuneq1 ⊢ ( dom 𝐹 = { 𝑎 } → ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = ∪ 𝑥 ∈ { 𝑎 } { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } )
27 vex ⊢ 𝑎 ∈ V
28 id ⊢ ( 𝑥 = 𝑎 → 𝑥 = 𝑎 )
29 fveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑎 ) )
30 28 29 opeq12d ⊢ ( 𝑥 = 𝑎 → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ = ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ )
31 30 sneqd ⊢ ( 𝑥 = 𝑎 → { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } )
32 27 31 iunxsn ⊢ ∪ 𝑥 ∈ { 𝑎 } { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ }
33 26 32 eqtrdi ⊢ ( dom 𝐹 = { 𝑎 } → ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } )
34 33 adantl ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) ∧ dom 𝐹 = { 𝑎 } ) → ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } )
35 34 eqeq2d ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) ∧ dom 𝐹 = { 𝑎 } ) → ( 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ↔ 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ) )
36 eqeq1 ⊢ ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ↔ ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ) )
37 36 adantl ⊢ ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ↔ ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ) )
38 eqcom ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ↔ { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } = ⟨ 𝑋 , 𝑌 ⟩ )
39 fvex ⊢ ( 𝐹 ‘ 𝑎 ) ∈ V
40 27 39 snopeqop ⊢ ( { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } = ⟨ 𝑋 , 𝑌 ⟩ ↔ ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) )
41 38 40 sylbb ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } → ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) )
42 37 41 syl6bi ⊢ ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } → ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) ) )
43 42 imp ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) ∧ 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ) → ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) )
44 simpr3 ⊢ ( ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ∧ ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) ) → 𝑋 = { 𝑎 } )
45 simp1 ⊢ ( ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) → 𝑎 = ( 𝐹 ‘ 𝑎 ) )
46 45 eqcomd ⊢ ( ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) → ( 𝐹 ‘ 𝑎 ) = 𝑎 )
47 46 opeq2d ⊢ ( ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) → ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ = ⟨ 𝑎 , 𝑎 ⟩ )
48 47 sneqd ⊢ ( ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) → { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } = { ⟨ 𝑎 , 𝑎 ⟩ } )
49 48 eqeq2d ⊢ ( ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) → ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ↔ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) )
50 49 biimpac ⊢ ( ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ∧ ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) ) → 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } )
51 44 50 jca ⊢ ( ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ∧ ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) ) → ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) )
52 51 ex ⊢ ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } → ( ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) → ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) )
53 52 adantl ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) ∧ 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ) → ( ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) → ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) )
54 53 a1dd ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) ∧ 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ) → ( ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) → ( dom 𝐹 = { 𝑎 } → ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) ) )
55 43 54 mpd ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) ∧ 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ) → ( dom 𝐹 = { 𝑎 } → ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) )
56 55 impancom ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) ∧ dom 𝐹 = { 𝑎 } ) → ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } → ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) )
57 35 56 sylbid ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) ∧ dom 𝐹 = { 𝑎 } ) → ( 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } → ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) )
58 57 impancom ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) ∧ 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ) → ( dom 𝐹 = { 𝑎 } → ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) )
59 58 eximdv ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) ∧ 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ) → ( ∃ 𝑎 dom 𝐹 = { 𝑎 } → ∃ 𝑎 ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) )
60 25 59 mpd ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) ∧ 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ) → ∃ 𝑎 ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) )
61 3 60 mpidan ⊢ ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) → ∃ 𝑎 ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) )