Step |
Hyp |
Ref |
Expression |
1 |
|
brfvrcld.r |
⊢ ( 𝜑 → 𝑅 ∈ V ) |
2 |
|
dfrcl4 |
⊢ r* = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ { 0 , 1 } ( 𝑟 ↑𝑟 𝑛 ) ) |
3 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
4 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
5 |
|
prssi |
⊢ ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) → { 0 , 1 } ⊆ ℕ0 ) |
6 |
3 4 5
|
mp2an |
⊢ { 0 , 1 } ⊆ ℕ0 |
7 |
6
|
a1i |
⊢ ( 𝜑 → { 0 , 1 } ⊆ ℕ0 ) |
8 |
2 1 7
|
brmptiunrelexpd |
⊢ ( 𝜑 → ( 𝐴 ( r* ‘ 𝑅 ) 𝐵 ↔ ∃ 𝑛 ∈ { 0 , 1 } 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ) ) |
9 |
|
oveq2 |
⊢ ( 𝑛 = 0 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 0 ) ) |
10 |
9
|
breqd |
⊢ ( 𝑛 = 0 → ( 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ↔ 𝐴 ( 𝑅 ↑𝑟 0 ) 𝐵 ) ) |
11 |
|
oveq2 |
⊢ ( 𝑛 = 1 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 1 ) ) |
12 |
11
|
breqd |
⊢ ( 𝑛 = 1 → ( 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ↔ 𝐴 ( 𝑅 ↑𝑟 1 ) 𝐵 ) ) |
13 |
10 12
|
rexprg |
⊢ ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) → ( ∃ 𝑛 ∈ { 0 , 1 } 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ↔ ( 𝐴 ( 𝑅 ↑𝑟 0 ) 𝐵 ∨ 𝐴 ( 𝑅 ↑𝑟 1 ) 𝐵 ) ) ) |
14 |
3 4 13
|
mp2an |
⊢ ( ∃ 𝑛 ∈ { 0 , 1 } 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ↔ ( 𝐴 ( 𝑅 ↑𝑟 0 ) 𝐵 ∨ 𝐴 ( 𝑅 ↑𝑟 1 ) 𝐵 ) ) |
15 |
8 14
|
syl6bb |
⊢ ( 𝜑 → ( 𝐴 ( r* ‘ 𝑅 ) 𝐵 ↔ ( 𝐴 ( 𝑅 ↑𝑟 0 ) 𝐵 ∨ 𝐴 ( 𝑅 ↑𝑟 1 ) 𝐵 ) ) ) |