Proof of Theorem fzo0pmtrlast
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fzo0pmtrlast.j | . . . . . 6
⊢ 𝐽 = (0..^𝑁) | 
| 2 | 1 | ovexi 7466 | . . . . 5
⊢ 𝐽 ∈ V | 
| 3 | 2 | a1i 11 | . . . 4
⊢ ((𝜑 ∧ 𝐼 = (𝑁 − 1)) → 𝐽 ∈ V) | 
| 4 | 3 | resiexd 7237 | . . 3
⊢ ((𝜑 ∧ 𝐼 = (𝑁 − 1)) → ( I ↾ 𝐽) ∈ V) | 
| 5 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐼 = (𝑁 − 1)) → 𝐼 = (𝑁 − 1)) | 
| 6 |  | fzo0pmtrlast.i | . . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ 𝐽) | 
| 7 | 6 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐼 = (𝑁 − 1)) → 𝐼 ∈ 𝐽) | 
| 8 | 5, 7 | eqeltrrd 2841 | . . . . . 6
⊢ ((𝜑 ∧ 𝐼 = (𝑁 − 1)) → (𝑁 − 1) ∈ 𝐽) | 
| 9 |  | fvresi 7194 | . . . . . 6
⊢ ((𝑁 − 1) ∈ 𝐽 → (( I ↾ 𝐽)‘(𝑁 − 1)) = (𝑁 − 1)) | 
| 10 | 8, 9 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ 𝐼 = (𝑁 − 1)) → (( I ↾ 𝐽)‘(𝑁 − 1)) = (𝑁 − 1)) | 
| 11 | 10, 5 | eqtr4d 2779 | . . . 4
⊢ ((𝜑 ∧ 𝐼 = (𝑁 − 1)) → (( I ↾ 𝐽)‘(𝑁 − 1)) = 𝐼) | 
| 12 |  | f1oi 6885 | . . . 4
⊢ ( I
↾ 𝐽):𝐽–1-1-onto→𝐽 | 
| 13 | 11, 12 | jctil 519 | . . 3
⊢ ((𝜑 ∧ 𝐼 = (𝑁 − 1)) → (( I ↾ 𝐽):𝐽–1-1-onto→𝐽 ∧ (( I ↾ 𝐽)‘(𝑁 − 1)) = 𝐼)) | 
| 14 |  | f1oeq1 6835 | . . . 4
⊢ (𝑠 = ( I ↾ 𝐽) → (𝑠:𝐽–1-1-onto→𝐽 ↔ ( I ↾ 𝐽):𝐽–1-1-onto→𝐽)) | 
| 15 |  | fveq1 6904 | . . . . 5
⊢ (𝑠 = ( I ↾ 𝐽) → (𝑠‘(𝑁 − 1)) = (( I ↾ 𝐽)‘(𝑁 − 1))) | 
| 16 | 15 | eqeq1d 2738 | . . . 4
⊢ (𝑠 = ( I ↾ 𝐽) → ((𝑠‘(𝑁 − 1)) = 𝐼 ↔ (( I ↾ 𝐽)‘(𝑁 − 1)) = 𝐼)) | 
| 17 | 14, 16 | anbi12d 632 | . . 3
⊢ (𝑠 = ( I ↾ 𝐽) → ((𝑠:𝐽–1-1-onto→𝐽 ∧ (𝑠‘(𝑁 − 1)) = 𝐼) ↔ (( I ↾ 𝐽):𝐽–1-1-onto→𝐽 ∧ (( I ↾ 𝐽)‘(𝑁 − 1)) = 𝐼))) | 
| 18 | 4, 13, 17 | spcedv 3597 | . 2
⊢ ((𝜑 ∧ 𝐼 = (𝑁 − 1)) → ∃𝑠(𝑠:𝐽–1-1-onto→𝐽 ∧ (𝑠‘(𝑁 − 1)) = 𝐼)) | 
| 19 |  | fvexd 6920 | . . 3
⊢ ((𝜑 ∧ 𝐼 ≠ (𝑁 − 1)) → ((pmTrsp‘𝐽)‘{𝐼, (𝑁 − 1)}) ∈ V) | 
| 20 | 2 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝐼 ≠ (𝑁 − 1)) → 𝐽 ∈ V) | 
| 21 | 6 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐼 ≠ (𝑁 − 1)) → 𝐼 ∈ 𝐽) | 
| 22 | 6, 1 | eleqtrdi 2850 | . . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ (0..^𝑁)) | 
| 23 |  | elfzo0 13741 | . . . . . . . . . . 11
⊢ (𝐼 ∈ (0..^𝑁) ↔ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) | 
| 24 | 23 | simp2bi 1146 | . . . . . . . . . 10
⊢ (𝐼 ∈ (0..^𝑁) → 𝑁 ∈ ℕ) | 
| 25 |  | fzo0end 13798 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁)) | 
| 26 | 22, 24, 25 | 3syl 18 | . . . . . . . . 9
⊢ (𝜑 → (𝑁 − 1) ∈ (0..^𝑁)) | 
| 27 | 26, 1 | eleqtrrdi 2851 | . . . . . . . 8
⊢ (𝜑 → (𝑁 − 1) ∈ 𝐽) | 
| 28 | 27 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐼 ≠ (𝑁 − 1)) → (𝑁 − 1) ∈ 𝐽) | 
| 29 | 21, 28 | prssd 4821 | . . . . . 6
⊢ ((𝜑 ∧ 𝐼 ≠ (𝑁 − 1)) → {𝐼, (𝑁 − 1)} ⊆ 𝐽) | 
| 30 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐼 ≠ (𝑁 − 1)) → 𝐼 ≠ (𝑁 − 1)) | 
| 31 |  | enpr2 10043 | . . . . . . 7
⊢ ((𝐼 ∈ 𝐽 ∧ (𝑁 − 1) ∈ 𝐽 ∧ 𝐼 ≠ (𝑁 − 1)) → {𝐼, (𝑁 − 1)} ≈
2o) | 
| 32 | 21, 28, 30, 31 | syl3anc 1372 | . . . . . 6
⊢ ((𝜑 ∧ 𝐼 ≠ (𝑁 − 1)) → {𝐼, (𝑁 − 1)} ≈
2o) | 
| 33 |  | eqid 2736 | . . . . . . 7
⊢
(pmTrsp‘𝐽) =
(pmTrsp‘𝐽) | 
| 34 |  | eqid 2736 | . . . . . . 7
⊢ ran
(pmTrsp‘𝐽) = ran
(pmTrsp‘𝐽) | 
| 35 | 33, 34 | pmtrrn 19476 | . . . . . 6
⊢ ((𝐽 ∈ V ∧ {𝐼, (𝑁 − 1)} ⊆ 𝐽 ∧ {𝐼, (𝑁 − 1)} ≈ 2o) →
((pmTrsp‘𝐽)‘{𝐼, (𝑁 − 1)}) ∈ ran (pmTrsp‘𝐽)) | 
| 36 | 20, 29, 32, 35 | syl3anc 1372 | . . . . 5
⊢ ((𝜑 ∧ 𝐼 ≠ (𝑁 − 1)) → ((pmTrsp‘𝐽)‘{𝐼, (𝑁 − 1)}) ∈ ran (pmTrsp‘𝐽)) | 
| 37 | 33, 34 | pmtrff1o 19482 | . . . . 5
⊢
(((pmTrsp‘𝐽)‘{𝐼, (𝑁 − 1)}) ∈ ran (pmTrsp‘𝐽) → ((pmTrsp‘𝐽)‘{𝐼, (𝑁 − 1)}):𝐽–1-1-onto→𝐽) | 
| 38 | 36, 37 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝐼 ≠ (𝑁 − 1)) → ((pmTrsp‘𝐽)‘{𝐼, (𝑁 − 1)}):𝐽–1-1-onto→𝐽) | 
| 39 | 33 | pmtrprfv2 33109 | . . . . 5
⊢ ((𝐽 ∈ V ∧ (𝐼 ∈ 𝐽 ∧ (𝑁 − 1) ∈ 𝐽 ∧ 𝐼 ≠ (𝑁 − 1))) → (((pmTrsp‘𝐽)‘{𝐼, (𝑁 − 1)})‘(𝑁 − 1)) = 𝐼) | 
| 40 | 20, 21, 28, 30, 39 | syl13anc 1373 | . . . 4
⊢ ((𝜑 ∧ 𝐼 ≠ (𝑁 − 1)) → (((pmTrsp‘𝐽)‘{𝐼, (𝑁 − 1)})‘(𝑁 − 1)) = 𝐼) | 
| 41 | 38, 40 | jca 511 | . . 3
⊢ ((𝜑 ∧ 𝐼 ≠ (𝑁 − 1)) → (((pmTrsp‘𝐽)‘{𝐼, (𝑁 − 1)}):𝐽–1-1-onto→𝐽 ∧ (((pmTrsp‘𝐽)‘{𝐼, (𝑁 − 1)})‘(𝑁 − 1)) = 𝐼)) | 
| 42 |  | f1oeq1 6835 | . . . 4
⊢ (𝑠 = ((pmTrsp‘𝐽)‘{𝐼, (𝑁 − 1)}) → (𝑠:𝐽–1-1-onto→𝐽 ↔ ((pmTrsp‘𝐽)‘{𝐼, (𝑁 − 1)}):𝐽–1-1-onto→𝐽)) | 
| 43 |  | fveq1 6904 | . . . . 5
⊢ (𝑠 = ((pmTrsp‘𝐽)‘{𝐼, (𝑁 − 1)}) → (𝑠‘(𝑁 − 1)) = (((pmTrsp‘𝐽)‘{𝐼, (𝑁 − 1)})‘(𝑁 − 1))) | 
| 44 | 43 | eqeq1d 2738 | . . . 4
⊢ (𝑠 = ((pmTrsp‘𝐽)‘{𝐼, (𝑁 − 1)}) → ((𝑠‘(𝑁 − 1)) = 𝐼 ↔ (((pmTrsp‘𝐽)‘{𝐼, (𝑁 − 1)})‘(𝑁 − 1)) = 𝐼)) | 
| 45 | 42, 44 | anbi12d 632 | . . 3
⊢ (𝑠 = ((pmTrsp‘𝐽)‘{𝐼, (𝑁 − 1)}) → ((𝑠:𝐽–1-1-onto→𝐽 ∧ (𝑠‘(𝑁 − 1)) = 𝐼) ↔ (((pmTrsp‘𝐽)‘{𝐼, (𝑁 − 1)}):𝐽–1-1-onto→𝐽 ∧ (((pmTrsp‘𝐽)‘{𝐼, (𝑁 − 1)})‘(𝑁 − 1)) = 𝐼))) | 
| 46 | 19, 41, 45 | spcedv 3597 | . 2
⊢ ((𝜑 ∧ 𝐼 ≠ (𝑁 − 1)) → ∃𝑠(𝑠:𝐽–1-1-onto→𝐽 ∧ (𝑠‘(𝑁 − 1)) = 𝐼)) | 
| 47 | 18, 46 | pm2.61dane 3028 | 1
⊢ (𝜑 → ∃𝑠(𝑠:𝐽–1-1-onto→𝐽 ∧ (𝑠‘(𝑁 − 1)) = 𝐼)) |