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

Metamath Proof Explorer

Theorem brfvopab

Description: The classes involved in a binary relation of a function value which is an ordered-pair class abstraction are sets. (Contributed by AV, 7-Jan-2021)

Ref Expression
Hypothesis brfvopab.1 ⊢ ( 𝑋 ∈ V → ( 𝐹 ‘ 𝑋 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } )
Assertion brfvopab ( 𝐴 ( 𝐹 ‘ 𝑋 ) 𝐵 → ( 𝑋 ∈ V ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) )

Proof

Step Hyp Ref Expression
1 brfvopab.1 ⊢ ( 𝑋 ∈ V → ( 𝐹 ‘ 𝑋 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } )
2 1 breqd ⊢ ( 𝑋 ∈ V → ( 𝐴 ( 𝐹 ‘ 𝑋 ) 𝐵 ↔ 𝐴 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } 𝐵 ) )
3 brabv ⊢ ( 𝐴 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
4 2 3 biimtrdi ⊢ ( 𝑋 ∈ V → ( 𝐴 ( 𝐹 ‘ 𝑋 ) 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
5 4 imdistani ⊢ ( ( 𝑋 ∈ V ∧ 𝐴 ( 𝐹 ‘ 𝑋 ) 𝐵 ) → ( 𝑋 ∈ V ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
6 3anass ⊢ ( ( 𝑋 ∈ V ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝑋 ∈ V ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
7 5 6 sylibr ⊢ ( ( 𝑋 ∈ V ∧ 𝐴 ( 𝐹 ‘ 𝑋 ) 𝐵 ) → ( 𝑋 ∈ V ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
8 7 ex ⊢ ( 𝑋 ∈ V → ( 𝐴 ( 𝐹 ‘ 𝑋 ) 𝐵 → ( 𝑋 ∈ V ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
9 fvprc ⊢ ( ¬ 𝑋 ∈ V → ( 𝐹 ‘ 𝑋 ) = ∅ )
10 breq ⊢ ( ( 𝐹 ‘ 𝑋 ) = ∅ → ( 𝐴 ( 𝐹 ‘ 𝑋 ) 𝐵 ↔ 𝐴 ∅ 𝐵 ) )
11 br0 ⊢ ¬ 𝐴 ∅ 𝐵
12 11 pm2.21i ⊢ ( 𝐴 ∅ 𝐵 → ( 𝑋 ∈ V ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
13 10 12 biimtrdi ⊢ ( ( 𝐹 ‘ 𝑋 ) = ∅ → ( 𝐴 ( 𝐹 ‘ 𝑋 ) 𝐵 → ( 𝑋 ∈ V ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
14 9 13 syl ⊢ ( ¬ 𝑋 ∈ V → ( 𝐴 ( 𝐹 ‘ 𝑋 ) 𝐵 → ( 𝑋 ∈ V ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
15 8 14 pm2.61i ⊢ ( 𝐴 ( 𝐹 ‘ 𝑋 ) 𝐵 → ( 𝑋 ∈ V ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) )