Theorem fwfffunres

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

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

Proof

Step	Hyp	Ref	Expression
1		fwfffunres.1	⊢ Ⅎ 𝑦 𝜓
2		fwfffunres.2	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐴 ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ( 𝜓 → 𝑧 = 𝑦 ) )
3		fwfffunres.3	⊢ 𝐹 = ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } ↾ 𝑥 )
4		eqid	⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) }
5	1 2 4	fwfffun	⊢ ( 𝜑 → ( ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑤 ∈ dom { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } ∧ ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } ‘ 𝑤 ) = 𝑧 ) ) )
6	5	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑥 ) → ( ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑤 ∈ dom { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } ∧ ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } ‘ 𝑤 ) = 𝑧 ) ) )
7	3	dmeqi	⊢ dom 𝐹 = dom ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } ↾ 𝑥 )
8		dmres	⊢ dom ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } ↾ 𝑥 ) = ( 𝑥 ∩ dom { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } )
9	7 8	eqtri	⊢ dom 𝐹 = ( 𝑥 ∩ dom { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } )
10	9	elin2	⊢ ( 𝑤 ∈ dom 𝐹 ↔ ( 𝑤 ∈ 𝑥 ∧ 𝑤 ∈ dom { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } ) )
11	10	baib	⊢ ( 𝑤 ∈ 𝑥 → ( 𝑤 ∈ dom 𝐹 ↔ 𝑤 ∈ dom { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } ) )
12	3	fveq1i	⊢ ( 𝐹 ‘ 𝑤 ) = ( ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } ↾ 𝑥 ) ‘ 𝑤 )
13		fvres	⊢ ( 𝑤 ∈ 𝑥 → ( ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } ↾ 𝑥 ) ‘ 𝑤 ) = ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } ‘ 𝑤 ) )
14	12 13	eqtrid	⊢ ( 𝑤 ∈ 𝑥 → ( 𝐹 ‘ 𝑤 ) = ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } ‘ 𝑤 ) )
15	14	eqeq1d	⊢ ( 𝑤 ∈ 𝑥 → ( ( 𝐹 ‘ 𝑤 ) = 𝑧 ↔ ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } ‘ 𝑤 ) = 𝑧 ) )
16	11 15	anbi12d	⊢ ( 𝑤 ∈ 𝑥 → ( ( 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ↔ ( 𝑤 ∈ dom { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } ∧ ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } ‘ 𝑤 ) = 𝑧 ) ) )
17	16	adantl	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑥 ) → ( ( 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ↔ ( 𝑤 ∈ dom { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } ∧ ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) } ‘ 𝑤 ) = 𝑧 ) ) )
18	6 17	bitr4d	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑥 ) → ( ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) )
19	18	pm5.32da	⊢ ( 𝜑 → ( ( 𝑤 ∈ 𝑥 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ( 𝑤 ∈ 𝑥 ∧ ( 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) )
20		an4	⊢ ( ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑤 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝜓 ) ) )
21		ancom	⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥 ) ↔ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝐴 ) )
22	21	anbi1i	⊢ ( ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ( ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝜓 ) ) )
23		an4	⊢ ( ( ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ( ( 𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝜓 ) ) )
24	20 22 23	3bitri	⊢ ( ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑤 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ( ( 𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝜓 ) ) )
25		13an22anass	⊢ ( ( 𝑧 ∈ 𝐴 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑤 ∈ 𝑥 ∧ 𝜓 ) ) )
26		13an22anass	⊢ ( ( 𝑤 ∈ 𝑥 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ( ( 𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝜓 ) ) )
27	24 25 26	3bitr4i	⊢ ( ( 𝑧 ∈ 𝐴 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ( 𝑤 ∈ 𝑥 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓 ) ) )
28	10	simplbi	⊢ ( 𝑤 ∈ dom 𝐹 → 𝑤 ∈ 𝑥 )
29	28	adantr	⊢ ( ( 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) → 𝑤 ∈ 𝑥 )
30	29	pm4.71ri	⊢ ( ( 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ↔ ( 𝑤 ∈ 𝑥 ∧ ( 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) )
31	19 27 30	3bitr4g	⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ( 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) )