Metamath Proof Explorer

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)

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

Proof

Step Hyp Ref Expression
1 fvmptopab.1 ⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → ( 𝜒 ↔ 𝜓 ) )
2 fvmptopab.2 ⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 } ∈ V )
3 fvmptopab.3 ⊢ 𝑀 = ( 𝑧 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑧 ) 𝑦 ∧ 𝜒 ) } )
4 fveq2 ⊢ ( 𝑧 = 𝑍 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑍 ) )
5 4 breqd ⊢ ( 𝑧 = 𝑍 → ( 𝑥 ( 𝐹 ‘ 𝑧 ) 𝑦 ↔ 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ) )
6 5 adantl ⊢ ( ( ( 𝑍 ∈ V ∧ 𝜑 ) ∧ 𝑧 = 𝑍 ) → ( 𝑥 ( 𝐹 ‘ 𝑧 ) 𝑦 ↔ 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ) )
7 1 adantll ⊢ ( ( ( 𝑍 ∈ V ∧ 𝜑 ) ∧ 𝑧 = 𝑍 ) → ( 𝜒 ↔ 𝜓 ) )
8 6 7 anbi12d ⊢ ( ( ( 𝑍 ∈ V ∧ 𝜑 ) ∧ 𝑧 = 𝑍 ) → ( ( 𝑥 ( 𝐹 ‘ 𝑧 ) 𝑦 ∧ 𝜒 ) ↔ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) ) )
9 8 opabbidv ⊢ ( ( ( 𝑍 ∈ V ∧ 𝜑 ) ∧ 𝑧 = 𝑍 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑧 ) 𝑦 ∧ 𝜒 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) } )
10 simpl ⊢ ( ( 𝑍 ∈ V ∧ 𝜑 ) → 𝑍 ∈ V )
11 id ⊢ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 → 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 )
12 11 gen2 ⊢ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 → 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 )
13 2 adantl ⊢ ( ( 𝑍 ∈ V ∧ 𝜑 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 } ∈ V )
14 opabbrex ⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 → 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 } ∈ V ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) } ∈ V )
15 12 13 14 sylancr ⊢ ( ( 𝑍 ∈ V ∧ 𝜑 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) } ∈ V )
16 3 9 10 15 fvmptd2 ⊢ ( ( 𝑍 ∈ V ∧ 𝜑 ) → ( 𝑀 ‘ 𝑍 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) } )
17 16 ex ⊢ ( 𝑍 ∈ V → ( 𝜑 → ( 𝑀 ‘ 𝑍 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) } ) )
18 fvprc ⊢ ( ¬ 𝑍 ∈ V → ( 𝑀 ‘ 𝑍 ) = ∅ )
19 br0 ⊢ ¬ 𝑥 ∅ 𝑦
20 fvprc ⊢ ( ¬ 𝑍 ∈ V → ( 𝐹 ‘ 𝑍 ) = ∅ )
21 20 breqd ⊢ ( ¬ 𝑍 ∈ V → ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ↔ 𝑥 ∅ 𝑦 ) )
22 19 21 mtbiri ⊢ ( ¬ 𝑍 ∈ V → ¬ 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 )
23 22 intnanrd ⊢ ( ¬ 𝑍 ∈ V → ¬ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) )
24 23 alrimivv ⊢ ( ¬ 𝑍 ∈ V → ∀ 𝑥 ∀ 𝑦 ¬ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) )
25 opab0 ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) } = ∅ ↔ ∀ 𝑥 ∀ 𝑦 ¬ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) )
26 24 25 sylibr ⊢ ( ¬ 𝑍 ∈ V → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) } = ∅ )
27 18 26 eqtr4d ⊢ ( ¬ 𝑍 ∈ V → ( 𝑀 ‘ 𝑍 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) } )
28 27 a1d ⊢ ( ¬ 𝑍 ∈ V → ( 𝜑 → ( 𝑀 ‘ 𝑍 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) } ) )
29 17 28 pm2.61i ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑍 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐹 ‘ 𝑍 ) 𝑦 ∧ 𝜓 ) } )