This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brfvopabrbr

Description: The binary relation of a function value which is an ordered-pair class abstraction of a restricted binary relation is the restricted binary relation. The first hypothesis can often be obtained by using fvmptopab . (Contributed by AV, 29-Oct-2021)

Ref Expression
Hypotheses brfvopabrbr.1 ⊢ ( 𝐴 ‘ 𝑍 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐵 ‘ 𝑍 ) 𝑦 ∧ 𝜑 ) }
brfvopabrbr.2 ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝜑 ↔ 𝜓 ) )
brfvopabrbr.3 ⊢ Rel ( 𝐵 ‘ 𝑍 )
Assertion brfvopabrbr ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 ↔ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 ∧ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 brfvopabrbr.1 ⊢ ( 𝐴 ‘ 𝑍 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐵 ‘ 𝑍 ) 𝑦 ∧ 𝜑 ) }
2 brfvopabrbr.2 ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝜑 ↔ 𝜓 ) )
3 brfvopabrbr.3 ⊢ Rel ( 𝐵 ‘ 𝑍 )
4 brne0 ⊢ ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 → ( 𝐴 ‘ 𝑍 ) ≠ ∅ )
5 fvprc ⊢ ( ¬ 𝑍 ∈ V → ( 𝐴 ‘ 𝑍 ) = ∅ )
6 5 necon1ai ⊢ ( ( 𝐴 ‘ 𝑍 ) ≠ ∅ → 𝑍 ∈ V )
7 4 6 syl ⊢ ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 → 𝑍 ∈ V )
8 1 relopabiv ⊢ Rel ( 𝐴 ‘ 𝑍 )
9 8 brrelex1i ⊢ ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 → 𝑋 ∈ V )
10 8 brrelex2i ⊢ ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 → 𝑌 ∈ V )
11 7 9 10 3jca ⊢ ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 → ( 𝑍 ∈ V ∧ 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
12 brne0 ⊢ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 → ( 𝐵 ‘ 𝑍 ) ≠ ∅ )
13 fvprc ⊢ ( ¬ 𝑍 ∈ V → ( 𝐵 ‘ 𝑍 ) = ∅ )
14 13 necon1ai ⊢ ( ( 𝐵 ‘ 𝑍 ) ≠ ∅ → 𝑍 ∈ V )
15 12 14 syl ⊢ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 → 𝑍 ∈ V )
16 3 brrelex1i ⊢ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 → 𝑋 ∈ V )
17 3 brrelex2i ⊢ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 → 𝑌 ∈ V )
18 15 16 17 3jca ⊢ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 → ( 𝑍 ∈ V ∧ 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
19 18 adantr ⊢ ( ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 ∧ 𝜓 ) → ( 𝑍 ∈ V ∧ 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
20 1 a1i ⊢ ( 𝑍 ∈ V → ( 𝐴 ‘ 𝑍 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐵 ‘ 𝑍 ) 𝑦 ∧ 𝜑 ) } )
21 20 2 rbropap ⊢ ( ( 𝑍 ∈ V ∧ 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 ↔ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 ∧ 𝜓 ) ) )
22 11 19 21 pm5.21nii ⊢ ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 ↔ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 ∧ 𝜓 ) )