Metamath Proof Explorer

Theorem f1otrgitv

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

Ref Expression
Hypotheses f1otrkg.p ⊢ P = Base G
f1otrkg.d ⊢ D = dist ⁡ G
f1otrkg.i ⊢ I = Itv ⁡ G
f1otrkg.b ⊢ B = Base H
f1otrkg.e ⊢ E = dist ⁡ H
f1otrkg.j ⊢ J = Itv ⁡ H
f1otrkg.f ⊢ φ → F : B ⟶ 1-1 onto P
f1otrkg.1 ⊢ φ ∧ e ∈ B ∧ f ∈ B → e E f = F ⁡ e D F ⁡ f
f1otrkg.2 ⊢ φ ∧ e ∈ B ∧ f ∈ B ∧ g ∈ B → g ∈ e J f ↔ F ⁡ g ∈ F ⁡ e I F ⁡ f
f1otrgitv.x ⊢ φ → X ∈ B
f1otrgitv.y ⊢ φ → Y ∈ B
f1otrgitv.z ⊢ φ → Z ∈ B
Assertion f1otrgitv ⊢ φ → Z ∈ X J Y ↔ F ⁡ Z ∈ F ⁡ X I F ⁡ Y

Proof

Step Hyp Ref Expression
1 f1otrkg.p ⊢ P = Base G
2 f1otrkg.d ⊢ D = dist ⁡ G
3 f1otrkg.i ⊢ I = Itv ⁡ G
4 f1otrkg.b ⊢ B = Base H
5 f1otrkg.e ⊢ E = dist ⁡ H
6 f1otrkg.j ⊢ J = Itv ⁡ H
7 f1otrkg.f ⊢ φ → F : B ⟶ 1-1 onto P
8 f1otrkg.1 ⊢ φ ∧ e ∈ B ∧ f ∈ B → e E f = F ⁡ e D F ⁡ f
9 f1otrkg.2 ⊢ φ ∧ e ∈ B ∧ f ∈ B ∧ g ∈ B → g ∈ e J f ↔ F ⁡ g ∈ F ⁡ e I F ⁡ f
10 f1otrgitv.x ⊢ φ → X ∈ B
11 f1otrgitv.y ⊢ φ → Y ∈ B
12 f1otrgitv.z ⊢ φ → Z ∈ B
13 9 ralrimivvva ⊢ φ → ∀ e ∈ B ∀ f ∈ B ∀ g ∈ B g ∈ e J f ↔ F ⁡ g ∈ F ⁡ e I F ⁡ f
14 oveq1 ⊢ e = X → e J f = X J f
15 14 eleq2d ⊢ e = X → g ∈ e J f ↔ g ∈ X J f
16 fveq2 ⊢ e = X → F ⁡ e = F ⁡ X
17 16 oveq1d ⊢ e = X → F ⁡ e I F ⁡ f = F ⁡ X I F ⁡ f
18 17 eleq2d ⊢ e = X → F ⁡ g ∈ F ⁡ e I F ⁡ f ↔ F ⁡ g ∈ F ⁡ X I F ⁡ f
19 15 18 bibi12d ⊢ e = X → g ∈ e J f ↔ F ⁡ g ∈ F ⁡ e I F ⁡ f ↔ g ∈ X J f ↔ F ⁡ g ∈ F ⁡ X I F ⁡ f
20 oveq2 ⊢ f = Y → X J f = X J Y
21 20 eleq2d ⊢ f = Y → g ∈ X J f ↔ g ∈ X J Y
22 fveq2 ⊢ f = Y → F ⁡ f = F ⁡ Y
23 22 oveq2d ⊢ f = Y → F ⁡ X I F ⁡ f = F ⁡ X I F ⁡ Y
24 23 eleq2d ⊢ f = Y → F ⁡ g ∈ F ⁡ X I F ⁡ f ↔ F ⁡ g ∈ F ⁡ X I F ⁡ Y
25 21 24 bibi12d ⊢ f = Y → g ∈ X J f ↔ F ⁡ g ∈ F ⁡ X I F ⁡ f ↔ g ∈ X J Y ↔ F ⁡ g ∈ F ⁡ X I F ⁡ Y
26 eleq1 ⊢ g = Z → g ∈ X J Y ↔ Z ∈ X J Y
27 fveq2 ⊢ g = Z → F ⁡ g = F ⁡ Z
28 27 eleq1d ⊢ g = Z → F ⁡ g ∈ F ⁡ X I F ⁡ Y ↔ F ⁡ Z ∈ F ⁡ X I F ⁡ Y
29 26 28 bibi12d ⊢ g = Z → g ∈ X J Y ↔ F ⁡ g ∈ F ⁡ X I F ⁡ Y ↔ Z ∈ X J Y ↔ F ⁡ Z ∈ F ⁡ X I F ⁡ Y
30 19 25 29 rspc3v ⊢ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → ∀ e ∈ B ∀ f ∈ B ∀ g ∈ B g ∈ e J f ↔ F ⁡ g ∈ F ⁡ e I F ⁡ f → Z ∈ X J Y ↔ F ⁡ Z ∈ F ⁡ X I F ⁡ Y
31 10 11 12 30 syl3anc ⊢ φ → ∀ e ∈ B ∀ f ∈ B ∀ g ∈ B g ∈ e J f ↔ F ⁡ g ∈ F ⁡ e I F ⁡ f → Z ∈ X J Y ↔ F ⁡ Z ∈ F ⁡ X I F ⁡ Y
32 13 31 mpd ⊢ φ → Z ∈ X J Y ↔ F ⁡ Z ∈ F ⁡ X I F ⁡ Y