| Step | Hyp | Ref
| Expression |
| 1 | | ixpfn 8943 |
. . . . . 6
⊢ (𝑓 ∈ X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)) → 𝑓 Fn 𝑋) |
| 2 | 1 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘))) → 𝑓 Fn 𝑋) |
| 3 | | rrxsnicc.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m 𝑋)) |
| 4 | | elmapfn 8905 |
. . . . . . 7
⊢ (𝐴 ∈ (ℝ
↑m 𝑋)
→ 𝐴 Fn 𝑋) |
| 5 | 3, 4 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐴 Fn 𝑋) |
| 6 | 5 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘))) → 𝐴 Fn 𝑋) |
| 7 | | simpll 767 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘))) ∧ 𝑗 ∈ 𝑋) → 𝜑) |
| 8 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → (𝐴‘𝑘) = (𝐴‘𝑗)) |
| 9 | 8, 8 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → ((𝐴‘𝑘)[,](𝐴‘𝑘)) = ((𝐴‘𝑗)[,](𝐴‘𝑗))) |
| 10 | 9 | cbvixpv 8955 |
. . . . . . . . 9
⊢ X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)) = X𝑗 ∈ 𝑋 ((𝐴‘𝑗)[,](𝐴‘𝑗)) |
| 11 | 10 | eleq2i 2833 |
. . . . . . . 8
⊢ (𝑓 ∈ X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)) ↔ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)[,](𝐴‘𝑗))) |
| 12 | 11 | biimpi 216 |
. . . . . . 7
⊢ (𝑓 ∈ X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)) → 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)[,](𝐴‘𝑗))) |
| 13 | 12 | ad2antlr 727 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘))) ∧ 𝑗 ∈ 𝑋) → 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)[,](𝐴‘𝑗))) |
| 14 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘))) ∧ 𝑗 ∈ 𝑋) → 𝑗 ∈ 𝑋) |
| 15 | | elmapi 8889 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (ℝ
↑m 𝑋)
→ 𝐴:𝑋⟶ℝ) |
| 16 | 3, 15 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
| 17 | 16 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (𝐴‘𝑗) ∈ ℝ) |
| 18 | 17 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)[,](𝐴‘𝑗))) ∧ 𝑗 ∈ 𝑋) → (𝐴‘𝑗) ∈ ℝ) |
| 19 | 18, 18 | iccssred 13474 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)[,](𝐴‘𝑗))) ∧ 𝑗 ∈ 𝑋) → ((𝐴‘𝑗)[,](𝐴‘𝑗)) ⊆ ℝ) |
| 20 | | fvixp2 45204 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ X𝑗 ∈
𝑋 ((𝐴‘𝑗)[,](𝐴‘𝑗)) ∧ 𝑗 ∈ 𝑋) → (𝑓‘𝑗) ∈ ((𝐴‘𝑗)[,](𝐴‘𝑗))) |
| 21 | 20 | adantll 714 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)[,](𝐴‘𝑗))) ∧ 𝑗 ∈ 𝑋) → (𝑓‘𝑗) ∈ ((𝐴‘𝑗)[,](𝐴‘𝑗))) |
| 22 | 19, 21 | sseldd 3984 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)[,](𝐴‘𝑗))) ∧ 𝑗 ∈ 𝑋) → (𝑓‘𝑗) ∈ ℝ) |
| 23 | 22 | rexrd 11311 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)[,](𝐴‘𝑗))) ∧ 𝑗 ∈ 𝑋) → (𝑓‘𝑗) ∈
ℝ*) |
| 24 | 18 | rexrd 11311 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)[,](𝐴‘𝑗))) ∧ 𝑗 ∈ 𝑋) → (𝐴‘𝑗) ∈
ℝ*) |
| 25 | | iccleub 13442 |
. . . . . . . 8
⊢ (((𝐴‘𝑗) ∈ ℝ* ∧ (𝐴‘𝑗) ∈ ℝ* ∧ (𝑓‘𝑗) ∈ ((𝐴‘𝑗)[,](𝐴‘𝑗))) → (𝑓‘𝑗) ≤ (𝐴‘𝑗)) |
| 26 | 24, 24, 21, 25 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)[,](𝐴‘𝑗))) ∧ 𝑗 ∈ 𝑋) → (𝑓‘𝑗) ≤ (𝐴‘𝑗)) |
| 27 | | iccgelb 13443 |
. . . . . . . 8
⊢ (((𝐴‘𝑗) ∈ ℝ* ∧ (𝐴‘𝑗) ∈ ℝ* ∧ (𝑓‘𝑗) ∈ ((𝐴‘𝑗)[,](𝐴‘𝑗))) → (𝐴‘𝑗) ≤ (𝑓‘𝑗)) |
| 28 | 24, 24, 21, 27 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)[,](𝐴‘𝑗))) ∧ 𝑗 ∈ 𝑋) → (𝐴‘𝑗) ≤ (𝑓‘𝑗)) |
| 29 | 23, 24, 26, 28 | xrletrid 13197 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)[,](𝐴‘𝑗))) ∧ 𝑗 ∈ 𝑋) → (𝑓‘𝑗) = (𝐴‘𝑗)) |
| 30 | 7, 13, 14, 29 | syl21anc 838 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘))) ∧ 𝑗 ∈ 𝑋) → (𝑓‘𝑗) = (𝐴‘𝑗)) |
| 31 | 2, 6, 30 | eqfnfvd 7054 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘))) → 𝑓 = 𝐴) |
| 32 | | velsn 4642 |
. . . . . 6
⊢ (𝑓 ∈ {𝐴} ↔ 𝑓 = 𝐴) |
| 33 | 32 | bicomi 224 |
. . . . 5
⊢ (𝑓 = 𝐴 ↔ 𝑓 ∈ {𝐴}) |
| 34 | 33 | biimpi 216 |
. . . 4
⊢ (𝑓 = 𝐴 → 𝑓 ∈ {𝐴}) |
| 35 | 31, 34 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘))) → 𝑓 ∈ {𝐴}) |
| 36 | 35 | ssd 45085 |
. 2
⊢ (𝜑 → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)) ⊆ {𝐴}) |
| 37 | 3 | elexd 3504 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ V) |
| 38 | 16 | ffvelcdmda 7104 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
| 39 | 38 | leidd 11829 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐴‘𝑘)) |
| 40 | 38, 38, 38, 39, 39 | eliccd 45517 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ((𝐴‘𝑘)[,](𝐴‘𝑘))) |
| 41 | 40 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ∈ ((𝐴‘𝑘)[,](𝐴‘𝑘))) |
| 42 | 37, 5, 41 | 3jca 1129 |
. . . 4
⊢ (𝜑 → (𝐴 ∈ V ∧ 𝐴 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ∈ ((𝐴‘𝑘)[,](𝐴‘𝑘)))) |
| 43 | | elixp2 8941 |
. . . 4
⊢ (𝐴 ∈ X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)) ↔ (𝐴 ∈ V ∧ 𝐴 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ∈ ((𝐴‘𝑘)[,](𝐴‘𝑘)))) |
| 44 | 42, 43 | sylibr 234 |
. . 3
⊢ (𝜑 → 𝐴 ∈ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘))) |
| 45 | | snssg 4783 |
. . . 4
⊢ (𝐴 ∈ (ℝ
↑m 𝑋)
→ (𝐴 ∈ X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)) ↔ {𝐴} ⊆ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)))) |
| 46 | 3, 45 | syl 17 |
. . 3
⊢ (𝜑 → (𝐴 ∈ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)) ↔ {𝐴} ⊆ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)))) |
| 47 | 44, 46 | mpbid 232 |
. 2
⊢ (𝜑 → {𝐴} ⊆ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘))) |
| 48 | 36, 47 | eqssd 4001 |
1
⊢ (𝜑 → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)) = {𝐴}) |