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