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

Metamath Proof Explorer

Theorem ov6g

Description: The value of an operation class abstraction. Special case. (Contributed by NM, 13-Nov-2006)

Ref Expression
Hypotheses ov6g.1 ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ → 𝑅 = 𝑆 )
ov6g.2 ⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅 ) }
Assertion ov6g ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 ) ∧ 𝑆 ∈ 𝐽 ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 )

Proof

Step Hyp Ref Expression
1 ov6g.1 ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ → 𝑅 = 𝑆 )
2 ov6g.2 ⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅 ) }
3 df-ov ⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
4 eqid ⊢ 𝑆 = 𝑆
5 biidd ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑆 = 𝑆 ↔ 𝑆 = 𝑆 ) )
6 5 copsex2g ⊢ ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ) → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑆 = 𝑆 ) ↔ 𝑆 = 𝑆 ) )
7 4 6 mpbiri ⊢ ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ) → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑆 = 𝑆 ) )
8 7 3adant3 ⊢ ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 ) → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑆 = 𝑆 ) )
9 8 adantr ⊢ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 ) ∧ 𝑆 ∈ 𝐽 ) → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑆 = 𝑆 ) )
10 eqeq1 ⊢ ( 𝑤 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
11 10 anbi1d ⊢ ( 𝑤 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑧 = 𝑅 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑧 = 𝑅 ) ) )
12 1 eqeq2d ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑧 = 𝑅 ↔ 𝑧 = 𝑆 ) )
13 12 eqcoms ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 = 𝑅 ↔ 𝑧 = 𝑆 ) )
14 13 pm5.32i ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑧 = 𝑅 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑧 = 𝑆 ) )
15 11 14 bitrdi ⊢ ( 𝑤 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑧 = 𝑅 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑧 = 𝑆 ) ) )
16 15 2exbidv ⊢ ( 𝑤 = ⟨ 𝐴 , 𝐵 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑧 = 𝑅 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑧 = 𝑆 ) ) )
17 eqeq1 ⊢ ( 𝑧 = 𝑆 → ( 𝑧 = 𝑆 ↔ 𝑆 = 𝑆 ) )
18 17 anbi2d ⊢ ( 𝑧 = 𝑆 → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑧 = 𝑆 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑆 = 𝑆 ) ) )
19 18 2exbidv ⊢ ( 𝑧 = 𝑆 → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑧 = 𝑆 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑆 = 𝑆 ) ) )
20 moeq ⊢ ∃* 𝑧 𝑧 = 𝑅
21 20 mosubop ⊢ ∃* 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑧 = 𝑅 )
22 21 a1i ⊢ ( 𝑤 ∈ 𝐶 → ∃* 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑧 = 𝑅 ) )
23 dfoprab2 ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅 ) } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅 ) ) }
24 eleq1 ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑤 ∈ 𝐶 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐶 ) )
25 24 anbi1d ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑤 ∈ 𝐶 ∧ 𝑧 = 𝑅 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅 ) ) )
26 25 pm5.32i ⊢ ( ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑧 = 𝑅 ) ) ↔ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅 ) ) )
27 an12 ⊢ ( ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐶 ∧ 𝑧 = 𝑅 ) ) ↔ ( 𝑤 ∈ 𝐶 ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑧 = 𝑅 ) ) )
28 26 27 bitr3i ⊢ ( ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅 ) ) ↔ ( 𝑤 ∈ 𝐶 ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑧 = 𝑅 ) ) )
29 28 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 ∈ 𝐶 ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑧 = 𝑅 ) ) )
30 19.42vv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑤 ∈ 𝐶 ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑧 = 𝑅 ) ) ↔ ( 𝑤 ∈ 𝐶 ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑧 = 𝑅 ) ) )
31 29 30 bitri ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅 ) ) ↔ ( 𝑤 ∈ 𝐶 ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑧 = 𝑅 ) ) )
32 31 opabbii ⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅 ) ) } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐶 ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑧 = 𝑅 ) ) }
33 2 23 32 3eqtri ⊢ 𝐹 = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐶 ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑧 = 𝑅 ) ) }
34 16 19 22 33 fvopab3ig ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 ∧ 𝑆 ∈ 𝐽 ) → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑆 = 𝑆 ) → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝑆 ) )
35 34 3ad2antl3 ⊢ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 ) ∧ 𝑆 ∈ 𝐽 ) → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑆 = 𝑆 ) → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝑆 ) )
36 9 35 mpd ⊢ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 ) ∧ 𝑆 ∈ 𝐽 ) → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝑆 )
37 3 36 eqtrid ⊢ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 ) ∧ 𝑆 ∈ 𝐽 ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 )