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