Metamath Proof Explorer

Theorem f1otrgitv

Description: Convenient lemma for f1otrg . (Contributed by Thierry Arnoux, 19-Mar-2019)

Ref Expression
Hypotheses f1otrkg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
f1otrkg.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
f1otrkg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
f1otrkg.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
f1otrkg.e ⊢ 𝐸 = ( dist ‘ 𝐻 )
f1otrkg.j ⊢ 𝐽 = ( Itv ‘ 𝐻 )
f1otrkg.f ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ 𝑃 )
f1otrkg.1 ⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) → ( 𝑒 𝐸 𝑓 ) = ( ( 𝐹 ‘ 𝑒 ) 𝐷 ( 𝐹 ‘ 𝑓 ) ) )
f1otrkg.2 ⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑔 ∈ ( 𝑒 𝐽 𝑓 ) ↔ ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑒 ) 𝐼 ( 𝐹 ‘ 𝑓 ) ) ) )
f1otrgitv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
f1otrgitv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
f1otrgitv.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion f1otrgitv ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐽 𝑌 ) ↔ ( 𝐹 ‘ 𝑍 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐼 ( 𝐹 ‘ 𝑌 ) ) ) )

Proof

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 ⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐽 𝑌 ) ↔ ( 𝐹 ‘ 𝑍 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐼 ( 𝐹 ‘ 𝑌 ) ) ) )