Step |
Hyp |
Ref |
Expression |
1 |
|
r1elwf |
⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) |
2 |
|
elfvdm |
⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐵 ∈ dom 𝑅1 ) |
3 |
1 2
|
jca |
⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) ) |
4 |
3
|
a1i |
⊢ ( Lim 𝐵 → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) ) ) |
5 |
|
r1elwf |
⊢ ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) |
6 |
|
pwwf |
⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) |
7 |
5 6
|
sylibr |
⊢ ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) |
8 |
|
elfvdm |
⊢ ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐵 ∈ dom 𝑅1 ) |
9 |
7 8
|
jca |
⊢ ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) ) |
10 |
9
|
a1i |
⊢ ( Lim 𝐵 → ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) ) ) |
11 |
|
limsuc |
⊢ ( Lim 𝐵 → ( ( rank ‘ 𝐴 ) ∈ 𝐵 ↔ suc ( rank ‘ 𝐴 ) ∈ 𝐵 ) ) |
12 |
11
|
adantr |
⊢ ( ( Lim 𝐵 ∧ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) ) → ( ( rank ‘ 𝐴 ) ∈ 𝐵 ↔ suc ( rank ‘ 𝐴 ) ∈ 𝐵 ) ) |
13 |
|
rankpwi |
⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝒫 𝐴 ) = suc ( rank ‘ 𝐴 ) ) |
14 |
13
|
ad2antrl |
⊢ ( ( Lim 𝐵 ∧ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) ) → ( rank ‘ 𝒫 𝐴 ) = suc ( rank ‘ 𝐴 ) ) |
15 |
14
|
eleq1d |
⊢ ( ( Lim 𝐵 ∧ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) ) → ( ( rank ‘ 𝒫 𝐴 ) ∈ 𝐵 ↔ suc ( rank ‘ 𝐴 ) ∈ 𝐵 ) ) |
16 |
12 15
|
bitr4d |
⊢ ( ( Lim 𝐵 ∧ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) ) → ( ( rank ‘ 𝐴 ) ∈ 𝐵 ↔ ( rank ‘ 𝒫 𝐴 ) ∈ 𝐵 ) ) |
17 |
|
rankr1ag |
⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐴 ) ∈ 𝐵 ) ) |
18 |
17
|
adantl |
⊢ ( ( Lim 𝐵 ∧ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) ) → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐴 ) ∈ 𝐵 ) ) |
19 |
|
rankr1ag |
⊢ ( ( 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝒫 𝐴 ) ∈ 𝐵 ) ) |
20 |
6 19
|
sylanb |
⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝒫 𝐴 ) ∈ 𝐵 ) ) |
21 |
20
|
adantl |
⊢ ( ( Lim 𝐵 ∧ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) ) → ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝒫 𝐴 ) ∈ 𝐵 ) ) |
22 |
16 18 21
|
3bitr4d |
⊢ ( ( Lim 𝐵 ∧ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) ) → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ 𝒫 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ) ) |
23 |
22
|
ex |
⊢ ( Lim 𝐵 → ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ 𝒫 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ) ) ) |
24 |
4 10 23
|
pm5.21ndd |
⊢ ( Lim 𝐵 → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ 𝒫 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ) ) |