Metamath Proof Explorer

Theorem rabrenfdioph

Description: Change variable numbers in a Diophantine class abstraction using explicit substitution. (Contributed by Stefan O'Rear, 17-Oct-2014)

Ref Expression
Assertion rabrenfdioph ( ( 𝐵 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝐴 ) ⟶ ( 1 ... 𝐵 ) ∧ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝐴 ) ) → { 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) ∣ [ ( 𝑏 ∘ 𝐹 ) / 𝑎 ] 𝜑 } ∈ ( Dioph ‘ 𝐵 ) )

Proof

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 ‘ 𝐵 ) )