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 ( ( ( 𝐴𝐺𝐵𝐻 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 ) ∧ 𝑆𝐽 ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 )