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

Metamath Proof Explorer

Theorem 2rbropap

Description: Properties of a pair in a restricted binary relation M expressed as an ordered-pair class abstraction: M is the binary relation W restricted by the conditions ps and ta . (Contributed by AV, 31-Jan-2021)

Ref Expression
Hypotheses 2rbropap.1 ⊢ ( 𝜑 → 𝑀 = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 𝑊 𝑝 ∧ 𝜓 ∧ 𝜏 ) } )
2rbropap.2 ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝜓 ↔ 𝜒 ) )
2rbropap.3 ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝜏 ↔ 𝜃 ) )
Assertion 2rbropap ( ( 𝜑 ∧ 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌 ) → ( 𝐹 𝑀 𝑃 ↔ ( 𝐹 𝑊 𝑃 ∧ 𝜒 ∧ 𝜃 ) ) )

Proof

Step Hyp Ref Expression
1 2rbropap.1 ⊢ ( 𝜑 → 𝑀 = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 𝑊 𝑝 ∧ 𝜓 ∧ 𝜏 ) } )
2 2rbropap.2 ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝜓 ↔ 𝜒 ) )
3 2rbropap.3 ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝜏 ↔ 𝜃 ) )
4 3anass ⊢ ( ( 𝑓 𝑊 𝑝 ∧ 𝜓 ∧ 𝜏 ) ↔ ( 𝑓 𝑊 𝑝 ∧ ( 𝜓 ∧ 𝜏 ) ) )
5 4 opabbii ⊢ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 𝑊 𝑝 ∧ 𝜓 ∧ 𝜏 ) } = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 𝑊 𝑝 ∧ ( 𝜓 ∧ 𝜏 ) ) }
6 1 5 eqtrdi ⊢ ( 𝜑 → 𝑀 = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 𝑊 𝑝 ∧ ( 𝜓 ∧ 𝜏 ) ) } )
7 2 3 anbi12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ( 𝜓 ∧ 𝜏 ) ↔ ( 𝜒 ∧ 𝜃 ) ) )
8 6 7 rbropap ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌 ) → ( 𝐹 𝑀 𝑃 ↔ ( 𝐹 𝑊 𝑃 ∧ ( 𝜒 ∧ 𝜃 ) ) ) )
9 3anass ⊢ ( ( 𝐹 𝑊 𝑃 ∧ 𝜒 ∧ 𝜃 ) ↔ ( 𝐹 𝑊 𝑃 ∧ ( 𝜒 ∧ 𝜃 ) ) )
10 8 9 bitr4di ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌 ) → ( 𝐹 𝑀 𝑃 ↔ ( 𝐹 𝑊 𝑃 ∧ 𝜒 ∧ 𝜃 ) ) )