Metamath Proof Explorer

Theorem opnvonmbllem1

Description: The half-open interval expressed using a composition of a function (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses opnvonmbllem1.i ⊢ Ⅎ 𝑖 𝜑
opnvonmbllem1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
opnvonmbllem1.c ⊢ ( 𝜑 → 𝐶 : 𝑋 ⟶ ℚ )
opnvonmbllem1.d ⊢ ( 𝜑 → 𝐷 : 𝑋 ⟶ ℚ )
opnvonmbllem1.s ⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ⊆ 𝐵 )
opnvonmbllem1.g ⊢ ( 𝜑 → 𝐵 ⊆ 𝐺 )
opnvonmbllem1.y ⊢ ( 𝜑 → 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) )
opnvonmbllem1.k ⊢ 𝐾 = { ℎ ∈ ( ( ℚ × ℚ ) ↑m 𝑋 ) ∣ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ℎ ) ‘ 𝑖 ) ⊆ 𝐺 }
opnvonmbllem1.h ⊢ 𝐻 = ( 𝑖 ∈ 𝑋 ↦ ⟨ ( 𝐶 ‘ 𝑖 ) , ( 𝐷 ‘ 𝑖 ) ⟩ )
Assertion opnvonmbllem1 ( 𝜑 → ∃ ℎ ∈ 𝐾 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ℎ ) ‘ 𝑖 ) )

Proof

