ovolicc2lem1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ovolicc2lem1		Structured version Visualization version GIF version

Theorem ovolicc2lem1 25266

Description: Lemma for ovolicc2 25271. (Contributed by Mario Carneiro, 14-Jun-2014.)

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

**Assertion**
Ref	Expression
ovolicc2lem1	⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝑃 ∈ 𝑋 ↔ (𝑃 ∈ ℝ ∧ (1^st ‘(𝐹‘(𝐺‘𝑋))) < 𝑃 ∧ 𝑃 < (2^nd ‘(𝐹‘(𝐺‘𝑋))))))

Distinct variable groups: 𝑡,𝐴 𝑡,𝐵 𝑡,𝐹 𝑡,𝐺 𝜑,𝑡 𝑡,𝑈 𝑡,𝑋 Allowed substitution hints: 𝑃(𝑡) 𝑆(𝑡)

**Proof of Theorem ovolicc2lem1**
Step	Hyp	Ref	Expression
1		ovolicc2.5	. . . . . 6 ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
2		inss2 4228	. . . . . 6 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
3		fss 6733	. . . . . 6 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ × ℝ))
4	1, 2, 3	sylancl 584	. . . . 5 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ × ℝ))
5		ovolicc2.8	. . . . . 6 ⊢ (𝜑 → 𝐺:𝑈⟶ℕ)
6	5	ffvelcdmda 7085	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝐺‘𝑋) ∈ ℕ)
7		fvco3 6989	. . . . 5 ⊢ ((𝐹:ℕ⟶(ℝ × ℝ) ∧ (𝐺‘𝑋) ∈ ℕ) → (((,) ∘ 𝐹)‘(𝐺‘𝑋)) = ((,)‘(𝐹‘(𝐺‘𝑋))))
8	4, 6, 7	syl2an2r 681	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑋)) = ((,)‘(𝐹‘(𝐺‘𝑋))))
9		ovolicc2.9	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)
10	9	ralrimiva 3144	. . . . 5 ⊢ (𝜑 → ∀𝑡 ∈ 𝑈 (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)
11		2fveq3 6895	. . . . . . 7 ⊢ (𝑡 = 𝑋 → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = (((,) ∘ 𝐹)‘(𝐺‘𝑋)))
12		id 22	. . . . . . 7 ⊢ (𝑡 = 𝑋 → 𝑡 = 𝑋)
13	11, 12	eqeq12d 2746	. . . . . 6 ⊢ (𝑡 = 𝑋 → ((((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡 ↔ (((,) ∘ 𝐹)‘(𝐺‘𝑋)) = 𝑋))
14	13	rspccva 3610	. . . . 5 ⊢ ((∀𝑡 ∈ 𝑈 (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡 ∧ 𝑋 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑋)) = 𝑋)
15	10, 14	sylan 578	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑋)) = 𝑋)
16	4	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → 𝐹:ℕ⟶(ℝ × ℝ))
17	16, 6	ffvelcdmd 7086	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝐹‘(𝐺‘𝑋)) ∈ (ℝ × ℝ))
18		1st2nd2 8016	. . . . . . 7 ⊢ ((𝐹‘(𝐺‘𝑋)) ∈ (ℝ × ℝ) → (𝐹‘(𝐺‘𝑋)) = ⟨(1^st ‘(𝐹‘(𝐺‘𝑋))), (2^nd ‘(𝐹‘(𝐺‘𝑋)))⟩)
19	17, 18	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝐹‘(𝐺‘𝑋)) = ⟨(1^st ‘(𝐹‘(𝐺‘𝑋))), (2^nd ‘(𝐹‘(𝐺‘𝑋)))⟩)
20	19	fveq2d 6894	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → ((,)‘(𝐹‘(𝐺‘𝑋))) = ((,)‘⟨(1^st ‘(𝐹‘(𝐺‘𝑋))), (2^nd ‘(𝐹‘(𝐺‘𝑋)))⟩))
21		df-ov 7414	. . . . 5 ⊢ ((1^st ‘(𝐹‘(𝐺‘𝑋)))(,)(2^nd ‘(𝐹‘(𝐺‘𝑋)))) = ((,)‘⟨(1^st ‘(𝐹‘(𝐺‘𝑋))), (2^nd ‘(𝐹‘(𝐺‘𝑋)))⟩)
22	20, 21	eqtr4di 2788	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → ((,)‘(𝐹‘(𝐺‘𝑋))) = ((1^st ‘(𝐹‘(𝐺‘𝑋)))(,)(2^nd ‘(𝐹‘(𝐺‘𝑋)))))
23	8, 15, 22	3eqtr3d 2778	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → 𝑋 = ((1^st ‘(𝐹‘(𝐺‘𝑋)))(,)(2^nd ‘(𝐹‘(𝐺‘𝑋)))))
24	23	eleq2d 2817	. 2 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝑃 ∈ 𝑋 ↔ 𝑃 ∈ ((1^st ‘(𝐹‘(𝐺‘𝑋)))(,)(2^nd ‘(𝐹‘(𝐺‘𝑋))))))
25		xp1st 8009	. . . 4 ⊢ ((𝐹‘(𝐺‘𝑋)) ∈ (ℝ × ℝ) → (1^st ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ)
26	17, 25	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (1^st ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ)
27		xp2nd 8010	. . . 4 ⊢ ((𝐹‘(𝐺‘𝑋)) ∈ (ℝ × ℝ) → (2^nd ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ)
28	17, 27	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (2^nd ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ)
29		rexr 11264	. . . 4 ⊢ ((1^st ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ → (1^st ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ^*)
30		rexr 11264	. . . 4 ⊢ ((2^nd ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ → (2^nd ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ^*)
31		elioo2 13369	. . . 4 ⊢ (((1^st ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ^* ∧ (2^nd ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ^*) → (𝑃 ∈ ((1^st ‘(𝐹‘(𝐺‘𝑋)))(,)(2^nd ‘(𝐹‘(𝐺‘𝑋)))) ↔ (𝑃 ∈ ℝ ∧ (1^st ‘(𝐹‘(𝐺‘𝑋))) < 𝑃 ∧ 𝑃 < (2^nd ‘(𝐹‘(𝐺‘𝑋))))))
32	29, 30, 31	syl2an 594	. . 3 ⊢ (((1^st ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ ∧ (2^nd ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ) → (𝑃 ∈ ((1^st ‘(𝐹‘(𝐺‘𝑋)))(,)(2^nd ‘(𝐹‘(𝐺‘𝑋)))) ↔ (𝑃 ∈ ℝ ∧ (1^st ‘(𝐹‘(𝐺‘𝑋))) < 𝑃 ∧ 𝑃 < (2^nd ‘(𝐹‘(𝐺‘𝑋))))))
33	26, 28, 32	syl2anc 582	. 2 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝑃 ∈ ((1^st ‘(𝐹‘(𝐺‘𝑋)))(,)(2^nd ‘(𝐹‘(𝐺‘𝑋)))) ↔ (𝑃 ∈ ℝ ∧ (1^st ‘(𝐹‘(𝐺‘𝑋))) < 𝑃 ∧ 𝑃 < (2^nd ‘(𝐹‘(𝐺‘𝑋))))))
34	24, 33	bitrd 278	1 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝑃 ∈ 𝑋 ↔ (𝑃 ∈ ℝ ∧ (1^st ‘(𝐹‘(𝐺‘𝑋))) < 𝑃 ∧ 𝑃 < (2^nd ‘(𝐹‘(𝐺‘𝑋))))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1085 = wceq 1539 ∈ wcel 2104 ∀wral 3059 ∩ cin 3946 ⊆ wss 3947 𝒫 cpw 4601 ⟨cop 4633 ∪ cuni 4907 class class class wbr 5147 × cxp 5673 ran crn 5676 ∘ ccom 5679 ⟶wf 6538 ‘cfv 6542 (class class class)co 7411 1^st c1st 7975 2^nd c2nd 7976 Fincfn 8941 ℝcr 11111 1c1 11113 + caddc 11115 ℝ^*cxr 11251 < clt 11252 ≤ cle 11253 − cmin 11448 ℕcn 12216 (,)cioo 13328 [,]cicc 13331 seqcseq 13970 abscabs 15185

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-cnex 11168 ax-resscn 11169 ax-pre-lttri 11186 ax-pre-lttrn 11187

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-po 5587 df-so 5588 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-ov 7414 df-oprab 7415 df-mpo 7416 df-1st 7977 df-2nd 7978 df-er 8705 df-en 8942 df-dom 8943 df-sdom 8944 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-ioo 13332

This theorem is referenced by: ovolicc2lem2 25267 ovolicc2lem3 25268 ovolicc2lem4 25269

W3C validator