ovolicc2lem1

	Ref	Expression
Hypotheses	ovolicc.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	ovolicc.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	ovolicc.3	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
	ovolicc2.4	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
	ovolicc2.5	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
	ovolicc2.6	⊢ ( 𝜑 → 𝑈 ∈ ( 𝒫 ran ( (,) ∘ 𝐹 ) ∩ Fin ) )
	ovolicc2.7	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑈 )
	ovolicc2.8	⊢ ( 𝜑 → 𝐺 : 𝑈 ⟶ ℕ )
	ovolicc2.9	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑈 ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = 𝑡 )
Assertion	ovolicc2lem1	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑃 ∈ 𝑋 ↔ ( 𝑃 ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) < 𝑃 ∧ 𝑃 < ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ovolicc.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		ovolicc.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		ovolicc.3	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
4		ovolicc2.4	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
5		ovolicc2.5	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
6		ovolicc2.6	⊢ ( 𝜑 → 𝑈 ∈ ( 𝒫 ran ( (,) ∘ 𝐹 ) ∩ Fin ) )
7		ovolicc2.7	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑈 )
8		ovolicc2.8	⊢ ( 𝜑 → 𝐺 : 𝑈 ⟶ ℕ )
9		ovolicc2.9	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑈 ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = 𝑡 )
10		inss2	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
11		fss	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ ) ) → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
12	5 10 11	sylancl	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
13	8	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝐺 ‘ 𝑋 ) ∈ ℕ )
14		fvco3	⊢ ( ( 𝐹 : ℕ ⟶ ( ℝ × ℝ ) ∧ ( 𝐺 ‘ 𝑋 ) ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑋 ) ) = ( (,) ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) )
15	12 13 14	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑋 ) ) = ( (,) ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) )
16	9	ralrimiva	⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑈 ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = 𝑡 )
17		2fveq3	⊢ ( 𝑡 = 𝑋 → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑋 ) ) )
18		id	⊢ ( 𝑡 = 𝑋 → 𝑡 = 𝑋 )
19	17 18	eqeq12d	⊢ ( 𝑡 = 𝑋 → ( ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = 𝑡 ↔ ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑋 ) ) = 𝑋 ) )
20	19	rspccva	⊢ ( ( ∀ 𝑡 ∈ 𝑈 ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = 𝑡 ∧ 𝑋 ∈ 𝑈 ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑋 ) ) = 𝑋 )
21	16 20	sylan	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑋 ) ) = 𝑋 )
22	12	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
23	22 13	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( ℝ × ℝ ) )
24		1st2nd2	⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ⟩ )
25	23 24	syl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ⟩ )
26	25	fveq2d	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( (,) ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ⟩ ) )
27		df-ov	⊢ ( ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ⟩ )
28	26 27	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( (,) ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) = ( ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) )
29	15 21 28	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 = ( ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) )
30	29	eleq2d	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑃 ∈ 𝑋 ↔ 𝑃 ∈ ( ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) ) )
31		xp1st	⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ )
32	23 31	syl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ )
33		xp2nd	⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( ℝ × ℝ ) → ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ )
34	23 33	syl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ )
35		rexr	⊢ ( ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ → ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ^* )
36		rexr	⊢ ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ → ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ^* )
37		elioo2	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ^* ∧ ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ^* ) → ( 𝑃 ∈ ( ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) ↔ ( 𝑃 ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) < 𝑃 ∧ 𝑃 < ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) ) )
38	35 36 37	syl2an	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ ℝ ) → ( 𝑃 ∈ ( ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) ↔ ( 𝑃 ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) < 𝑃 ∧ 𝑃 < ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) ) )
39	32 34 38	syl2anc	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑃 ∈ ( ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) ↔ ( 𝑃 ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) < 𝑃 ∧ 𝑃 < ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) ) )
40	30 39	bitrd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑃 ∈ 𝑋 ↔ ( 𝑃 ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) < 𝑃 ∧ 𝑃 < ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ) ) ) )

Metamath Proof Explorer

Theorem ovolicc2lem1

Proof