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	$⊢ (B \in ℕ_{0} \land F : (1 \dots A) ⟶ (1 \dots B) \land \{a \in ({ℕ_{0}}^{(1 \dots A)}) \| φ\} \in Dioph (A)) \to \{b \in ({ℕ_{0}}^{(1 \dots B)}) \| \underset{˙}{[} (b \circ F) / a \underset{˙}{]} φ\} \in Dioph (B)$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ ((B \in ℕ_{0} \land F : (1 \dots A) ⟶ (1 \dots B)) \land b \in ({ℕ_{0}}^{(1 \dots B)})) \to b \in ({ℕ_{0}}^{(1 \dots B)})$
2		simplr	$⊢ ((B \in ℕ_{0} \land F : (1 \dots A) ⟶ (1 \dots B)) \land b \in ({ℕ_{0}}^{(1 \dots B)})) \to F : (1 \dots A) ⟶ (1 \dots B)$
3		ovex	$⊢ (1 \dots A) \in V$
4	3	mapco2	$⊢ (b \in ({ℕ_{0}}^{(1 \dots B)}) \land F : (1 \dots A) ⟶ (1 \dots B)) \to b \circ F \in ({ℕ_{0}}^{(1 \dots A)})$
5	1 2 4	syl2anc	$⊢ ((B \in ℕ_{0} \land F : (1 \dots A) ⟶ (1 \dots B)) \land b \in ({ℕ_{0}}^{(1 \dots B)})) \to b \circ F \in ({ℕ_{0}}^{(1 \dots A)})$
6	5	biantrurd	$⊢ ((B \in ℕ_{0} \land F : (1 \dots A) ⟶ (1 \dots B)) \land b \in ({ℕ_{0}}^{(1 \dots B)})) \to (\underset{˙}{[} (b \circ F) / a \underset{˙}{]} φ \leftrightarrow (b \circ F \in ({ℕ_{0}}^{(1 \dots A)}) \land \underset{˙}{[} (b \circ F) / a \underset{˙}{]} φ))$
7		nfcv	$⊢ \underline{Ⅎ} a ({ℕ_{0}}^{(1 \dots A)})$
8	7	elrabsf	$⊢ b \circ F \in \{a \in ({ℕ_{0}}^{(1 \dots A)}) \| φ\} \leftrightarrow (b \circ F \in ({ℕ_{0}}^{(1 \dots A)}) \land \underset{˙}{[} (b \circ F) / a \underset{˙}{]} φ)$
9	6 8	bitr4di	$⊢ ((B \in ℕ_{0} \land F : (1 \dots A) ⟶ (1 \dots B)) \land b \in ({ℕ_{0}}^{(1 \dots B)})) \to (\underset{˙}{[} (b \circ F) / a \underset{˙}{]} φ \leftrightarrow b \circ F \in \{a \in ({ℕ_{0}}^{(1 \dots A)}) \| φ\})$
10	9	rabbidva	$⊢ (B \in ℕ_{0} \land F : (1 \dots A) ⟶ (1 \dots B)) \to \{b \in ({ℕ_{0}}^{(1 \dots B)}) \| \underset{˙}{[} (b \circ F) / a \underset{˙}{]} φ\} = \{b \in ({ℕ_{0}}^{(1 \dots B)}) \| b \circ F \in \{a \in ({ℕ_{0}}^{(1 \dots A)}) \| φ\}\}$
11	10	3adant3	$⊢ (B \in ℕ_{0} \land F : (1 \dots A) ⟶ (1 \dots B) \land \{a \in ({ℕ_{0}}^{(1 \dots A)}) \| φ\} \in Dioph (A)) \to \{b \in ({ℕ_{0}}^{(1 \dots B)}) \| \underset{˙}{[} (b \circ F) / a \underset{˙}{]} φ\} = \{b \in ({ℕ_{0}}^{(1 \dots B)}) \| b \circ F \in \{a \in ({ℕ_{0}}^{(1 \dots A)}) \| φ\}\}$
12		diophren	$⊢ (\{a \in ({ℕ_{0}}^{(1 \dots A)}) \| φ\} \in Dioph (A) \land B \in ℕ_{0} \land F : (1 \dots A) ⟶ (1 \dots B)) \to \{b \in ({ℕ_{0}}^{(1 \dots B)}) \| b \circ F \in \{a \in ({ℕ_{0}}^{(1 \dots A)}) \| φ\}\} \in Dioph (B)$
13	12	3coml	$⊢ (B \in ℕ_{0} \land F : (1 \dots A) ⟶ (1 \dots B) \land \{a \in ({ℕ_{0}}^{(1 \dots A)}) \| φ\} \in Dioph (A)) \to \{b \in ({ℕ_{0}}^{(1 \dots B)}) \| b \circ F \in \{a \in ({ℕ_{0}}^{(1 \dots A)}) \| φ\}\} \in Dioph (B)$
14	11 13	eqeltrd	$⊢ (B \in ℕ_{0} \land F : (1 \dots A) ⟶ (1 \dots B) \land \{a \in ({ℕ_{0}}^{(1 \dots A)}) \| φ\} \in Dioph (A)) \to \{b \in ({ℕ_{0}}^{(1 \dots B)}) \| \underset{˙}{[} (b \circ F) / a \underset{˙}{]} φ\} \in Dioph (B)$