Step |
Hyp |
Ref |
Expression |
1 |
|
ofrfvalg.1 |
⊢ ( 𝜑 → 𝐹 Fn 𝐴 ) |
2 |
|
ofrfvalg.2 |
⊢ ( 𝜑 → 𝐺 Fn 𝐵 ) |
3 |
|
ofrfvalg.3 |
⊢ ( 𝜑 → 𝐹 ∈ 𝑉 ) |
4 |
|
ofrfvalg.4 |
⊢ ( 𝜑 → 𝐺 ∈ 𝑊 ) |
5 |
|
ofrfvalg.5 |
⊢ ( 𝐴 ∩ 𝐵 ) = 𝑆 |
6 |
|
ofrfvalg.6 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐶 ) |
7 |
|
ofrfvalg.7 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑥 ) = 𝐷 ) |
8 |
|
dmeq |
⊢ ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 ) |
9 |
|
dmeq |
⊢ ( 𝑔 = 𝐺 → dom 𝑔 = dom 𝐺 ) |
10 |
8 9
|
ineqan12d |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( dom 𝑓 ∩ dom 𝑔 ) = ( dom 𝐹 ∩ dom 𝐺 ) ) |
11 |
|
fveq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) |
12 |
|
fveq1 |
⊢ ( 𝑔 = 𝐺 → ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) |
13 |
11 12
|
breqan12d |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) |
14 |
10 13
|
raleqbidv |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ∀ 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) |
15 |
|
df-ofr |
⊢ ∘r 𝑅 = { 〈 𝑓 , 𝑔 〉 ∣ ∀ 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) } |
16 |
14 15
|
brabga |
⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( 𝐹 ∘r 𝑅 𝐺 ↔ ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) |
17 |
3 4 16
|
syl2anc |
⊢ ( 𝜑 → ( 𝐹 ∘r 𝑅 𝐺 ↔ ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) |
18 |
1
|
fndmd |
⊢ ( 𝜑 → dom 𝐹 = 𝐴 ) |
19 |
2
|
fndmd |
⊢ ( 𝜑 → dom 𝐺 = 𝐵 ) |
20 |
18 19
|
ineq12d |
⊢ ( 𝜑 → ( dom 𝐹 ∩ dom 𝐺 ) = ( 𝐴 ∩ 𝐵 ) ) |
21 |
20 5
|
eqtrdi |
⊢ ( 𝜑 → ( dom 𝐹 ∩ dom 𝐺 ) = 𝑆 ) |
22 |
21
|
raleqdv |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) |
23 |
|
inss1 |
⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 |
24 |
5 23
|
eqsstrri |
⊢ 𝑆 ⊆ 𝐴 |
25 |
24
|
sseli |
⊢ ( 𝑥 ∈ 𝑆 → 𝑥 ∈ 𝐴 ) |
26 |
25 6
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐹 ‘ 𝑥 ) = 𝐶 ) |
27 |
|
inss2 |
⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 |
28 |
5 27
|
eqsstrri |
⊢ 𝑆 ⊆ 𝐵 |
29 |
28
|
sseli |
⊢ ( 𝑥 ∈ 𝑆 → 𝑥 ∈ 𝐵 ) |
30 |
29 7
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑥 ) = 𝐷 ) |
31 |
26 30
|
breq12d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ↔ 𝐶 𝑅 𝐷 ) ) |
32 |
31
|
ralbidva |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 𝐶 𝑅 𝐷 ) ) |
33 |
17 22 32
|
3bitrd |
⊢ ( 𝜑 → ( 𝐹 ∘r 𝑅 𝐺 ↔ ∀ 𝑥 ∈ 𝑆 𝐶 𝑅 𝐷 ) ) |