Theorem fwfffun

Description: If ps is function-like over A , then F matches its behavior. (Contributed by BTernaryTau, 28-Sep-2026)

	Ref	Expression
Hypotheses	fwfffun.1	⊢ Ⅎ 𝑦 𝜓
	fwfffun.2	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ( 𝜓 → 𝑧 = 𝑦 ) )
	fwfffun.3	⊢ 𝐹 = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) }
Assertion	fwfffun	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fwfffun.1	⊢ Ⅎ 𝑦 𝜓
2		fwfffun.2	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ( 𝜓 → 𝑧 = 𝑦 ) )
3		fwfffun.3	⊢ 𝐹 = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) }
4	3	eleq2i	⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } )
5		opabidw	⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) )
6	4 5	bitri	⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) )
7	1	rmo2	⊢ ( ∃* 𝑧 ∈ 𝐴 𝜓 ↔ ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ( 𝜓 → 𝑧 = 𝑦 ) )
8	7	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑧 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ( 𝜓 → 𝑧 = 𝑦 ) )
9	2 8	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃* 𝑧 ∈ 𝐴 𝜓 )
10		funopab	⊢ ( Fun { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } ↔ ∀ 𝑥 ∃* 𝑧 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) )
11	3	funeqi	⊢ ( Fun 𝐹 ↔ Fun { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } )
12		2reu5lem2	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑧 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ∃* 𝑧 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) )
13	10 11 12	3bitr4i	⊢ ( Fun 𝐹 ↔ ∀ 𝑥 ∈ 𝐴 ∃* 𝑧 ∈ 𝐴 𝜓 )
14	9 13	sylibr	⊢ ( 𝜑 → Fun 𝐹 )
15		df-br	⊢ ( 𝑥 𝐹 𝑧 ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 )
16		funbrfv2b	⊢ ( Fun 𝐹 → ( 𝑥 𝐹 𝑧 ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑧 ) ) )
17	15 16	bitr3id	⊢ ( Fun 𝐹 → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑧 ) ) )
18	14 17	syl	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑧 ) ) )
19	6 18	bitr3id	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑧 ) ) )