bnj579

Description: Technical lemma for bnj852 . 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	bnj579.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (x, A, R)$
	bnj579.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj579.3	$⊢ D = ω ∖ \{\emptyset\}$
Assertion	bnj579	$⊢ n \in D \to \exists^{*} f (f Fn n \land φ \land ψ)$

Proof

Step	Hyp	Ref	Expression
1		bnj579.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (x, A, R)$
2		bnj579.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj579.3	$⊢ D = ω ∖ \{\emptyset\}$
4		biid	$⊢ (f Fn n \land φ \land ψ) \leftrightarrow (f Fn n \land φ \land ψ)$
5		biid	$⊢ \underset{˙}{[} g / f \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} g / f \underset{˙}{]} φ$
6		biid	$⊢ \underset{˙}{[} g / f \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} g / f \underset{˙}{]} ψ$
7		biid	$⊢ \underset{˙}{[} g / f \underset{˙}{]} (f Fn n \land φ \land ψ) \leftrightarrow \underset{˙}{[} g / f \underset{˙}{]} (f Fn n \land φ \land ψ)$
8		biid	$⊢ ((n \in D \land (f Fn n \land φ \land ψ) \land \underset{˙}{[} g / f \underset{˙}{]} (f Fn n \land φ \land ψ)) \to f (j) = g (j)) \leftrightarrow ((n \in D \land (f Fn n \land φ \land ψ) \land \underset{˙}{[} g / f \underset{˙}{]} (f Fn n \land φ \land ψ)) \to f (j) = g (j))$
9		biid	$⊢ \forall k \in n (k E j \to \underset{˙}{[} k / j \underset{˙}{]} ((n \in D \land (f Fn n \land φ \land ψ) \land \underset{˙}{[} g / f \underset{˙}{]} (f Fn n \land φ \land ψ)) \to f (j) = g (j))) \leftrightarrow \forall k \in n (k E j \to \underset{˙}{[} k / j \underset{˙}{]} ((n \in D \land (f Fn n \land φ \land ψ) \land \underset{˙}{[} g / f \underset{˙}{]} (f Fn n \land φ \land ψ)) \to f (j) = g (j)))$
10	1 2 4 5 6 7 3 8 9	bnj580	$⊢ n \in D \to \exists^{*} f (f Fn n \land φ \land ψ)$

Metamath Proof Explorer

Theorem bnj579

Proof