bnj864

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj864.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
	bnj864.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj864.3	$⊢ D = ω ∖ \{\emptyset\}$
	bnj864.4	$⊢ χ \leftrightarrow (R FrSe A \land X \in A \land n \in D)$
	bnj864.5	$⊢ θ \leftrightarrow (f Fn n \land φ \land ψ)$
Assertion	bnj864	$⊢ χ \to \exists! f θ$

Proof

Step	Hyp	Ref	Expression
1		bnj864.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj864.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj864.3	$⊢ D = ω ∖ \{\emptyset\}$
4		bnj864.4	$⊢ χ \leftrightarrow (R FrSe A \land X \in A \land n \in D)$
5		bnj864.5	$⊢ θ \leftrightarrow (f Fn n \land φ \land ψ)$
6	1 2 3	bnj852	$⊢ (R FrSe A \land X \in A) \to \forall n \in D \exists! f (f Fn n \land φ \land ψ)$
7		df-ral	$⊢ \forall n \in D \exists! f (f Fn n \land φ \land ψ) \leftrightarrow \forall n (n \in D \to \exists! f (f Fn n \land φ \land ψ))$
8	7	imbi2i	$⊢ ((R FrSe A \land X \in A) \to \forall n \in D \exists! f (f Fn n \land φ \land ψ)) \leftrightarrow ((R FrSe A \land X \in A) \to \forall n (n \in D \to \exists! f (f Fn n \land φ \land ψ)))$
9		19.21v	$⊢ \forall n ((R FrSe A \land X \in A) \to (n \in D \to \exists! f (f Fn n \land φ \land ψ))) \leftrightarrow ((R FrSe A \land X \in A) \to \forall n (n \in D \to \exists! f (f Fn n \land φ \land ψ)))$
10		impexp	$⊢ (((R FrSe A \land X \in A) \land n \in D) \to \exists! f (f Fn n \land φ \land ψ)) \leftrightarrow ((R FrSe A \land X \in A) \to (n \in D \to \exists! f (f Fn n \land φ \land ψ)))$
11		df-3an	$⊢ (R FrSe A \land X \in A \land n \in D) \leftrightarrow ((R FrSe A \land X \in A) \land n \in D)$
12	11	bicomi	$⊢ ((R FrSe A \land X \in A) \land n \in D) \leftrightarrow (R FrSe A \land X \in A \land n \in D)$
13	12	imbi1i	$⊢ (((R FrSe A \land X \in A) \land n \in D) \to \exists! f (f Fn n \land φ \land ψ)) \leftrightarrow ((R FrSe A \land X \in A \land n \in D) \to \exists! f (f Fn n \land φ \land ψ))$
14	10 13	bitr3i	$⊢ ((R FrSe A \land X \in A) \to (n \in D \to \exists! f (f Fn n \land φ \land ψ))) \leftrightarrow ((R FrSe A \land X \in A \land n \in D) \to \exists! f (f Fn n \land φ \land ψ))$
15	14	albii	$⊢ \forall n ((R FrSe A \land X \in A) \to (n \in D \to \exists! f (f Fn n \land φ \land ψ))) \leftrightarrow \forall n ((R FrSe A \land X \in A \land n \in D) \to \exists! f (f Fn n \land φ \land ψ))$
16	8 9 15	3bitr2i	$⊢ ((R FrSe A \land X \in A) \to \forall n \in D \exists! f (f Fn n \land φ \land ψ)) \leftrightarrow \forall n ((R FrSe A \land X \in A \land n \in D) \to \exists! f (f Fn n \land φ \land ψ))$
17	6 16	mpbi	$⊢ \forall n ((R FrSe A \land X \in A \land n \in D) \to \exists! f (f Fn n \land φ \land ψ))$
18	17	spi	$⊢ (R FrSe A \land X \in A \land n \in D) \to \exists! f (f Fn n \land φ \land ψ)$
19	5	eubii	$⊢ \exists! f θ \leftrightarrow \exists! f (f Fn n \land φ \land ψ)$
20	18 4 19	3imtr4i	$⊢ χ \to \exists! f θ$

Metamath Proof Explorer

Theorem bnj864

Proof