axcc4

Description: A version of axcc3 that uses wffs instead of classes. (Contributed by Mario Carneiro, 7-Apr-2013)

	Ref	Expression
Hypotheses	axcc4.1	$⊢ A \in V$
	axcc4.2	$⊢ N \approx ω$
	axcc4.3	$⊢ x = f (n) \to (φ \leftrightarrow ψ)$
Assertion	axcc4	$⊢ \forall n \in N \exists x \in A φ \to \exists f (f : N ⟶ A \land \forall n \in N ψ)$

Proof

Step	Hyp	Ref	Expression
1		axcc4.1	$⊢ A \in V$
2		axcc4.2	$⊢ N \approx ω$
3		axcc4.3	$⊢ x = f (n) \to (φ \leftrightarrow ψ)$
4	1	rabex	$⊢ \{x \in A \| φ\} \in V$
5	4 2	axcc3	$⊢ \exists f (f Fn N \land \forall n \in N (\{x \in A \| φ\} \neq \emptyset \to f (n) \in \{x \in A \| φ\}))$
6		rabn0	$⊢ \{x \in A \| φ\} \neq \emptyset \leftrightarrow \exists x \in A φ$
7		pm2.27	$⊢ \{x \in A \| φ\} \neq \emptyset \to ((\{x \in A \| φ\} \neq \emptyset \to f (n) \in \{x \in A \| φ\}) \to f (n) \in \{x \in A \| φ\})$
8	6 7	sylbir	$⊢ \exists x \in A φ \to ((\{x \in A \| φ\} \neq \emptyset \to f (n) \in \{x \in A \| φ\}) \to f (n) \in \{x \in A \| φ\})$
9	3	elrab	$⊢ f (n) \in \{x \in A \| φ\} \leftrightarrow (f (n) \in A \land ψ)$
10	8 9	imbitrdi	$⊢ \exists x \in A φ \to ((\{x \in A \| φ\} \neq \emptyset \to f (n) \in \{x \in A \| φ\}) \to (f (n) \in A \land ψ))$
11	10	ral2imi	$⊢ \forall n \in N \exists x \in A φ \to (\forall n \in N (\{x \in A \| φ\} \neq \emptyset \to f (n) \in \{x \in A \| φ\}) \to \forall n \in N (f (n) \in A \land ψ))$
12		simpl	$⊢ (f (n) \in A \land ψ) \to f (n) \in A$
13	12	ralimi	$⊢ \forall n \in N (f (n) \in A \land ψ) \to \forall n \in N f (n) \in A$
14	11 13	syl6	$⊢ \forall n \in N \exists x \in A φ \to (\forall n \in N (\{x \in A \| φ\} \neq \emptyset \to f (n) \in \{x \in A \| φ\}) \to \forall n \in N f (n) \in A)$
15	14	anim2d	$⊢ \forall n \in N \exists x \in A φ \to ((f Fn N \land \forall n \in N (\{x \in A \| φ\} \neq \emptyset \to f (n) \in \{x \in A \| φ\})) \to (f Fn N \land \forall n \in N f (n) \in A))$
16		ffnfv	$⊢ f : N ⟶ A \leftrightarrow (f Fn N \land \forall n \in N f (n) \in A)$
17	15 16	imbitrrdi	$⊢ \forall n \in N \exists x \in A φ \to ((f Fn N \land \forall n \in N (\{x \in A \| φ\} \neq \emptyset \to f (n) \in \{x \in A \| φ\})) \to f : N ⟶ A)$
18		simpr	$⊢ (f (n) \in A \land ψ) \to ψ$
19	18	ralimi	$⊢ \forall n \in N (f (n) \in A \land ψ) \to \forall n \in N ψ$
20	11 19	syl6	$⊢ \forall n \in N \exists x \in A φ \to (\forall n \in N (\{x \in A \| φ\} \neq \emptyset \to f (n) \in \{x \in A \| φ\}) \to \forall n \in N ψ)$
21	20	adantld	$⊢ \forall n \in N \exists x \in A φ \to ((f Fn N \land \forall n \in N (\{x \in A \| φ\} \neq \emptyset \to f (n) \in \{x \in A \| φ\})) \to \forall n \in N ψ)$
22	17 21	jcad	$⊢ \forall n \in N \exists x \in A φ \to ((f Fn N \land \forall n \in N (\{x \in A \| φ\} \neq \emptyset \to f (n) \in \{x \in A \| φ\})) \to (f : N ⟶ A \land \forall n \in N ψ))$
23	22	eximdv	$⊢ \forall n \in N \exists x \in A φ \to (\exists f (f Fn N \land \forall n \in N (\{x \in A \| φ\} \neq \emptyset \to f (n) \in \{x \in A \| φ\})) \to \exists f (f : N ⟶ A \land \forall n \in N ψ))$
24	5 23	mpi	$⊢ \forall n \in N \exists x \in A φ \to \exists f (f : N ⟶ A \land \forall n \in N ψ)$

Metamath Proof Explorer

Theorem axcc4

Proof