Proof of Theorem ovolicc2lem1
Step | Hyp | Ref
| Expression |
1 | | ovolicc2.8 |
. . . . . 6
⊢ (𝜑 → 𝐺:𝑈⟶ℕ) |
2 | 1 | ffvelrnda 6359 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝐺‘𝑋) ∈ ℕ) |
3 | | ovolicc2.5 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
4 | | inss2 3834 |
. . . . . . 7
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
5 | | fss 6056 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
6 | 3, 4, 5 | sylancl 694 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
7 | | fvco3 6275 |
. . . . . 6
⊢ ((𝐹:ℕ⟶(ℝ ×
ℝ) ∧ (𝐺‘𝑋) ∈ ℕ) → (((,) ∘ 𝐹)‘(𝐺‘𝑋)) = ((,)‘(𝐹‘(𝐺‘𝑋)))) |
8 | 6, 7 | sylan 488 |
. . . . 5
⊢ ((𝜑 ∧ (𝐺‘𝑋) ∈ ℕ) → (((,) ∘ 𝐹)‘(𝐺‘𝑋)) = ((,)‘(𝐹‘(𝐺‘𝑋)))) |
9 | 2, 8 | syldan 487 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑋)) = ((,)‘(𝐹‘(𝐺‘𝑋)))) |
10 | | ovolicc2.9 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) |
11 | 10 | ralrimiva 2966 |
. . . . 5
⊢ (𝜑 → ∀𝑡 ∈ 𝑈 (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) |
12 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑡 = 𝑋 → (𝐺‘𝑡) = (𝐺‘𝑋)) |
13 | 12 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑡 = 𝑋 → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = (((,) ∘ 𝐹)‘(𝐺‘𝑋))) |
14 | | id 22 |
. . . . . . 7
⊢ (𝑡 = 𝑋 → 𝑡 = 𝑋) |
15 | 13, 14 | eqeq12d 2637 |
. . . . . 6
⊢ (𝑡 = 𝑋 → ((((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡 ↔ (((,) ∘ 𝐹)‘(𝐺‘𝑋)) = 𝑋)) |
16 | 15 | rspccva 3308 |
. . . . 5
⊢
((∀𝑡 ∈
𝑈 (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡 ∧ 𝑋 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑋)) = 𝑋) |
17 | 11, 16 | sylan 488 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑋)) = 𝑋) |
18 | 6 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
19 | 18, 2 | ffvelrnd 6360 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝐹‘(𝐺‘𝑋)) ∈ (ℝ ×
ℝ)) |
20 | | 1st2nd2 7205 |
. . . . . . 7
⊢ ((𝐹‘(𝐺‘𝑋)) ∈ (ℝ × ℝ) →
(𝐹‘(𝐺‘𝑋)) = 〈(1st ‘(𝐹‘(𝐺‘𝑋))), (2nd ‘(𝐹‘(𝐺‘𝑋)))〉) |
21 | 19, 20 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝐹‘(𝐺‘𝑋)) = 〈(1st ‘(𝐹‘(𝐺‘𝑋))), (2nd ‘(𝐹‘(𝐺‘𝑋)))〉) |
22 | 21 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → ((,)‘(𝐹‘(𝐺‘𝑋))) = ((,)‘〈(1st
‘(𝐹‘(𝐺‘𝑋))), (2nd ‘(𝐹‘(𝐺‘𝑋)))〉)) |
23 | | df-ov 6653 |
. . . . 5
⊢
((1st ‘(𝐹‘(𝐺‘𝑋)))(,)(2nd ‘(𝐹‘(𝐺‘𝑋)))) = ((,)‘〈(1st
‘(𝐹‘(𝐺‘𝑋))), (2nd ‘(𝐹‘(𝐺‘𝑋)))〉) |
24 | 22, 23 | syl6eqr 2674 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → ((,)‘(𝐹‘(𝐺‘𝑋))) = ((1st ‘(𝐹‘(𝐺‘𝑋)))(,)(2nd ‘(𝐹‘(𝐺‘𝑋))))) |
25 | 9, 17, 24 | 3eqtr3d 2664 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → 𝑋 = ((1st ‘(𝐹‘(𝐺‘𝑋)))(,)(2nd ‘(𝐹‘(𝐺‘𝑋))))) |
26 | 25 | eleq2d 2687 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝑃 ∈ 𝑋 ↔ 𝑃 ∈ ((1st ‘(𝐹‘(𝐺‘𝑋)))(,)(2nd ‘(𝐹‘(𝐺‘𝑋)))))) |
27 | | xp1st 7198 |
. . . 4
⊢ ((𝐹‘(𝐺‘𝑋)) ∈ (ℝ × ℝ) →
(1st ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ) |
28 | 19, 27 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (1st ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ) |
29 | | xp2nd 7199 |
. . . 4
⊢ ((𝐹‘(𝐺‘𝑋)) ∈ (ℝ × ℝ) →
(2nd ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ) |
30 | 19, 29 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (2nd ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ) |
31 | | rexr 10085 |
. . . 4
⊢
((1st ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ → (1st
‘(𝐹‘(𝐺‘𝑋))) ∈
ℝ*) |
32 | | rexr 10085 |
. . . 4
⊢
((2nd ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ → (2nd
‘(𝐹‘(𝐺‘𝑋))) ∈
ℝ*) |
33 | | elioo2 12216 |
. . . 4
⊢
(((1st ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ* ∧
(2nd ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ*) →
(𝑃 ∈ ((1st
‘(𝐹‘(𝐺‘𝑋)))(,)(2nd ‘(𝐹‘(𝐺‘𝑋)))) ↔ (𝑃 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘𝑋))) < 𝑃 ∧ 𝑃 < (2nd ‘(𝐹‘(𝐺‘𝑋)))))) |
34 | 31, 32, 33 | syl2an 494 |
. . 3
⊢
(((1st ‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ ∧ (2nd
‘(𝐹‘(𝐺‘𝑋))) ∈ ℝ) → (𝑃 ∈ ((1st
‘(𝐹‘(𝐺‘𝑋)))(,)(2nd ‘(𝐹‘(𝐺‘𝑋)))) ↔ (𝑃 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘𝑋))) < 𝑃 ∧ 𝑃 < (2nd ‘(𝐹‘(𝐺‘𝑋)))))) |
35 | 28, 30, 34 | syl2anc 693 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝑃 ∈ ((1st ‘(𝐹‘(𝐺‘𝑋)))(,)(2nd ‘(𝐹‘(𝐺‘𝑋)))) ↔ (𝑃 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘𝑋))) < 𝑃 ∧ 𝑃 < (2nd ‘(𝐹‘(𝐺‘𝑋)))))) |
36 | 26, 35 | bitrd 268 |
1
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝑃 ∈ 𝑋 ↔ (𝑃 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘𝑋))) < 𝑃 ∧ 𝑃 < (2nd ‘(𝐹‘(𝐺‘𝑋)))))) |