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