bnj852

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	bnj852.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
	bnj852.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj852.3	$⊢ D = ω ∖ \{\emptyset\}$
Assertion	bnj852	$⊢ (R FrSe A \land X \in A) \to \forall n \in D \exists! f (f Fn n \land φ \land ψ)$

Proof

Step	Hyp	Ref	Expression
1		bnj852.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj852.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj852.3	$⊢ D = ω ∖ \{\emptyset\}$
4		elisset	$⊢ X \in A \to \exists x x = X$
5	4	adantl	$⊢ (R FrSe A \land X \in A) \to \exists x x = X$
6	5	ancri	$⊢ (R FrSe A \land X \in A) \to (\exists x x = X \land (R FrSe A \land X \in A))$
7	6	bnj534	$⊢ (R FrSe A \land X \in A) \to \exists x (x = X \land (R FrSe A \land X \in A))$
8		eleq1	$⊢ x = X \to (x \in A \leftrightarrow X \in A)$
9	8	anbi2d	$⊢ x = X \to ((R FrSe A \land x \in A) \leftrightarrow (R FrSe A \land X \in A))$
10	9	biimpar	$⊢ (x = X \land (R FrSe A \land X \in A)) \to (R FrSe A \land x \in A)$
11		biid	$⊢ \forall z \in D (z E n \to \underset{˙}{[} z / n \underset{˙}{]} ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ))) \leftrightarrow \forall z \in D (z E n \to \underset{˙}{[} z / n \underset{˙}{]} ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ)))$
12		omex	$⊢ ω \in V$
13		difexg	$⊢ ω \in V \to ω ∖ \{\emptyset\} \in V$
14	12 13	ax-mp	$⊢ ω ∖ \{\emptyset\} \in V$
15	3 14	eqeltri	$⊢ D \in V$
16		zfregfr	$⊢ E Fr D$
17	11 15 16	bnj157	$⊢ \forall n \in D (\forall z \in D (z E n \to \underset{˙}{[} z / n \underset{˙}{]} ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ))) \to ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ))) \to \forall n \in D ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ))$
18		biid	$⊢ f (\emptyset) = pred (x, A, R) \leftrightarrow f (\emptyset) = pred (x, A, R)$
19		biid	$⊢ ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ)) \leftrightarrow ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ))$
20	18 2 3 19 11	bnj153	$⊢ n = 1_{𝑜} \to ((n \in D \land \forall z \in D (z E n \to \underset{˙}{[} z / n \underset{˙}{]} ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ)))) \to ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ)))$
21	18 2 3 19 11	bnj601	$⊢ n \neq 1_{𝑜} \to ((n \in D \land \forall z \in D (z E n \to \underset{˙}{[} z / n \underset{˙}{]} ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ)))) \to ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ)))$
22	20 21	pm2.61ine	$⊢ (n \in D \land \forall z \in D (z E n \to \underset{˙}{[} z / n \underset{˙}{]} ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ)))) \to ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ))$
23	22	ex	$⊢ n \in D \to (\forall z \in D (z E n \to \underset{˙}{[} z / n \underset{˙}{]} ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ))) \to ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ)))$
24	17 23	mprg	$⊢ \forall n \in D ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ))$
25		r19.21v	$⊢ \forall n \in D ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ)) \leftrightarrow ((R FrSe A \land x \in A) \to \forall n \in D \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ))$
26	24 25	mpbi	$⊢ (R FrSe A \land x \in A) \to \forall n \in D \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ)$
27	10 26	syl	$⊢ (x = X \land (R FrSe A \land X \in A)) \to \forall n \in D \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ)$
28		bnj602	$⊢ x = X \to pred (x, A, R) = pred (X, A, R)$
29	28	eqeq2d	$⊢ x = X \to (f (\emptyset) = pred (x, A, R) \leftrightarrow f (\emptyset) = pred (X, A, R))$
30	29 1	bitr4di	$⊢ x = X \to (f (\emptyset) = pred (x, A, R) \leftrightarrow φ)$
31	30	3anbi2d	$⊢ x = X \to ((f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ) \leftrightarrow (f Fn n \land φ \land ψ))$
32	31	eubidv	$⊢ x = X \to (\exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ) \leftrightarrow \exists! f (f Fn n \land φ \land ψ))$
33	32	ralbidv	$⊢ x = X \to (\forall n \in D \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ) \leftrightarrow \forall n \in D \exists! f (f Fn n \land φ \land ψ))$
34	33	adantr	$⊢ (x = X \land (R FrSe A \land X \in A)) \to (\forall n \in D \exists! f (f Fn n \land f (\emptyset) = pred (x, A, R) \land ψ) \leftrightarrow \forall n \in D \exists! f (f Fn n \land φ \land ψ))$
35	27 34	mpbid	$⊢ (x = X \land (R FrSe A \land X \in A)) \to \forall n \in D \exists! f (f Fn n \land φ \land ψ)$
36	7 35	bnj593	$⊢ (R FrSe A \land X \in A) \to \exists x \forall n \in D \exists! f (f Fn n \land φ \land ψ)$
37	36	bnj937	$⊢ (R FrSe A \land X \in A) \to \forall n \in D \exists! f (f Fn n \land φ \land ψ)$

Metamath Proof Explorer

Theorem bnj852

Proof