Step |
Hyp |
Ref |
Expression |
1 |
|
f1otrkg.p |
⊢ 𝑃 = ( Base ‘ 𝐺 ) |
2 |
|
f1otrkg.d |
⊢ 𝐷 = ( dist ‘ 𝐺 ) |
3 |
|
f1otrkg.i |
⊢ 𝐼 = ( Itv ‘ 𝐺 ) |
4 |
|
f1otrkg.b |
⊢ 𝐵 = ( Base ‘ 𝐻 ) |
5 |
|
f1otrkg.e |
⊢ 𝐸 = ( dist ‘ 𝐻 ) |
6 |
|
f1otrkg.j |
⊢ 𝐽 = ( Itv ‘ 𝐻 ) |
7 |
|
f1otrkg.f |
⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ 𝑃 ) |
8 |
|
f1otrkg.1 |
⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) → ( 𝑒 𝐸 𝑓 ) = ( ( 𝐹 ‘ 𝑒 ) 𝐷 ( 𝐹 ‘ 𝑓 ) ) ) |
9 |
|
f1otrkg.2 |
⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑔 ∈ ( 𝑒 𝐽 𝑓 ) ↔ ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑒 ) 𝐼 ( 𝐹 ‘ 𝑓 ) ) ) ) |
10 |
|
f1otrgitv.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
11 |
|
f1otrgitv.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝐵 ) |
12 |
|
f1otrgitv.z |
⊢ ( 𝜑 → 𝑍 ∈ 𝐵 ) |
13 |
9
|
ralrimivvva |
⊢ ( 𝜑 → ∀ 𝑒 ∈ 𝐵 ∀ 𝑓 ∈ 𝐵 ∀ 𝑔 ∈ 𝐵 ( 𝑔 ∈ ( 𝑒 𝐽 𝑓 ) ↔ ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑒 ) 𝐼 ( 𝐹 ‘ 𝑓 ) ) ) ) |
14 |
|
oveq1 |
⊢ ( 𝑒 = 𝑋 → ( 𝑒 𝐽 𝑓 ) = ( 𝑋 𝐽 𝑓 ) ) |
15 |
14
|
eleq2d |
⊢ ( 𝑒 = 𝑋 → ( 𝑔 ∈ ( 𝑒 𝐽 𝑓 ) ↔ 𝑔 ∈ ( 𝑋 𝐽 𝑓 ) ) ) |
16 |
|
fveq2 |
⊢ ( 𝑒 = 𝑋 → ( 𝐹 ‘ 𝑒 ) = ( 𝐹 ‘ 𝑋 ) ) |
17 |
16
|
oveq1d |
⊢ ( 𝑒 = 𝑋 → ( ( 𝐹 ‘ 𝑒 ) 𝐼 ( 𝐹 ‘ 𝑓 ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝐼 ( 𝐹 ‘ 𝑓 ) ) ) |
18 |
17
|
eleq2d |
⊢ ( 𝑒 = 𝑋 → ( ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑒 ) 𝐼 ( 𝐹 ‘ 𝑓 ) ) ↔ ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐼 ( 𝐹 ‘ 𝑓 ) ) ) ) |
19 |
15 18
|
bibi12d |
⊢ ( 𝑒 = 𝑋 → ( ( 𝑔 ∈ ( 𝑒 𝐽 𝑓 ) ↔ ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑒 ) 𝐼 ( 𝐹 ‘ 𝑓 ) ) ) ↔ ( 𝑔 ∈ ( 𝑋 𝐽 𝑓 ) ↔ ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐼 ( 𝐹 ‘ 𝑓 ) ) ) ) ) |
20 |
|
oveq2 |
⊢ ( 𝑓 = 𝑌 → ( 𝑋 𝐽 𝑓 ) = ( 𝑋 𝐽 𝑌 ) ) |
21 |
20
|
eleq2d |
⊢ ( 𝑓 = 𝑌 → ( 𝑔 ∈ ( 𝑋 𝐽 𝑓 ) ↔ 𝑔 ∈ ( 𝑋 𝐽 𝑌 ) ) ) |
22 |
|
fveq2 |
⊢ ( 𝑓 = 𝑌 → ( 𝐹 ‘ 𝑓 ) = ( 𝐹 ‘ 𝑌 ) ) |
23 |
22
|
oveq2d |
⊢ ( 𝑓 = 𝑌 → ( ( 𝐹 ‘ 𝑋 ) 𝐼 ( 𝐹 ‘ 𝑓 ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝐼 ( 𝐹 ‘ 𝑌 ) ) ) |
24 |
23
|
eleq2d |
⊢ ( 𝑓 = 𝑌 → ( ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐼 ( 𝐹 ‘ 𝑓 ) ) ↔ ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐼 ( 𝐹 ‘ 𝑌 ) ) ) ) |
25 |
21 24
|
bibi12d |
⊢ ( 𝑓 = 𝑌 → ( ( 𝑔 ∈ ( 𝑋 𝐽 𝑓 ) ↔ ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐼 ( 𝐹 ‘ 𝑓 ) ) ) ↔ ( 𝑔 ∈ ( 𝑋 𝐽 𝑌 ) ↔ ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐼 ( 𝐹 ‘ 𝑌 ) ) ) ) ) |
26 |
|
eleq1 |
⊢ ( 𝑔 = 𝑍 → ( 𝑔 ∈ ( 𝑋 𝐽 𝑌 ) ↔ 𝑍 ∈ ( 𝑋 𝐽 𝑌 ) ) ) |
27 |
|
fveq2 |
⊢ ( 𝑔 = 𝑍 → ( 𝐹 ‘ 𝑔 ) = ( 𝐹 ‘ 𝑍 ) ) |
28 |
27
|
eleq1d |
⊢ ( 𝑔 = 𝑍 → ( ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐼 ( 𝐹 ‘ 𝑌 ) ) ↔ ( 𝐹 ‘ 𝑍 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐼 ( 𝐹 ‘ 𝑌 ) ) ) ) |
29 |
26 28
|
bibi12d |
⊢ ( 𝑔 = 𝑍 → ( ( 𝑔 ∈ ( 𝑋 𝐽 𝑌 ) ↔ ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐼 ( 𝐹 ‘ 𝑌 ) ) ) ↔ ( 𝑍 ∈ ( 𝑋 𝐽 𝑌 ) ↔ ( 𝐹 ‘ 𝑍 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐼 ( 𝐹 ‘ 𝑌 ) ) ) ) ) |
30 |
19 25 29
|
rspc3v |
⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ∀ 𝑒 ∈ 𝐵 ∀ 𝑓 ∈ 𝐵 ∀ 𝑔 ∈ 𝐵 ( 𝑔 ∈ ( 𝑒 𝐽 𝑓 ) ↔ ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑒 ) 𝐼 ( 𝐹 ‘ 𝑓 ) ) ) → ( 𝑍 ∈ ( 𝑋 𝐽 𝑌 ) ↔ ( 𝐹 ‘ 𝑍 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐼 ( 𝐹 ‘ 𝑌 ) ) ) ) ) |
31 |
10 11 12 30
|
syl3anc |
⊢ ( 𝜑 → ( ∀ 𝑒 ∈ 𝐵 ∀ 𝑓 ∈ 𝐵 ∀ 𝑔 ∈ 𝐵 ( 𝑔 ∈ ( 𝑒 𝐽 𝑓 ) ↔ ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑒 ) 𝐼 ( 𝐹 ‘ 𝑓 ) ) ) → ( 𝑍 ∈ ( 𝑋 𝐽 𝑌 ) ↔ ( 𝐹 ‘ 𝑍 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐼 ( 𝐹 ‘ 𝑌 ) ) ) ) ) |
32 |
13 31
|
mpd |
⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐽 𝑌 ) ↔ ( 𝐹 ‘ 𝑍 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐼 ( 𝐹 ‘ 𝑌 ) ) ) ) |