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 24535

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		ffvelrn 6941	. . . . 5 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → (𝐹‘𝑁) ∈ ( ≤ ∩ (ℝ × ℝ)))
2	1	elin2d 4129	. . . 4 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → (𝐹‘𝑁) ∈ (ℝ × ℝ))
3		1st2nd2 7843	. . . 4 ⊢ ((𝐹‘𝑁) ∈ (ℝ × ℝ) → (𝐹‘𝑁) = ⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩)
4	2, 3	syl 17	. . 3 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → (𝐹‘𝑁) = ⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩)
5	4, 1	eqeltrrd 2840	. 2 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → ⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ ( ≤ ∩ (ℝ × ℝ)))
6		ancom 460	. . 3 ⊢ (((1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁)) ∧ ((1^st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑁)) ∈ ℝ)) ↔ (((1^st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑁)) ∈ ℝ) ∧ (1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁))))
7		elin 3899	. . . 4 ⊢ (⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ ( ≤ ∩ (ℝ × ℝ)) ↔ (⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ ≤ ∧ ⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ (ℝ × ℝ)))
8		df-br 5071	. . . . . 6 ⊢ ((1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁)) ↔ ⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ ≤ )
9	8	bicomi 223	. . . . 5 ⊢ (⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ ≤ ↔ (1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁)))
10		opelxp 5616	. . . . 5 ⊢ (⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ (ℝ × ℝ) ↔ ((1^st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑁)) ∈ ℝ))
11	9, 10	anbi12i 626	. . . 4 ⊢ ((⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ ≤ ∧ ⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ (ℝ × ℝ)) ↔ ((1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁)) ∧ ((1^st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑁)) ∈ ℝ)))
12	7, 11	bitri 274	. . 3 ⊢ (⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ ( ≤ ∩ (ℝ × ℝ)) ↔ ((1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁)) ∧ ((1^st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑁)) ∈ ℝ)))
13		df-3an 1087	. . 3 ⊢ (((1^st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑁)) ∈ ℝ ∧ (1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁))) ↔ (((1^st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑁)) ∈ ℝ) ∧ (1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁))))
14	6, 12, 13	3bitr4i 302	. 2 ⊢ (⟨(1^st ‘(𝐹‘𝑁)), (2^nd ‘(𝐹‘𝑁))⟩ ∈ ( ≤ ∩ (ℝ × ℝ)) ↔ ((1^st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑁)) ∈ ℝ ∧ (1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁))))
15	5, 14	sylib 217	1 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → ((1^st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑁)) ∈ ℝ ∧ (1^st ‘(𝐹‘𝑁)) ≤ (2^nd ‘(𝐹‘𝑁))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ∩ cin 3882 ⟨cop 4564 class class class wbr 5070 × cxp 5578 ⟶wf 6414 ‘cfv 6418 1^st c1st 7802 2^nd c2nd 7803 ℝcr 10801 ≤ cle 10941 ℕcn 11903

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pr 5347 ax-un 7566

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-fv 6426 df-1st 7804 df-2nd 7805

This theorem is referenced by: ovolfioo 24536 ovolficc 24537 ovolfsval 24539 ovolfsf 24540 ovollb2lem 24557 ovolshftlem1 24578 ovolscalem1 24582 ioombl1lem1 24627 ioombl1lem3 24629 ioombl1lem4 24630 ovolfs2 24640 uniiccdif 24647 uniioovol 24648 uniioombllem2a 24651 uniioombllem2 24652 uniioombllem3a 24653 uniioombllem3 24654 uniioombllem4 24655 uniioombllem6 24657 ovolval3 44075

W3C validator