Metamath Proof Explorer

Theorem axcontlem1

Description: Lemma for axcont . Change bound variables for later use. (Contributed by Scott Fenton, 20-Jun-2013)

Ref Expression
Hypothesis axcontlem1.1 ⊢F=xt|x∈D∧t∈0+∞∧∀i∈1…Nx⁡i=1−t⁢Z⁡i+t⁢U⁡i
Assertion axcontlem1 ⊢F=ys|y∈D∧s∈0+∞∧∀j∈1…Ny⁡j=1−s⁢Z⁡j+s⁢U⁡j

Proof

Step Hyp Ref Expression
1 axcontlem1.1 ⊢F=xt|x∈D∧t∈0+∞∧∀i∈1…Nx⁡i=1−t⁢Z⁡i+t⁢U⁡i
2 eleq1w ⊢x=y→x∈D↔y∈D
3 2 adantr ⊢x=y∧t=s→x∈D↔y∈D
4 eleq1w ⊢t=s→t∈0+∞↔s∈0+∞
5 4 adantl ⊢x=y∧t=s→t∈0+∞↔s∈0+∞
6 fveq1 ⊢x=y→x⁡i=y⁡i
7 oveq2 ⊢t=s→1−t=1−s
8 7 oveq1d ⊢t=s→1−t⁢Z⁡i=1−s⁢Z⁡i
9 oveq1 ⊢t=s→t⁢U⁡i=s⁢U⁡i
10 8 9 oveq12d ⊢t=s→1−t⁢Z⁡i+t⁢U⁡i=1−s⁢Z⁡i+s⁢U⁡i
11 6 10 eqeqan12d ⊢x=y∧t=s→x⁡i=1−t⁢Z⁡i+t⁢U⁡i↔y⁡i=1−s⁢Z⁡i+s⁢U⁡i
12 11 ralbidv ⊢x=y∧t=s→∀i∈1…Nx⁡i=1−t⁢Z⁡i+t⁢U⁡i↔∀i∈1…Ny⁡i=1−s⁢Z⁡i+s⁢U⁡i
13 fveq2 ⊢i=j→y⁡i=y⁡j
14 fveq2 ⊢i=j→Z⁡i=Z⁡j
15 14 oveq2d ⊢i=j→1−s⁢Z⁡i=1−s⁢Z⁡j
16 fveq2 ⊢i=j→U⁡i=U⁡j
17 16 oveq2d ⊢i=j→s⁢U⁡i=s⁢U⁡j
18 15 17 oveq12d ⊢i=j→1−s⁢Z⁡i+s⁢U⁡i=1−s⁢Z⁡j+s⁢U⁡j
19 13 18 eqeq12d ⊢i=j→y⁡i=1−s⁢Z⁡i+s⁢U⁡i↔y⁡j=1−s⁢Z⁡j+s⁢U⁡j
20 19 cbvralvw ⊢∀i∈1…Ny⁡i=1−s⁢Z⁡i+s⁢U⁡i↔∀j∈1…Ny⁡j=1−s⁢Z⁡j+s⁢U⁡j
21 12 20 bitrdi ⊢x=y∧t=s→∀i∈1…Nx⁡i=1−t⁢Z⁡i+t⁢U⁡i↔∀j∈1…Ny⁡j=1−s⁢Z⁡j+s⁢U⁡j
22 5 21 anbi12d ⊢x=y∧t=s→t∈0+∞∧∀i∈1…Nx⁡i=1−t⁢Z⁡i+t⁢U⁡i↔s∈0+∞∧∀j∈1…Ny⁡j=1−s⁢Z⁡j+s⁢U⁡j
23 3 22 anbi12d ⊢x=y∧t=s→x∈D∧t∈0+∞∧∀i∈1…Nx⁡i=1−t⁢Z⁡i+t⁢U⁡i↔y∈D∧s∈0+∞∧∀j∈1…Ny⁡j=1−s⁢Z⁡j+s⁢U⁡j
24 23 cbvopabv ⊢xt|x∈D∧t∈0+∞∧∀i∈1…Nx⁡i=1−t⁢Z⁡i+t⁢U⁡i=ys|y∈D∧s∈0+∞∧∀j∈1…Ny⁡j=1−s⁢Z⁡j+s⁢U⁡j
25 1 24 eqtri ⊢F=ys|y∈D∧s∈0+∞∧∀j∈1…Ny⁡j=1−s⁢Z⁡j+s⁢U⁡j