Step |
Hyp |
Ref |
Expression |
1 |
|
ovg.1 |
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) |
2 |
|
ovg.2 |
⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) |
3 |
|
ovg.3 |
⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) ) |
4 |
|
ovg.4 |
⊢ ( ( 𝜏 ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ) → ∃! 𝑧 𝜑 ) |
5 |
|
ovg.5 |
⊢ 𝐹 = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } |
6 |
|
df-ov |
⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ 〈 𝐴 , 𝐵 〉 ) |
7 |
5
|
fveq1i |
⊢ ( 𝐹 ‘ 〈 𝐴 , 𝐵 〉 ) = ( { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ 〈 𝐴 , 𝐵 〉 ) |
8 |
6 7
|
eqtri |
⊢ ( 𝐴 𝐹 𝐵 ) = ( { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ 〈 𝐴 , 𝐵 〉 ) |
9 |
8
|
eqeq1i |
⊢ ( ( 𝐴 𝐹 𝐵 ) = 𝐶 ↔ ( { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ 〈 𝐴 , 𝐵 〉 ) = 𝐶 ) |
10 |
|
eqeq2 |
⊢ ( 𝑐 = 𝐶 → ( ( { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ 〈 𝐴 , 𝐵 〉 ) = 𝑐 ↔ ( { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ 〈 𝐴 , 𝐵 〉 ) = 𝐶 ) ) |
11 |
|
opeq2 |
⊢ ( 𝑐 = 𝐶 → 〈 〈 𝐴 , 𝐵 〉 , 𝑐 〉 = 〈 〈 𝐴 , 𝐵 〉 , 𝐶 〉 ) |
12 |
11
|
eleq1d |
⊢ ( 𝑐 = 𝐶 → ( 〈 〈 𝐴 , 𝐵 〉 , 𝑐 〉 ∈ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ↔ 〈 〈 𝐴 , 𝐵 〉 , 𝐶 〉 ∈ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) ) |
13 |
10 12
|
bibi12d |
⊢ ( 𝑐 = 𝐶 → ( ( ( { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ 〈 𝐴 , 𝐵 〉 ) = 𝑐 ↔ 〈 〈 𝐴 , 𝐵 〉 , 𝑐 〉 ∈ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) ↔ ( ( { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ 〈 𝐴 , 𝐵 〉 ) = 𝐶 ↔ 〈 〈 𝐴 , 𝐵 〉 , 𝐶 〉 ∈ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) ) ) |
14 |
13
|
imbi2d |
⊢ ( 𝑐 = 𝐶 → ( ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ( ( { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ 〈 𝐴 , 𝐵 〉 ) = 𝑐 ↔ 〈 〈 𝐴 , 𝐵 〉 , 𝑐 〉 ∈ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) ) ↔ ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ( ( { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ 〈 𝐴 , 𝐵 〉 ) = 𝐶 ↔ 〈 〈 𝐴 , 𝐵 〉 , 𝐶 〉 ∈ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) ) ) ) |
15 |
4
|
ex |
⊢ ( 𝜏 → ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ∃! 𝑧 𝜑 ) ) |
16 |
15
|
alrimivv |
⊢ ( 𝜏 → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ∃! 𝑧 𝜑 ) ) |
17 |
|
fnoprabg |
⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ∃! 𝑧 𝜑 ) → { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } Fn { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } ) |
18 |
16 17
|
syl |
⊢ ( 𝜏 → { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } Fn { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } ) |
19 |
|
eleq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝑅 ↔ 𝐴 ∈ 𝑅 ) ) |
20 |
19
|
anbi1d |
⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ↔ ( 𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ) ) |
21 |
|
eleq1 |
⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝑆 ↔ 𝐵 ∈ 𝑆 ) ) |
22 |
21
|
anbi2d |
⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ↔ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) ) |
23 |
20 22
|
opelopabg |
⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } ↔ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) ) |
24 |
23
|
ibir |
⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } ) |
25 |
|
fnopfvb |
⊢ ( ( { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } Fn { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } ∧ 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } ) → ( ( { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ 〈 𝐴 , 𝐵 〉 ) = 𝑐 ↔ 〈 〈 𝐴 , 𝐵 〉 , 𝑐 〉 ∈ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) ) |
26 |
18 24 25
|
syl2an |
⊢ ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ( ( { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ 〈 𝐴 , 𝐵 〉 ) = 𝑐 ↔ 〈 〈 𝐴 , 𝐵 〉 , 𝑐 〉 ∈ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) ) |
27 |
14 26
|
vtoclg |
⊢ ( 𝐶 ∈ 𝐷 → ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ( ( { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ 〈 𝐴 , 𝐵 〉 ) = 𝐶 ↔ 〈 〈 𝐴 , 𝐵 〉 , 𝐶 〉 ∈ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) ) ) |
28 |
27
|
com12 |
⊢ ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝐶 ∈ 𝐷 → ( ( { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ 〈 𝐴 , 𝐵 〉 ) = 𝐶 ↔ 〈 〈 𝐴 , 𝐵 〉 , 𝐶 〉 ∈ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) ) ) |
29 |
28
|
exp32 |
⊢ ( 𝜏 → ( 𝐴 ∈ 𝑅 → ( 𝐵 ∈ 𝑆 → ( 𝐶 ∈ 𝐷 → ( ( { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ 〈 𝐴 , 𝐵 〉 ) = 𝐶 ↔ 〈 〈 𝐴 , 𝐵 〉 , 𝐶 〉 ∈ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) ) ) ) ) |
30 |
29
|
3imp2 |
⊢ ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷 ) ) → ( ( { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ 〈 𝐴 , 𝐵 〉 ) = 𝐶 ↔ 〈 〈 𝐴 , 𝐵 〉 , 𝐶 〉 ∈ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) ) |
31 |
20 1
|
anbi12d |
⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜓 ) ) ) |
32 |
22 2
|
anbi12d |
⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜓 ) ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜒 ) ) ) |
33 |
3
|
anbi2d |
⊢ ( 𝑧 = 𝐶 → ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜒 ) ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ) ) |
34 |
31 32 33
|
eloprabg |
⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷 ) → ( 〈 〈 𝐴 , 𝐵 〉 , 𝐶 〉 ∈ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ) ) |
35 |
34
|
adantl |
⊢ ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷 ) ) → ( 〈 〈 𝐴 , 𝐵 〉 , 𝐶 〉 ∈ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ) ) |
36 |
30 35
|
bitrd |
⊢ ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷 ) ) → ( ( { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ 〈 𝐴 , 𝐵 〉 ) = 𝐶 ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ) ) |
37 |
9 36
|
syl5bb |
⊢ ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷 ) ) → ( ( 𝐴 𝐹 𝐵 ) = 𝐶 ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ) ) |
38 |
|
biidd |
⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ) ) |
39 |
38
|
bianabs |
⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ↔ 𝜃 ) ) |
40 |
39
|
3adant3 |
⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷 ) → ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ↔ 𝜃 ) ) |
41 |
40
|
adantl |
⊢ ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷 ) ) → ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ↔ 𝜃 ) ) |
42 |
37 41
|
bitrd |
⊢ ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷 ) ) → ( ( 𝐴 𝐹 𝐵 ) = 𝐶 ↔ 𝜃 ) ) |