Proof of Theorem caucvgsrlemfv
Step | Hyp | Ref
| Expression |
1 | | caucvgsrlemf.xfr |
. . . . . . 7
⊢ 𝐺 = (𝑥 ∈ N ↦
(℩𝑦 ∈
P (𝐹‘𝑥) = [〈(𝑦 +P
1P), 1P〉]
~R )) |
2 | 1 | a1i 9 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ N) → 𝐺 = (𝑥 ∈ N ↦
(℩𝑦 ∈
P (𝐹‘𝑥) = [〈(𝑦 +P
1P), 1P〉]
~R ))) |
3 | | fveq2 5496 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) |
4 | 3 | eqeq1d 2179 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = [〈(𝑦 +P
1P), 1P〉]
~R ↔ (𝐹‘𝐴) = [〈(𝑦 +P
1P), 1P〉]
~R )) |
5 | 4 | riotabidv 5811 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (℩𝑦 ∈ P (𝐹‘𝑥) = [〈(𝑦 +P
1P), 1P〉]
~R ) = (℩𝑦 ∈ P (𝐹‘𝐴) = [〈(𝑦 +P
1P), 1P〉]
~R )) |
6 | 5 | adantl 275 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ N) ∧ 𝑥 = 𝐴) → (℩𝑦 ∈ P (𝐹‘𝑥) = [〈(𝑦 +P
1P), 1P〉]
~R ) = (℩𝑦 ∈ P (𝐹‘𝐴) = [〈(𝑦 +P
1P), 1P〉]
~R )) |
7 | | simpr 109 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ N) → 𝐴 ∈
N) |
8 | | caucvgsr.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:N⟶R) |
9 | | caucvgsrlemgt1.gt1 |
. . . . . . 7
⊢ (𝜑 → ∀𝑚 ∈ N
1R <R (𝐹‘𝑚)) |
10 | 8, 9 | caucvgsrlemcl 7751 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ N) →
(℩𝑦 ∈
P (𝐹‘𝐴) = [〈(𝑦 +P
1P), 1P〉]
~R ) ∈ P) |
11 | 2, 6, 7, 10 | fvmptd 5577 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ N) → (𝐺‘𝐴) = (℩𝑦 ∈ P (𝐹‘𝐴) = [〈(𝑦 +P
1P), 1P〉]
~R )) |
12 | 11 | oveq1d 5868 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ N) → ((𝐺‘𝐴) +P
1P) = ((℩𝑦 ∈ P (𝐹‘𝐴) = [〈(𝑦 +P
1P), 1P〉]
~R ) +P
1P)) |
13 | 12 | opeq1d 3771 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ N) →
〈((𝐺‘𝐴) +P
1P), 1P〉 =
〈((℩𝑦
∈ P (𝐹‘𝐴) = [〈(𝑦 +P
1P), 1P〉]
~R ) +P
1P),
1P〉) |
14 | 13 | eceq1d 6549 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ N) →
[〈((𝐺‘𝐴) +P
1P), 1P〉]
~R = [〈((℩𝑦 ∈ P (𝐹‘𝐴) = [〈(𝑦 +P
1P), 1P〉]
~R ) +P
1P), 1P〉]
~R ) |
15 | | eqcom 2172 |
. . . . . . 7
⊢ ((𝐹‘𝐴) = [〈(𝑦 +P
1P), 1P〉]
~R ↔ [〈(𝑦 +P
1P), 1P〉]
~R = (𝐹‘𝐴)) |
16 | 15 | a1i 9 |
. . . . . 6
⊢ (𝑦 ∈ P →
((𝐹‘𝐴) = [〈(𝑦 +P
1P), 1P〉]
~R ↔ [〈(𝑦 +P
1P), 1P〉]
~R = (𝐹‘𝐴))) |
17 | 16 | riotabiia 5826 |
. . . . 5
⊢
(℩𝑦
∈ P (𝐹‘𝐴) = [〈(𝑦 +P
1P), 1P〉]
~R ) = (℩𝑦 ∈ P [〈(𝑦 +P
1P), 1P〉]
~R = (𝐹‘𝐴)) |
18 | 17 | oveq1i 5863 |
. . . 4
⊢
((℩𝑦
∈ P (𝐹‘𝐴) = [〈(𝑦 +P
1P), 1P〉]
~R ) +P
1P) = ((℩𝑦 ∈ P [〈(𝑦 +P
1P), 1P〉]
~R = (𝐹‘𝐴)) +P
1P) |
19 | 18 | opeq1i 3768 |
. . 3
⊢
〈((℩𝑦 ∈ P (𝐹‘𝐴) = [〈(𝑦 +P
1P), 1P〉]
~R ) +P
1P), 1P〉 =
〈((℩𝑦
∈ P [〈(𝑦 +P
1P), 1P〉]
~R = (𝐹‘𝐴)) +P
1P),
1P〉 |
20 | | eceq1 6548 |
. . 3
⊢
(〈((℩𝑦 ∈ P (𝐹‘𝐴) = [〈(𝑦 +P
1P), 1P〉]
~R ) +P
1P), 1P〉 =
〈((℩𝑦
∈ P [〈(𝑦 +P
1P), 1P〉]
~R = (𝐹‘𝐴)) +P
1P), 1P〉 →
[〈((℩𝑦
∈ P (𝐹‘𝐴) = [〈(𝑦 +P
1P), 1P〉]
~R ) +P
1P), 1P〉]
~R = [〈((℩𝑦 ∈ P [〈(𝑦 +P
1P), 1P〉]
~R = (𝐹‘𝐴)) +P
1P), 1P〉]
~R ) |
21 | 19, 20 | mp1i 10 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ N) →
[〈((℩𝑦
∈ P (𝐹‘𝐴) = [〈(𝑦 +P
1P), 1P〉]
~R ) +P
1P), 1P〉]
~R = [〈((℩𝑦 ∈ P [〈(𝑦 +P
1P), 1P〉]
~R = (𝐹‘𝐴)) +P
1P), 1P〉]
~R ) |
22 | 8 | ffvelrnda 5631 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ N) → (𝐹‘𝐴) ∈ R) |
23 | | 0lt1sr 7727 |
. . . 4
⊢
0R <R
1R |
24 | | fveq2 5496 |
. . . . . . 7
⊢ (𝑚 = 𝐴 → (𝐹‘𝑚) = (𝐹‘𝐴)) |
25 | 24 | breq2d 4001 |
. . . . . 6
⊢ (𝑚 = 𝐴 → (1R
<R (𝐹‘𝑚) ↔ 1R
<R (𝐹‘𝐴))) |
26 | 25 | rspcv 2830 |
. . . . 5
⊢ (𝐴 ∈ N →
(∀𝑚 ∈
N 1R <R
(𝐹‘𝑚) → 1R
<R (𝐹‘𝐴))) |
27 | 9, 26 | mpan9 279 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ N) →
1R <R (𝐹‘𝐴)) |
28 | | ltsosr 7726 |
. . . . 5
⊢
<R Or R |
29 | | ltrelsr 7700 |
. . . . 5
⊢
<R ⊆ (R ×
R) |
30 | 28, 29 | sotri 5006 |
. . . 4
⊢
((0R <R
1R ∧ 1R
<R (𝐹‘𝐴)) → 0R
<R (𝐹‘𝐴)) |
31 | 23, 27, 30 | sylancr 412 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ N) →
0R <R (𝐹‘𝐴)) |
32 | | prsrriota 7750 |
. . 3
⊢ (((𝐹‘𝐴) ∈ R ∧
0R <R (𝐹‘𝐴)) → [〈((℩𝑦 ∈ P
[〈(𝑦
+P 1P),
1P〉] ~R = (𝐹‘𝐴)) +P
1P), 1P〉]
~R = (𝐹‘𝐴)) |
33 | 22, 31, 32 | syl2anc 409 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ N) →
[〈((℩𝑦
∈ P [〈(𝑦 +P
1P), 1P〉]
~R = (𝐹‘𝐴)) +P
1P), 1P〉]
~R = (𝐹‘𝐴)) |
34 | 14, 21, 33 | 3eqtrd 2207 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ N) →
[〈((𝐺‘𝐴) +P
1P), 1P〉]
~R = (𝐹‘𝐴)) |