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

Metamath Proof Explorer

Theorem eloprabi

Description: A consequence of membership in an operation class abstraction, using ordered pair extractors. (Contributed by NM, 6-Nov-2006) (Revised by David Abernethy, 19-Jun-2012)

Ref Expression
Hypotheses eloprabi.1 ⊢ ( 𝑥 = ( 1st ‘ ( 1st ‘ 𝐴 ) ) → ( 𝜑 ↔ 𝜓 ) )
eloprabi.2 ⊢ ( 𝑦 = ( 2nd ‘ ( 1st ‘ 𝐴 ) ) → ( 𝜓 ↔ 𝜒 ) )
eloprabi.3 ⊢ ( 𝑧 = ( 2nd ‘ 𝐴 ) → ( 𝜒 ↔ 𝜃 ) )
Assertion eloprabi ( 𝐴 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → 𝜃 )

Proof

Step Hyp Ref Expression
1 eloprabi.1 ⊢ ( 𝑥 = ( 1st ‘ ( 1st ‘ 𝐴 ) ) → ( 𝜑 ↔ 𝜓 ) )
2 eloprabi.2 ⊢ ( 𝑦 = ( 2nd ‘ ( 1st ‘ 𝐴 ) ) → ( 𝜓 ↔ 𝜒 ) )
3 eloprabi.3 ⊢ ( 𝑧 = ( 2nd ‘ 𝐴 ) → ( 𝜒 ↔ 𝜃 ) )
4 eqeq1 ⊢ ( 𝑤 = 𝐴 → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
5 4 anbi1d ⊢ ( 𝑤 = 𝐴 → ( ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ) )
6 5 3exbidv ⊢ ( 𝑤 = 𝐴 → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ) )
7 df-oprab ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) }
8 6 7 elab2g ⊢ ( 𝐴 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → ( 𝐴 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ) )
9 8 ibi ⊢ ( 𝐴 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
10 opex ⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
11 vex ⊢ 𝑧 ∈ V
12 10 11 op1std ⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 1st ‘ 𝐴 ) = ⟨ 𝑥 , 𝑦 ⟩ )
13 12 fveq2d ⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 1st ‘ ( 1st ‘ 𝐴 ) ) = ( 1st ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
14 vex ⊢ 𝑥 ∈ V
15 vex ⊢ 𝑦 ∈ V
16 14 15 op1st ⊢ ( 1st ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑥
17 13 16 eqtr2di ⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → 𝑥 = ( 1st ‘ ( 1st ‘ 𝐴 ) ) )
18 17 1 syl ⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝜑 ↔ 𝜓 ) )
19 12 fveq2d ⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 2nd ‘ ( 1st ‘ 𝐴 ) ) = ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
20 14 15 op2nd ⊢ ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦
21 19 20 eqtr2di ⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → 𝑦 = ( 2nd ‘ ( 1st ‘ 𝐴 ) ) )
22 21 2 syl ⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝜓 ↔ 𝜒 ) )
23 10 11 op2ndd ⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 2nd ‘ 𝐴 ) = 𝑧 )
24 23 eqcomd ⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → 𝑧 = ( 2nd ‘ 𝐴 ) )
25 24 3 syl ⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝜒 ↔ 𝜃 ) )
26 18 22 25 3bitrd ⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝜑 ↔ 𝜃 ) )
27 26 biimpa ⊢ ( ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜃 )
28 27 exlimiv ⊢ ( ∃ 𝑧 ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜃 )
29 28 exlimiv ⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜃 )
30 29 exlimiv ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜃 )
31 9 30 syl ⊢ ( 𝐴 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → 𝜃 )