Theorem funop1

Description: A function is an ordered pair iff it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020) (Avoid depending on this detail.)

	Ref	Expression
Assertion	funop1	⊢ ( ∃ 𝑥 ∃ 𝑦 𝐹 = ⟨ 𝑥 , 𝑦 ⟩ → ( Fun 𝐹 ↔ ∃ 𝑥 ∃ 𝑦 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ } ) )

Proof

Step	Hyp	Ref	Expression
1		opeq12	⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑤 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑣 , 𝑤 ⟩ )
2	1	eqeq2d	⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑤 ) → ( 𝐹 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝐹 = ⟨ 𝑣 , 𝑤 ⟩ ) )
3	2	cbvex2vw	⊢ ( ∃ 𝑥 ∃ 𝑦 𝐹 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑣 ∃ 𝑤 𝐹 = ⟨ 𝑣 , 𝑤 ⟩ )
4		vex	⊢ 𝑣 ∈ V
5		vex	⊢ 𝑤 ∈ V
6	4 5	funopsn	⊢ ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑣 , 𝑤 ⟩ ) → ∃ 𝑎 ( 𝑣 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) )
7		vex	⊢ 𝑎 ∈ V
8		opeq12	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑎 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑎 ⟩ )
9	8	sneqd	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑎 ) → { ⟨ 𝑥 , 𝑦 ⟩ } = { ⟨ 𝑎 , 𝑎 ⟩ } )
10	9	eqeq2d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑎 ) → ( 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ } ↔ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) )
11	7 7 10	spc2ev	⊢ ( 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } → ∃ 𝑥 ∃ 𝑦 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ } )
12	11	adantl	⊢ ( ( 𝑣 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) → ∃ 𝑥 ∃ 𝑦 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ } )
13	12	exlimiv	⊢ ( ∃ 𝑎 ( 𝑣 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) → ∃ 𝑥 ∃ 𝑦 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ } )
14	6 13	syl	⊢ ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑣 , 𝑤 ⟩ ) → ∃ 𝑥 ∃ 𝑦 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ } )
15	14	expcom	⊢ ( 𝐹 = ⟨ 𝑣 , 𝑤 ⟩ → ( Fun 𝐹 → ∃ 𝑥 ∃ 𝑦 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ } ) )
16		vex	⊢ 𝑥 ∈ V
17		vex	⊢ 𝑦 ∈ V
18	16 17	funsn	⊢ Fun { ⟨ 𝑥 , 𝑦 ⟩ }
19		funeq	⊢ ( 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ } → ( Fun 𝐹 ↔ Fun { ⟨ 𝑥 , 𝑦 ⟩ } ) )
20	18 19	mpbiri	⊢ ( 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ } → Fun 𝐹 )
21	20	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ } → Fun 𝐹 )
22	15 21	impbid1	⊢ ( 𝐹 = ⟨ 𝑣 , 𝑤 ⟩ → ( Fun 𝐹 ↔ ∃ 𝑥 ∃ 𝑦 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ } ) )
23	22	exlimivv	⊢ ( ∃ 𝑣 ∃ 𝑤 𝐹 = ⟨ 𝑣 , 𝑤 ⟩ → ( Fun 𝐹 ↔ ∃ 𝑥 ∃ 𝑦 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ } ) )
24	3 23	sylbi	⊢ ( ∃ 𝑥 ∃ 𝑦 𝐹 = ⟨ 𝑥 , 𝑦 ⟩ → ( Fun 𝐹 ↔ ∃ 𝑥 ∃ 𝑦 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ } ) )