Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
⊢ ( ( ( 𝐵 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝐴 ) ⟶ ( 1 ... 𝐵 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) ) → 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) ) |
2 |
|
simplr |
⊢ ( ( ( 𝐵 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝐴 ) ⟶ ( 1 ... 𝐵 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) ) → 𝐹 : ( 1 ... 𝐴 ) ⟶ ( 1 ... 𝐵 ) ) |
3 |
|
ovex |
⊢ ( 1 ... 𝐴 ) ∈ V |
4 |
3
|
mapco2 |
⊢ ( ( 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) ∧ 𝐹 : ( 1 ... 𝐴 ) ⟶ ( 1 ... 𝐵 ) ) → ( 𝑏 ∘ 𝐹 ) ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ) |
5 |
1 2 4
|
syl2anc |
⊢ ( ( ( 𝐵 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝐴 ) ⟶ ( 1 ... 𝐵 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) ) → ( 𝑏 ∘ 𝐹 ) ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ) |
6 |
5
|
biantrurd |
⊢ ( ( ( 𝐵 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝐴 ) ⟶ ( 1 ... 𝐵 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) ) → ( [ ( 𝑏 ∘ 𝐹 ) / 𝑎 ] 𝜑 ↔ ( ( 𝑏 ∘ 𝐹 ) ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∧ [ ( 𝑏 ∘ 𝐹 ) / 𝑎 ] 𝜑 ) ) ) |
7 |
|
nfcv |
⊢ Ⅎ 𝑎 ( ℕ0 ↑m ( 1 ... 𝐴 ) ) |
8 |
7
|
elrabsf |
⊢ ( ( 𝑏 ∘ 𝐹 ) ∈ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∣ 𝜑 } ↔ ( ( 𝑏 ∘ 𝐹 ) ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∧ [ ( 𝑏 ∘ 𝐹 ) / 𝑎 ] 𝜑 ) ) |
9 |
6 8
|
bitr4di |
⊢ ( ( ( 𝐵 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝐴 ) ⟶ ( 1 ... 𝐵 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) ) → ( [ ( 𝑏 ∘ 𝐹 ) / 𝑎 ] 𝜑 ↔ ( 𝑏 ∘ 𝐹 ) ∈ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∣ 𝜑 } ) ) |
10 |
9
|
rabbidva |
⊢ ( ( 𝐵 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝐴 ) ⟶ ( 1 ... 𝐵 ) ) → { 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) ∣ [ ( 𝑏 ∘ 𝐹 ) / 𝑎 ] 𝜑 } = { 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) ∣ ( 𝑏 ∘ 𝐹 ) ∈ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∣ 𝜑 } } ) |
11 |
10
|
3adant3 |
⊢ ( ( 𝐵 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝐴 ) ⟶ ( 1 ... 𝐵 ) ∧ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝐴 ) ) → { 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) ∣ [ ( 𝑏 ∘ 𝐹 ) / 𝑎 ] 𝜑 } = { 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) ∣ ( 𝑏 ∘ 𝐹 ) ∈ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∣ 𝜑 } } ) |
12 |
|
diophren |
⊢ ( ( { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝐴 ) ∧ 𝐵 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝐴 ) ⟶ ( 1 ... 𝐵 ) ) → { 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) ∣ ( 𝑏 ∘ 𝐹 ) ∈ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∣ 𝜑 } } ∈ ( Dioph ‘ 𝐵 ) ) |
13 |
12
|
3coml |
⊢ ( ( 𝐵 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝐴 ) ⟶ ( 1 ... 𝐵 ) ∧ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝐴 ) ) → { 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) ∣ ( 𝑏 ∘ 𝐹 ) ∈ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∣ 𝜑 } } ∈ ( Dioph ‘ 𝐵 ) ) |
14 |
11 13
|
eqeltrd |
⊢ ( ( 𝐵 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝐴 ) ⟶ ( 1 ... 𝐵 ) ∧ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝐴 ) ) → { 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) ∣ [ ( 𝑏 ∘ 𝐹 ) / 𝑎 ] 𝜑 } ∈ ( Dioph ‘ 𝐵 ) ) |