Metamath Proof Explorer

Theorem ov3

Description: The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995) (Revised by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses ov3.1 ⊢ 𝑆 ∈ V
ov3.2 ⊢ ( ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) ∧ ( 𝑢 = 𝐶 ∧ 𝑓 = 𝐷 ) ) → 𝑅 = 𝑆 )
ov3.3 ⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( 𝐻 × 𝐻 ) ∧ 𝑦 ∈ ( 𝐻 × 𝐻 ) ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ) }
Assertion ov3 ( ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) ∧ ( 𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 ⟨ 𝐶 , 𝐷 ⟩ ) = 𝑆 )

Proof

Step Hyp Ref Expression
1 ov3.1 ⊢ 𝑆 ∈ V
2 ov3.2 ⊢ ( ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) ∧ ( 𝑢 = 𝐶 ∧ 𝑓 = 𝐷 ) ) → 𝑅 = 𝑆 )
3 ov3.3 ⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( 𝐻 × 𝐻 ) ∧ 𝑦 ∈ ( 𝐻 × 𝐻 ) ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ) }
4 1 isseti ⊢ ∃ 𝑧 𝑧 = 𝑆
5 nfv ⊢ Ⅎ 𝑧 ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) ∧ ( 𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻 ) )
6 nfcv ⊢ Ⅎ 𝑧 ⟨ 𝐴 , 𝐵 ⟩
7 nfoprab3 ⊢ Ⅎ 𝑧 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( 𝐻 × 𝐻 ) ∧ 𝑦 ∈ ( 𝐻 × 𝐻 ) ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ) }
8 3 7 nfcxfr ⊢ Ⅎ 𝑧 𝐹
9 nfcv ⊢ Ⅎ 𝑧 ⟨ 𝐶 , 𝐷 ⟩
10 6 8 9 nfov ⊢ Ⅎ 𝑧 ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 ⟨ 𝐶 , 𝐷 ⟩ )
11 10 nfeq1 ⊢ Ⅎ 𝑧 ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 ⟨ 𝐶 , 𝐷 ⟩ ) = 𝑆
12 2 eqeq2d ⊢ ( ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) ∧ ( 𝑢 = 𝐶 ∧ 𝑓 = 𝐷 ) ) → ( 𝑧 = 𝑅 ↔ 𝑧 = 𝑆 ) )
13 12 copsex4g ⊢ ( ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) ∧ ( 𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻 ) ) → ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ↔ 𝑧 = 𝑆 ) )
14 opelxpi ⊢ ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐻 × 𝐻 ) )
15 opelxpi ⊢ ( ( 𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻 ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐻 × 𝐻 ) )
16 nfcv ⊢ Ⅎ 𝑥 ⟨ 𝐴 , 𝐵 ⟩
17 nfcv ⊢ Ⅎ 𝑦 ⟨ 𝐴 , 𝐵 ⟩
18 nfcv ⊢ Ⅎ 𝑦 ⟨ 𝐶 , 𝐷 ⟩
19 nfv ⊢ Ⅎ 𝑥 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 )
20 nfoprab1 ⊢ Ⅎ 𝑥 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( 𝐻 × 𝐻 ) ∧ 𝑦 ∈ ( 𝐻 × 𝐻 ) ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ) }
21 3 20 nfcxfr ⊢ Ⅎ 𝑥 𝐹
22 nfcv ⊢ Ⅎ 𝑥 𝑦
23 16 21 22 nfov ⊢ Ⅎ 𝑥 ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 𝑦 )
24 23 nfeq1 ⊢ Ⅎ 𝑥 ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 𝑦 ) = 𝑧
25 19 24 nfim ⊢ Ⅎ 𝑥 ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) → ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 𝑦 ) = 𝑧 )
26 nfv ⊢ Ⅎ 𝑦 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 )
27 nfoprab2 ⊢ Ⅎ 𝑦 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( 𝐻 × 𝐻 ) ∧ 𝑦 ∈ ( 𝐻 × 𝐻 ) ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ) }
28 3 27 nfcxfr ⊢ Ⅎ 𝑦 𝐹
29 17 28 18 nfov ⊢ Ⅎ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 ⟨ 𝐶 , 𝐷 ⟩ )
30 29 nfeq1 ⊢ Ⅎ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 ⟨ 𝐶 , 𝐷 ⟩ ) = 𝑧
31 26 30 nfim ⊢ Ⅎ 𝑦 ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) → ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 ⟨ 𝐶 , 𝐷 ⟩ ) = 𝑧 )
32 eqeq1 ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ ) )
33 32 anbi1d ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ) )
34 33 anbi1d ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ) )
35 34 4exbidv ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ↔ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ) )
36 oveq1 ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑥 𝐹 𝑦 ) = ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 𝑦 ) )
37 36 eqeq1d ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( 𝑥 𝐹 𝑦 ) = 𝑧 ↔ ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 𝑦 ) = 𝑧 ) )
38 35 37 imbi12d ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) → ( 𝑥 𝐹 𝑦 ) = 𝑧 ) ↔ ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) → ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 𝑦 ) = 𝑧 ) ) )
39 eqeq1 ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ↔ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑢 , 𝑓 ⟩ ) )
40 39 anbi2d ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑢 , 𝑓 ⟩ ) ) )
41 40 anbi1d ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ) )
42 41 4exbidv ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ↔ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ) )
43 oveq2 ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 𝑦 ) = ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 ⟨ 𝐶 , 𝐷 ⟩ ) )
44 43 eqeq1d ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 𝑦 ) = 𝑧 ↔ ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 ⟨ 𝐶 , 𝐷 ⟩ ) = 𝑧 ) )
45 42 44 imbi12d ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) → ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 𝑦 ) = 𝑧 ) ↔ ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) → ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 ⟨ 𝐶 , 𝐷 ⟩ ) = 𝑧 ) ) )
46 moeq ⊢ ∃* 𝑧 𝑧 = 𝑅
47 46 mosubop ⊢ ∃* 𝑧 ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = 𝑅 )
48 47 mosubop ⊢ ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = 𝑅 ) )
49 anass ⊢ ( ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ↔ ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = 𝑅 ) ) )
50 49 2exbii ⊢ ( ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ↔ ∃ 𝑢 ∃ 𝑓 ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = 𝑅 ) ) )
51 19.42vv ⊢ ( ∃ 𝑢 ∃ 𝑓 ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = 𝑅 ) ) ↔ ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = 𝑅 ) ) )
52 50 51 bitri ⊢ ( ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ↔ ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = 𝑅 ) ) )
53 52 2exbii ⊢ ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ↔ ∃ 𝑤 ∃ 𝑣 ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = 𝑅 ) ) )
54 53 mobii ⊢ ( ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ↔ ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = 𝑅 ) ) )
55 48 54 mpbir ⊢ ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 )
56 55 a1i ⊢ ( ( 𝑥 ∈ ( 𝐻 × 𝐻 ) ∧ 𝑦 ∈ ( 𝐻 × 𝐻 ) ) → ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) )
57 56 3 ovidi ⊢ ( ( 𝑥 ∈ ( 𝐻 × 𝐻 ) ∧ 𝑦 ∈ ( 𝐻 × 𝐻 ) ) → ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) → ( 𝑥 𝐹 𝑦 ) = 𝑧 ) )
58 16 17 18 25 31 38 45 57 vtocl2gaf ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐻 × 𝐻 ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐻 × 𝐻 ) ) → ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) → ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 ⟨ 𝐶 , 𝐷 ⟩ ) = 𝑧 ) )
59 14 15 58 syl2an ⊢ ( ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) ∧ ( 𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻 ) ) → ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) → ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 ⟨ 𝐶 , 𝐷 ⟩ ) = 𝑧 ) )
60 13 59 sylbird ⊢ ( ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) ∧ ( 𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻 ) ) → ( 𝑧 = 𝑆 → ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 ⟨ 𝐶 , 𝐷 ⟩ ) = 𝑧 ) )
61 eqeq2 ⊢ ( 𝑧 = 𝑆 → ( ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 ⟨ 𝐶 , 𝐷 ⟩ ) = 𝑧 ↔ ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 ⟨ 𝐶 , 𝐷 ⟩ ) = 𝑆 ) )
62 60 61 mpbidi ⊢ ( ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) ∧ ( 𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻 ) ) → ( 𝑧 = 𝑆 → ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 ⟨ 𝐶 , 𝐷 ⟩ ) = 𝑆 ) )
63 5 11 62 exlimd ⊢ ( ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) ∧ ( 𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻 ) ) → ( ∃ 𝑧 𝑧 = 𝑆 → ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 ⟨ 𝐶 , 𝐷 ⟩ ) = 𝑆 ) )
64 4 63 mpi ⊢ ( ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) ∧ ( 𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ 𝐹 ⟨ 𝐶 , 𝐷 ⟩ ) = 𝑆 )