ovolfcl - Metamath Proof Explorer

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

Theorem ovolfcl 25590

Description: Closure for the interval endpoint function. (Contributed by Mario Carneiro, 16-Mar-2014.)

**Assertion**
Ref	Expression
ovolfcl	⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → ((1^st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑁)) ∈ ℝ ∧ (1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁))))

**Proof of Theorem ovolfcl**
Step	Hyp	Ref	Expression
1		ffvelcdm 7074	. . . . 5 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → (𝐹‘𝑁) ∈ ( ≤ ∩ (ℝ × ℝ)))
2	1	elin2d 4166	. . . 4 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → (𝐹‘𝑁) ∈ (ℝ × ℝ))
3		1st2nd2 8021	. . . 4 ⊢ ((𝐹‘𝑁) ∈ (ℝ × ℝ) → (𝐹‘𝑁) = ⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩)
4	2, 3	syl 18	. . 3 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → (𝐹‘𝑁) = ⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩)
5	4, 1	eqeltrrd 2870	. 2 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → ⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ ( ≤ ∩ (ℝ × ℝ)))
6		ancom 465	. . 3 ⊢ (((1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁)) ∧ ((1^st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑁)) ∈ ℝ)) ↔ (((1^st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑁)) ∈ ℝ) ∧ (1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁))))
7		elin 3929	. . . 4 ⊢ (⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ ( ≤ ∩ (ℝ × ℝ)) ↔ (⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ ≤ ∧ ⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ (ℝ × ℝ)))
8		df-br 5111	. . . . . 6 ⊢ ((1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁)) ↔ ⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ ≤ )
9	8	bicomi 227	. . . . 5 ⊢ (⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ ≤ ↔ (1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁)))
10		opelxp 5695	. . . . 5 ⊢ (⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ (ℝ × ℝ) ↔ ((1^st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑁)) ∈ ℝ))
11	9, 10	anbi12i 639	. . . 4 ⊢ ((⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ ≤ ∧ ⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ (ℝ × ℝ)) ↔ ((1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁)) ∧ ((1^st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑁)) ∈ ℝ)))
12	7, 11	bitri 278	. . 3 ⊢ (⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ ( ≤ ∩ (ℝ × ℝ)) ↔ ((1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁)) ∧ ((1^st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑁)) ∈ ℝ)))
13		df-3an 1103	. . 3 ⊢ (((1^st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑁)) ∈ ℝ ∧ (1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁))) ↔ (((1^st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑁)) ∈ ℝ) ∧ (1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁))))
14	6, 12, 13	3bitr4i 306	. 2 ⊢ (⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ ( ≤ ∩ (ℝ × ℝ)) ↔ ((1^st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑁)) ∈ ℝ ∧ (1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁))))
15	5, 14	sylib 221	1 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → ((1^st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑁)) ∈ ℝ ∧ (1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 ∩ cin 3912 ⟨cop 4597 class class class wbr 5110 × cxp 5657 ⟶wf 6529 ‘cfv 6533 1^st c1st 7980 2^nd c2nd 7981 ℝcr 11095 ≤ cle 11240 ℕcn 12229

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5258 ax-nul 5268 ax-pr 5402 ax-un 7730

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-rab 3424 df-v 3465 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4490 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4874 df-br 5111 df-opab 5175 df-mpt 5194 df-id 5554 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-fv 6541 df-1st 7982 df-2nd 7983

This theorem is referenced by: ovolfioo 25591 ovolficc 25592 ovolfsval 25594 ovolfsf 25595 ovollb2lem 25612 ovolshftlem1 25633 ovolscalem1 25637 ioombl1lem1 25682 ioombl1lem3 25684 ioombl1lem4 25685 ovolfs2 25695 uniiccdif 25702 uniioovol 25703 uniioombllem2a 25706 uniioombllem2 25707 uniioombllem3a 25708 uniioombllem3 25709 uniioombllem4 25710 uniioombllem6 25712 ovolval3 47246

W3C validator