| Step | Hyp | Ref
| Expression |
| 1 | | elnn0 12528 |
. . 3
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
| 2 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 1 → (𝐴↑𝑟𝑥) = (𝐴↑𝑟1)) |
| 3 | 2 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑥 = 1 → ((𝐴↑𝑟𝑥)↑𝑟0) = ((𝐴↑𝑟1)↑𝑟0)) |
| 4 | 3 | sseq1d 4015 |
. . . . . 6
⊢ (𝑥 = 1 → (((𝐴↑𝑟𝑥)↑𝑟0) ⊆ (𝐴↑𝑟0)
↔ ((𝐴↑𝑟1)↑𝑟0)
⊆ (𝐴↑𝑟0))) |
| 5 | 4 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = 1 → ((𝐴 ∈ 𝑉 → ((𝐴↑𝑟𝑥)↑𝑟0) ⊆ (𝐴↑𝑟0))
↔ (𝐴 ∈ 𝑉 → ((𝐴↑𝑟1)↑𝑟0)
⊆ (𝐴↑𝑟0)))) |
| 6 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐴↑𝑟𝑥) = (𝐴↑𝑟𝑦)) |
| 7 | 6 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝐴↑𝑟𝑥)↑𝑟0) = ((𝐴↑𝑟𝑦)↑𝑟0)) |
| 8 | 7 | sseq1d 4015 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (((𝐴↑𝑟𝑥)↑𝑟0) ⊆ (𝐴↑𝑟0)
↔ ((𝐴↑𝑟𝑦)↑𝑟0) ⊆ (𝐴↑𝑟0))) |
| 9 | 8 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝐴 ∈ 𝑉 → ((𝐴↑𝑟𝑥)↑𝑟0) ⊆ (𝐴↑𝑟0))
↔ (𝐴 ∈ 𝑉 → ((𝐴↑𝑟𝑦)↑𝑟0) ⊆ (𝐴↑𝑟0)))) |
| 10 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 + 1) → (𝐴↑𝑟𝑥) = (𝐴↑𝑟(𝑦 + 1))) |
| 11 | 10 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → ((𝐴↑𝑟𝑥)↑𝑟0) = ((𝐴↑𝑟(𝑦 +
1))↑𝑟0)) |
| 12 | 11 | sseq1d 4015 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → (((𝐴↑𝑟𝑥)↑𝑟0) ⊆ (𝐴↑𝑟0)
↔ ((𝐴↑𝑟(𝑦 +
1))↑𝑟0) ⊆ (𝐴↑𝑟0))) |
| 13 | 12 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → ((𝐴 ∈ 𝑉 → ((𝐴↑𝑟𝑥)↑𝑟0) ⊆ (𝐴↑𝑟0))
↔ (𝐴 ∈ 𝑉 → ((𝐴↑𝑟(𝑦 +
1))↑𝑟0) ⊆ (𝐴↑𝑟0)))) |
| 14 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝐴↑𝑟𝑥) = (𝐴↑𝑟𝑁)) |
| 15 | 14 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → ((𝐴↑𝑟𝑥)↑𝑟0) = ((𝐴↑𝑟𝑁)↑𝑟0)) |
| 16 | 15 | sseq1d 4015 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (((𝐴↑𝑟𝑥)↑𝑟0) ⊆ (𝐴↑𝑟0)
↔ ((𝐴↑𝑟𝑁)↑𝑟0) ⊆ (𝐴↑𝑟0))) |
| 17 | 16 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = 𝑁 → ((𝐴 ∈ 𝑉 → ((𝐴↑𝑟𝑥)↑𝑟0) ⊆ (𝐴↑𝑟0))
↔ (𝐴 ∈ 𝑉 → ((𝐴↑𝑟𝑁)↑𝑟0) ⊆ (𝐴↑𝑟0)))) |
| 18 | | relexp1g 15065 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝐴↑𝑟1) = 𝐴) |
| 19 | 18 | oveq1d 7446 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ((𝐴↑𝑟1)↑𝑟0)
= (𝐴↑𝑟0)) |
| 20 | | ssid 4006 |
. . . . . 6
⊢ (𝐴↑𝑟0)
⊆ (𝐴↑𝑟0) |
| 21 | 19, 20 | eqsstrdi 4028 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ((𝐴↑𝑟1)↑𝑟0)
⊆ (𝐴↑𝑟0)) |
| 22 | | simp2 1138 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝐴 ∈ 𝑉 ∧ ((𝐴↑𝑟𝑦)↑𝑟0) ⊆ (𝐴↑𝑟0))
→ 𝐴 ∈ 𝑉) |
| 23 | | simp1 1137 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝐴 ∈ 𝑉 ∧ ((𝐴↑𝑟𝑦)↑𝑟0) ⊆ (𝐴↑𝑟0))
→ 𝑦 ∈
ℕ) |
| 24 | | relexpsucnnr 15064 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ℕ) → (𝐴↑𝑟(𝑦 + 1)) = ((𝐴↑𝑟𝑦) ∘ 𝐴)) |
| 25 | 24 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ℕ) → ((𝐴↑𝑟(𝑦 +
1))↑𝑟0) = (((𝐴↑𝑟𝑦) ∘ 𝐴)↑𝑟0)) |
| 26 | 22, 23, 25 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ 𝐴 ∈ 𝑉 ∧ ((𝐴↑𝑟𝑦)↑𝑟0) ⊆ (𝐴↑𝑟0))
→ ((𝐴↑𝑟(𝑦 +
1))↑𝑟0) = (((𝐴↑𝑟𝑦) ∘ 𝐴)↑𝑟0)) |
| 27 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢ (𝐴↑𝑟𝑦) ∈ V |
| 28 | | coexg 7951 |
. . . . . . . . . . . . 13
⊢ (((𝐴↑𝑟𝑦) ∈ V ∧ 𝐴 ∈ 𝑉) → ((𝐴↑𝑟𝑦) ∘ 𝐴) ∈ V) |
| 29 | 27, 28 | mpan 690 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → ((𝐴↑𝑟𝑦) ∘ 𝐴) ∈ V) |
| 30 | | relexp0g 15061 |
. . . . . . . . . . . 12
⊢ (((𝐴↑𝑟𝑦) ∘ 𝐴) ∈ V → (((𝐴↑𝑟𝑦) ∘ 𝐴)↑𝑟0) = ( I ↾
(dom ((𝐴↑𝑟𝑦) ∘ 𝐴) ∪ ran ((𝐴↑𝑟𝑦) ∘ 𝐴)))) |
| 31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → (((𝐴↑𝑟𝑦) ∘ 𝐴)↑𝑟0) = ( I ↾
(dom ((𝐴↑𝑟𝑦) ∘ 𝐴) ∪ ran ((𝐴↑𝑟𝑦) ∘ 𝐴)))) |
| 32 | | dmcoss 5985 |
. . . . . . . . . . . . 13
⊢ dom
((𝐴↑𝑟𝑦) ∘ 𝐴) ⊆ dom 𝐴 |
| 33 | | rncoss 5986 |
. . . . . . . . . . . . 13
⊢ ran
((𝐴↑𝑟𝑦) ∘ 𝐴) ⊆ ran (𝐴↑𝑟𝑦) |
| 34 | | unss12 4188 |
. . . . . . . . . . . . 13
⊢ ((dom
((𝐴↑𝑟𝑦) ∘ 𝐴) ⊆ dom 𝐴 ∧ ran ((𝐴↑𝑟𝑦) ∘ 𝐴) ⊆ ran (𝐴↑𝑟𝑦)) → (dom ((𝐴↑𝑟𝑦) ∘ 𝐴) ∪ ran ((𝐴↑𝑟𝑦) ∘ 𝐴)) ⊆ (dom 𝐴 ∪ ran (𝐴↑𝑟𝑦))) |
| 35 | 32, 33, 34 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (dom
((𝐴↑𝑟𝑦) ∘ 𝐴) ∪ ran ((𝐴↑𝑟𝑦) ∘ 𝐴)) ⊆ (dom 𝐴 ∪ ran (𝐴↑𝑟𝑦)) |
| 36 | | ssres2 6022 |
. . . . . . . . . . . 12
⊢ ((dom
((𝐴↑𝑟𝑦) ∘ 𝐴) ∪ ran ((𝐴↑𝑟𝑦) ∘ 𝐴)) ⊆ (dom 𝐴 ∪ ran (𝐴↑𝑟𝑦)) → ( I ↾ (dom ((𝐴↑𝑟𝑦) ∘ 𝐴) ∪ ran ((𝐴↑𝑟𝑦) ∘ 𝐴))) ⊆ ( I ↾ (dom 𝐴 ∪ ran (𝐴↑𝑟𝑦)))) |
| 37 | 35, 36 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ( I
↾ (dom ((𝐴↑𝑟𝑦) ∘ 𝐴) ∪ ran ((𝐴↑𝑟𝑦) ∘ 𝐴))) ⊆ ( I ↾ (dom 𝐴 ∪ ran (𝐴↑𝑟𝑦))) |
| 38 | 31, 37 | eqsstrdi 4028 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (((𝐴↑𝑟𝑦) ∘ 𝐴)↑𝑟0) ⊆ ( I
↾ (dom 𝐴 ∪ ran
(𝐴↑𝑟𝑦)))) |
| 39 | 22, 38 | syl 17 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝐴 ∈ 𝑉 ∧ ((𝐴↑𝑟𝑦)↑𝑟0) ⊆ (𝐴↑𝑟0))
→ (((𝐴↑𝑟𝑦) ∘ 𝐴)↑𝑟0) ⊆ ( I
↾ (dom 𝐴 ∪ ran
(𝐴↑𝑟𝑦)))) |
| 40 | | resundi 6011 |
. . . . . . . . . . 11
⊢ ( I
↾ (dom 𝐴 ∪ ran
(𝐴↑𝑟𝑦))) = (( I ↾ dom 𝐴) ∪ ( I ↾ ran (𝐴↑𝑟𝑦))) |
| 41 | | ssun1 4178 |
. . . . . . . . . . . . . . 15
⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) |
| 42 | | ssres2 6022 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) → ( I ↾ dom 𝐴) ⊆ ( I ↾ (dom 𝐴 ∪ ran 𝐴))) |
| 43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ( I
↾ dom 𝐴) ⊆ ( I
↾ (dom 𝐴 ∪ ran
𝐴)) |
| 44 | | relexp0g 15061 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑉 → (𝐴↑𝑟0) = ( I ↾
(dom 𝐴 ∪ ran 𝐴))) |
| 45 | 43, 44 | sseqtrrid 4027 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → ( I ↾ dom 𝐴) ⊆ (𝐴↑𝑟0)) |
| 46 | 45 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ ((𝐴↑𝑟𝑦)↑𝑟0) ⊆ (𝐴↑𝑟0))
→ ( I ↾ dom 𝐴)
⊆ (𝐴↑𝑟0)) |
| 47 | | ssun2 4179 |
. . . . . . . . . . . . . . 15
⊢ ran
(𝐴↑𝑟𝑦) ⊆ (dom (𝐴↑𝑟𝑦) ∪ ran (𝐴↑𝑟𝑦)) |
| 48 | | ssres2 6022 |
. . . . . . . . . . . . . . 15
⊢ (ran
(𝐴↑𝑟𝑦) ⊆ (dom (𝐴↑𝑟𝑦) ∪ ran (𝐴↑𝑟𝑦)) → ( I ↾ ran (𝐴↑𝑟𝑦)) ⊆ ( I ↾ (dom (𝐴↑𝑟𝑦) ∪ ran (𝐴↑𝑟𝑦)))) |
| 49 | 47, 48 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ( I
↾ ran (𝐴↑𝑟𝑦)) ⊆ ( I ↾ (dom (𝐴↑𝑟𝑦) ∪ ran (𝐴↑𝑟𝑦))) |
| 50 | | relexp0g 15061 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴↑𝑟𝑦) ∈ V → ((𝐴↑𝑟𝑦)↑𝑟0) =
( I ↾ (dom (𝐴↑𝑟𝑦) ∪ ran (𝐴↑𝑟𝑦)))) |
| 51 | 27, 50 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((𝐴↑𝑟𝑦)↑𝑟0) =
( I ↾ (dom (𝐴↑𝑟𝑦) ∪ ran (𝐴↑𝑟𝑦))) |
| 52 | 49, 51 | sseqtrri 4033 |
. . . . . . . . . . . . 13
⊢ ( I
↾ ran (𝐴↑𝑟𝑦)) ⊆ ((𝐴↑𝑟𝑦)↑𝑟0) |
| 53 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ ((𝐴↑𝑟𝑦)↑𝑟0) ⊆ (𝐴↑𝑟0))
→ ((𝐴↑𝑟𝑦)↑𝑟0) ⊆ (𝐴↑𝑟0)) |
| 54 | 52, 53 | sstrid 3995 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ ((𝐴↑𝑟𝑦)↑𝑟0) ⊆ (𝐴↑𝑟0))
→ ( I ↾ ran (𝐴↑𝑟𝑦)) ⊆ (𝐴↑𝑟0)) |
| 55 | 46, 54 | unssd 4192 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ ((𝐴↑𝑟𝑦)↑𝑟0) ⊆ (𝐴↑𝑟0))
→ (( I ↾ dom 𝐴)
∪ ( I ↾ ran (𝐴↑𝑟𝑦))) ⊆ (𝐴↑𝑟0)) |
| 56 | 40, 55 | eqsstrid 4022 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ ((𝐴↑𝑟𝑦)↑𝑟0) ⊆ (𝐴↑𝑟0))
→ ( I ↾ (dom 𝐴
∪ ran (𝐴↑𝑟𝑦))) ⊆ (𝐴↑𝑟0)) |
| 57 | 56 | 3adant1 1131 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝐴 ∈ 𝑉 ∧ ((𝐴↑𝑟𝑦)↑𝑟0) ⊆ (𝐴↑𝑟0))
→ ( I ↾ (dom 𝐴
∪ ran (𝐴↑𝑟𝑦))) ⊆ (𝐴↑𝑟0)) |
| 58 | 39, 57 | sstrd 3994 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ 𝐴 ∈ 𝑉 ∧ ((𝐴↑𝑟𝑦)↑𝑟0) ⊆ (𝐴↑𝑟0))
→ (((𝐴↑𝑟𝑦) ∘ 𝐴)↑𝑟0) ⊆ (𝐴↑𝑟0)) |
| 59 | 26, 58 | eqsstrd 4018 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝐴 ∈ 𝑉 ∧ ((𝐴↑𝑟𝑦)↑𝑟0) ⊆ (𝐴↑𝑟0))
→ ((𝐴↑𝑟(𝑦 +
1))↑𝑟0) ⊆ (𝐴↑𝑟0)) |
| 60 | 59 | 3exp 1120 |
. . . . . 6
⊢ (𝑦 ∈ ℕ → (𝐴 ∈ 𝑉 → (((𝐴↑𝑟𝑦)↑𝑟0) ⊆ (𝐴↑𝑟0)
→ ((𝐴↑𝑟(𝑦 +
1))↑𝑟0) ⊆ (𝐴↑𝑟0)))) |
| 61 | 60 | a2d 29 |
. . . . 5
⊢ (𝑦 ∈ ℕ → ((𝐴 ∈ 𝑉 → ((𝐴↑𝑟𝑦)↑𝑟0) ⊆ (𝐴↑𝑟0))
→ (𝐴 ∈ 𝑉 → ((𝐴↑𝑟(𝑦 +
1))↑𝑟0) ⊆ (𝐴↑𝑟0)))) |
| 62 | 5, 9, 13, 17, 21, 61 | nnind 12284 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝐴 ∈ 𝑉 → ((𝐴↑𝑟𝑁)↑𝑟0) ⊆ (𝐴↑𝑟0))) |
| 63 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑁 = 0 → (𝐴↑𝑟𝑁) = (𝐴↑𝑟0)) |
| 64 | 63 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑁 = 0 → ((𝐴↑𝑟𝑁)↑𝑟0) = ((𝐴↑𝑟0)↑𝑟0)) |
| 65 | | relexp0idm 43728 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → ((𝐴↑𝑟0)↑𝑟0)
= (𝐴↑𝑟0)) |
| 66 | 64, 65 | sylan9eq 2797 |
. . . . . 6
⊢ ((𝑁 = 0 ∧ 𝐴 ∈ 𝑉) → ((𝐴↑𝑟𝑁)↑𝑟0) = (𝐴↑𝑟0)) |
| 67 | | eqimss 4042 |
. . . . . 6
⊢ (((𝐴↑𝑟𝑁)↑𝑟0) =
(𝐴↑𝑟0) → ((𝐴↑𝑟𝑁)↑𝑟0)
⊆ (𝐴↑𝑟0)) |
| 68 | 66, 67 | syl 17 |
. . . . 5
⊢ ((𝑁 = 0 ∧ 𝐴 ∈ 𝑉) → ((𝐴↑𝑟𝑁)↑𝑟0) ⊆ (𝐴↑𝑟0)) |
| 69 | 68 | ex 412 |
. . . 4
⊢ (𝑁 = 0 → (𝐴 ∈ 𝑉 → ((𝐴↑𝑟𝑁)↑𝑟0) ⊆ (𝐴↑𝑟0))) |
| 70 | 62, 69 | jaoi 858 |
. . 3
⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (𝐴 ∈ 𝑉 → ((𝐴↑𝑟𝑁)↑𝑟0) ⊆ (𝐴↑𝑟0))) |
| 71 | 1, 70 | sylbi 217 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ∈ 𝑉 → ((𝐴↑𝑟𝑁)↑𝑟0) ⊆ (𝐴↑𝑟0))) |
| 72 | 71 | impcom 407 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝐴↑𝑟𝑁)↑𝑟0)
⊆ (𝐴↑𝑟0)) |