Step Hyp Ref Expression
1 opnvonmbllem1.i ⊢ Ⅎ 𝑖 𝜑
2 opnvonmbllem1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
3 opnvonmbllem1.c ⊢ ( 𝜑 → 𝐶 : 𝑋 ⟶ ℚ )
4 opnvonmbllem1.d ⊢ ( 𝜑 → 𝐷 : 𝑋 ⟶ ℚ )
5 opnvonmbllem1.s ⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ⊆ 𝐵 )
6 opnvonmbllem1.g ⊢ ( 𝜑 → 𝐵 ⊆ 𝐺 )
7 opnvonmbllem1.y ⊢ ( 𝜑 → 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) )
8 opnvonmbllem1.k ⊢ 𝐾 = { ℎ ∈ ( ( ℚ × ℚ ) ↑m 𝑋 ) ∣ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ℎ ) ‘ 𝑖 ) ⊆ 𝐺 }
9 opnvonmbllem1.h ⊢ 𝐻 = ( 𝑖 ∈ 𝑋 ↦ ⟨ ( 𝐶 ‘ 𝑖 ) , ( 𝐷 ‘ 𝑖 ) ⟩ )
10 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑖 ) ∈ ℚ )
11 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐷 ‘ 𝑖 ) ∈ ℚ )
12 opelxpi ⊢ ( ( ( 𝐶 ‘ 𝑖 ) ∈ ℚ ∧ ( 𝐷 ‘ 𝑖 ) ∈ ℚ ) → ⟨ ( 𝐶 ‘ 𝑖 ) , ( 𝐷 ‘ 𝑖 ) ⟩ ∈ ( ℚ × ℚ ) )
13 10 11 12 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ⟨ ( 𝐶 ‘ 𝑖 ) , ( 𝐷 ‘ 𝑖 ) ⟩ ∈ ( ℚ × ℚ ) )
14 1 13 9 fmptdf ⊢ ( 𝜑 → 𝐻 : 𝑋 ⟶ ( ℚ × ℚ ) )
15 qex ⊢ ℚ ∈ V
16 15 15 xpex ⊢ ( ℚ × ℚ ) ∈ V
17 16 a1i ⊢ ( 𝜑 → ( ℚ × ℚ ) ∈ V )
18 17 2 jca ⊢ ( 𝜑 → ( ( ℚ × ℚ ) ∈ V ∧ 𝑋 ∈ 𝑉 ) )
19 elmapg ⊢ ( ( ( ℚ × ℚ ) ∈ V ∧ 𝑋 ∈ 𝑉 ) → ( 𝐻 ∈ ( ( ℚ × ℚ ) ↑m 𝑋 ) ↔ 𝐻 : 𝑋 ⟶ ( ℚ × ℚ ) ) )
20 18 19 syl ⊢ ( 𝜑 → ( 𝐻 ∈ ( ( ℚ × ℚ ) ↑m 𝑋 ) ↔ 𝐻 : 𝑋 ⟶ ( ℚ × ℚ ) ) )
21 14 20 mpbird ⊢ ( 𝜑 → 𝐻 ∈ ( ( ℚ × ℚ ) ↑m 𝑋 ) )
22 1 9 hoi2toco ⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( [,) ∘ 𝐻 ) ‘ 𝑖 ) = X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) )
23 5 6 sstrd ⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ⊆ 𝐺 )
24 22 23 eqsstrd ⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( [,) ∘ 𝐻 ) ‘ 𝑖 ) ⊆ 𝐺 )
25 21 24 jca ⊢ ( 𝜑 → ( 𝐻 ∈ ( ( ℚ × ℚ ) ↑m 𝑋 ) ∧ X 𝑖 ∈ 𝑋 ( ( [,) ∘ 𝐻 ) ‘ 𝑖 ) ⊆ 𝐺 ) )
26 nfcv ⊢ Ⅎ 𝑖 ℎ
27 nfmpt1 ⊢ Ⅎ 𝑖 ( 𝑖 ∈ 𝑋 ↦ ⟨ ( 𝐶 ‘ 𝑖 ) , ( 𝐷 ‘ 𝑖 ) ⟩ )
28 9 27 nfcxfr ⊢ Ⅎ 𝑖 𝐻
29 26 28 nfeq ⊢ Ⅎ 𝑖 ℎ = 𝐻
30 coeq2 ⊢ ( ℎ = 𝐻 → ( [,) ∘ ℎ ) = ( [,) ∘ 𝐻 ) )
31 30 fveq1d ⊢ ( ℎ = 𝐻 → ( ( [,) ∘ ℎ ) ‘ 𝑖 ) = ( ( [,) ∘ 𝐻 ) ‘ 𝑖 ) )
32 31 adantr ⊢ ( ( ℎ = 𝐻 ∧ 𝑖 ∈ 𝑋 ) → ( ( [,) ∘ ℎ ) ‘ 𝑖 ) = ( ( [,) ∘ 𝐻 ) ‘ 𝑖 ) )
33 29 32 ixpeq2d ⊢ ( ℎ = 𝐻 → X 𝑖 ∈ 𝑋 ( ( [,) ∘ ℎ ) ‘ 𝑖 ) = X 𝑖 ∈ 𝑋 ( ( [,) ∘ 𝐻 ) ‘ 𝑖 ) )
34 33 sseq1d ⊢ ( ℎ = 𝐻 → ( X 𝑖 ∈ 𝑋 ( ( [,) ∘ ℎ ) ‘ 𝑖 ) ⊆ 𝐺 ↔ X 𝑖 ∈ 𝑋 ( ( [,) ∘ 𝐻 ) ‘ 𝑖 ) ⊆ 𝐺 ) )
35 34 8 elrab2 ⊢ ( 𝐻 ∈ 𝐾 ↔ ( 𝐻 ∈ ( ( ℚ × ℚ ) ↑m 𝑋 ) ∧ X 𝑖 ∈ 𝑋 ( ( [,) ∘ 𝐻 ) ‘ 𝑖 ) ⊆ 𝐺 ) )
36 25 35 sylibr ⊢ ( 𝜑 → 𝐻 ∈ 𝐾 )
37 7 22 eleqtrrd ⊢ ( 𝜑 → 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( [,) ∘ 𝐻 ) ‘ 𝑖 ) )
38 nfv ⊢ Ⅎ ℎ 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( [,) ∘ 𝐻 ) ‘ 𝑖 )
39 nfcv ⊢ Ⅎ ℎ 𝐻
40 nfrab1 ⊢ Ⅎ ℎ { ℎ ∈ ( ( ℚ × ℚ ) ↑m 𝑋 ) ∣ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ℎ ) ‘ 𝑖 ) ⊆ 𝐺 }
41 8 40 nfcxfr ⊢ Ⅎ ℎ 𝐾
42 33 eleq2d ⊢ ( ℎ = 𝐻 → ( 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ℎ ) ‘ 𝑖 ) ↔ 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( [,) ∘ 𝐻 ) ‘ 𝑖 ) ) )
43 38 39 41 42 rspcef ⊢ ( ( 𝐻 ∈ 𝐾 ∧ 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( [,) ∘ 𝐻 ) ‘ 𝑖 ) ) → ∃ ℎ ∈ 𝐾 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ℎ ) ‘ 𝑖 ) )
44 36 37 43 syl2anc ⊢ ( 𝜑 → ∃ ℎ ∈ 𝐾 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ℎ ) ‘ 𝑖 ) )