Theorem fvmptopab

Description: The function value of a mapping M to a restricted binary relation expressed as an ordered-pair class abstraction: The restricted binary relation is a binary relation given as value of a function F restricted by the condition ps . (Contributed by AV, 31-Jan-2021) (Revised by AV, 29-Oct-2021) Add disjoint variable condition on F , x , y to remove a sethood hypothesis. (Revised by SN, 13-Dec-2024)

	Ref	Expression
Hypotheses	fvmptopab.1	⊢ ( 𝑧 = 𝑍 → ( 𝜑 ↔ 𝜓 ) )
	fvmptopab.m	⊢ 𝑀 = ( 𝑧 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑧 ) 𝑦 ∧ 𝜑 ) } )
Assertion	fvmptopab	⊢ ( 𝑀 ‘ 𝑍 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) }

Proof

Step	Hyp	Ref	Expression
1		fvmptopab.1	⊢ ( 𝑧 = 𝑍 → ( 𝜑 ↔ 𝜓 ) )
2		fvmptopab.m	⊢ 𝑀 = ( 𝑧 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑧 ) 𝑦 ∧ 𝜑 ) } )
3		fveq2	⊢ ( 𝑧 = 𝑍 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑍 ) )
4	3	breqd	⊢ ( 𝑧 = 𝑍 → ( 𝑥 ( 𝐹 ‘ 𝑧 ) 𝑦 ↔ 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ) )
5	4 1	anbi12d	⊢ ( 𝑧 = 𝑍 → ( ( 𝑥 ( 𝐹 ‘ 𝑧 ) 𝑦 ∧ 𝜑 ) ↔ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) ) )
6	5	opabbidv	⊢ ( 𝑧 = 𝑍 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑧 ) 𝑦 ∧ 𝜑 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) } )
7		opabresex2	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) } ∈ V
8	6 2 7	fvmpt	⊢ ( 𝑍 ∈ V → ( 𝑀 ‘ 𝑍 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) } )
9		fvprc	⊢ ( ¬ 𝑍 ∈ V → ( 𝑀 ‘ 𝑍 ) = ∅ )
10		elopabran	⊢ ( 𝑧 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) } → 𝑧 ∈ ( 𝐹 ‘ 𝑍 ) )
11	10	ssriv	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) } ⊆ ( 𝐹 ‘ 𝑍 )
12		fvprc	⊢ ( ¬ 𝑍 ∈ V → ( 𝐹 ‘ 𝑍 ) = ∅ )
13	11 12	sseqtrid	⊢ ( ¬ 𝑍 ∈ V → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) } ⊆ ∅ )
14		ss0	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) } ⊆ ∅ → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) } = ∅ )
15	13 14	syl	⊢ ( ¬ 𝑍 ∈ V → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) } = ∅ )
16	9 15	eqtr4d	⊢ ( ¬ 𝑍 ∈ V → ( 𝑀 ‘ 𝑍 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) } )
17	8 16	pm2.61i	⊢ ( 𝑀 ‘ 𝑍 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) }