abrexdom

Description: An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Hypothesis	abrexdom.1	$⊢ y \in A \to \exists^{*} x φ$
	Assertion	abrexdom	$⊢ A \in V \to \{x \| \exists y \in A φ\} ≼ A$

Proof

Step	Hyp	Ref	Expression
1		abrexdom.1	$⊢ y \in A \to \exists^{*} x φ$
2		df-rex	$⊢ \exists y \in A φ \leftrightarrow \exists y (y \in A \land φ)$
3	2	abbii	$⊢ \{x \| \exists y \in A φ\} = \{x \| \exists y (y \in A \land φ)\}$
4		rnopab	$⊢ ran \{⟨y, x⟩ \| (y \in A \land φ)\} = \{x \| \exists y (y \in A \land φ)\}$
5	3 4	eqtr4i	$⊢ \{x \| \exists y \in A φ\} = ran \{⟨y, x⟩ \| (y \in A \land φ)\}$
6		dmopabss	$⊢ dom \{⟨y, x⟩ \| (y \in A \land φ)\} \subseteq A$
7		ssexg	$⊢ (dom \{⟨y, x⟩ \| (y \in A \land φ)\} \subseteq A \land A \in V) \to dom \{⟨y, x⟩ \| (y \in A \land φ)\} \in V$
8	6 7	mpan	$⊢ A \in V \to dom \{⟨y, x⟩ \| (y \in A \land φ)\} \in V$
9		funopab	$⊢ Fun \{⟨y, x⟩ \| (y \in A \land φ)\} \leftrightarrow \forall y \exists^{*} x (y \in A \land φ)$
10		moanimv	$⊢ \exists^{} x (y \in A \land φ) \leftrightarrow (y \in A \to \exists^{} x φ)$
11	1 10	mpbir	$⊢ \exists^{*} x (y \in A \land φ)$
12	9 11	mpgbir	$⊢ Fun \{⟨y, x⟩ \| (y \in A \land φ)\}$
13	12	a1i	$⊢ A \in V \to Fun \{⟨y, x⟩ \| (y \in A \land φ)\}$
14		funfn	$⊢ Fun \{⟨y, x⟩ \| (y \in A \land φ)\} \leftrightarrow \{⟨y, x⟩ \| (y \in A \land φ)\} Fn dom \{⟨y, x⟩ \| (y \in A \land φ)\}$
15	13 14	sylib	$⊢ A \in V \to \{⟨y, x⟩ \| (y \in A \land φ)\} Fn dom \{⟨y, x⟩ \| (y \in A \land φ)\}$
16		fnrndomg	$⊢ dom \{⟨y, x⟩ \| (y \in A \land φ)\} \in V \to (\{⟨y, x⟩ \| (y \in A \land φ)\} Fn dom \{⟨y, x⟩ \| (y \in A \land φ)\} \to ran \{⟨y, x⟩ \| (y \in A \land φ)\} ≼ dom \{⟨y, x⟩ \| (y \in A \land φ)\})$
17	8 15 16	sylc	$⊢ A \in V \to ran \{⟨y, x⟩ \| (y \in A \land φ)\} ≼ dom \{⟨y, x⟩ \| (y \in A \land φ)\}$
18		ssdomg	$⊢ A \in V \to (dom \{⟨y, x⟩ \| (y \in A \land φ)\} \subseteq A \to dom \{⟨y, x⟩ \| (y \in A \land φ)\} ≼ A)$
19	6 18	mpi	$⊢ A \in V \to dom \{⟨y, x⟩ \| (y \in A \land φ)\} ≼ A$
20		domtr	$⊢ (ran \{⟨y, x⟩ \| (y \in A \land φ)\} ≼ dom \{⟨y, x⟩ \| (y \in A \land φ)\} \land dom \{⟨y, x⟩ \| (y \in A \land φ)\} ≼ A) \to ran \{⟨y, x⟩ \| (y \in A \land φ)\} ≼ A$
21	17 19 20	syl2anc	$⊢ A \in V \to ran \{⟨y, x⟩ \| (y \in A \land φ)\} ≼ A$
22	5 21	eqbrtrid	$⊢ A \in V \to \{x \| \exists y \in A φ\} ≼ A$

Metamath Proof Explorer

Theorem abrexdom

Proof