bnj929

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	bnj929.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
	bnj929.4	No typesetting found for \|- ( ph' <-> [. p / n ]. ph ) with typecode \|-
	bnj929.7	No typesetting found for \|- ( ph" <-> [. G / f ]. ph' ) with typecode \|-
	bnj929.10	$⊢ D = ω ∖ \{\emptyset\}$
	bnj929.13	$⊢ G = f \cup \{⟨n, C⟩\}$
	bnj929.50	$⊢ C \in V$
Assertion	bnj929	Could not format assertion : No typesetting found for \|- ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ph" ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		bnj929.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj929.4	Could not format ( ph' <-> [. p / n ]. ph ) : No typesetting found for \|- ( ph' <-> [. p / n ]. ph ) with typecode \|-
3		bnj929.7	Could not format ( ph" <-> [. G / f ]. ph' ) : No typesetting found for \|- ( ph" <-> [. G / f ]. ph' ) with typecode \|-
4		bnj929.10	$⊢ D = ω ∖ \{\emptyset\}$
5		bnj929.13	$⊢ G = f \cup \{⟨n, C⟩\}$
6		bnj929.50	$⊢ C \in V$
7		bnj645	$⊢ (n \in D \land p = suc n \land f Fn n \land φ) \to φ$
8		bnj334	$⊢ (n \in D \land p = suc n \land f Fn n \land φ) \leftrightarrow (f Fn n \land n \in D \land p = suc n \land φ)$
9		bnj257	$⊢ (f Fn n \land n \in D \land p = suc n \land φ) \leftrightarrow (f Fn n \land n \in D \land φ \land p = suc n)$
10	8 9	bitri	$⊢ (n \in D \land p = suc n \land f Fn n \land φ) \leftrightarrow (f Fn n \land n \in D \land φ \land p = suc n)$
11		bnj345	$⊢ (f Fn n \land n \in D \land φ \land p = suc n) \leftrightarrow (p = suc n \land f Fn n \land n \in D \land φ)$
12		bnj253	$⊢ (p = suc n \land f Fn n \land n \in D \land φ) \leftrightarrow ((p = suc n \land f Fn n) \land n \in D \land φ)$
13	10 11 12	3bitri	$⊢ (n \in D \land p = suc n \land f Fn n \land φ) \leftrightarrow ((p = suc n \land f Fn n) \land n \in D \land φ)$
14	13	simp1bi	$⊢ (n \in D \land p = suc n \land f Fn n \land φ) \to (p = suc n \land f Fn n)$
15	5 6	bnj927	$⊢ (p = suc n \land f Fn n) \to G Fn p$
16	15	bnj930	$⊢ (p = suc n \land f Fn n) \to Fun G$
17	14 16	syl	$⊢ (n \in D \land p = suc n \land f Fn n \land φ) \to Fun G$
18	5	bnj931	$⊢ f \subseteq G$
19	18	a1i	$⊢ (n \in D \land p = suc n \land f Fn n \land φ) \to f \subseteq G$
20		bnj268	$⊢ (n \in D \land f Fn n \land p = suc n \land φ) \leftrightarrow (n \in D \land p = suc n \land f Fn n \land φ)$
21		bnj253	$⊢ (n \in D \land f Fn n \land p = suc n \land φ) \leftrightarrow ((n \in D \land f Fn n) \land p = suc n \land φ)$
22	20 21	bitr3i	$⊢ (n \in D \land p = suc n \land f Fn n \land φ) \leftrightarrow ((n \in D \land f Fn n) \land p = suc n \land φ)$
23	22	simp1bi	$⊢ (n \in D \land p = suc n \land f Fn n \land φ) \to (n \in D \land f Fn n)$
24		fndm	$⊢ f Fn n \to dom f = n$
25	4	bnj529	$⊢ n \in D \to \emptyset \in n$
26		eleq2	$⊢ dom f = n \to (\emptyset \in dom f \leftrightarrow \emptyset \in n)$
27	26	biimpar	$⊢ (dom f = n \land \emptyset \in n) \to \emptyset \in dom f$
28	24 25 27	syl2anr	$⊢ (n \in D \land f Fn n) \to \emptyset \in dom f$
29	23 28	syl	$⊢ (n \in D \land p = suc n \land f Fn n \land φ) \to \emptyset \in dom f$
30	17 19 29	bnj1502	$⊢ (n \in D \land p = suc n \land f Fn n \land φ) \to G (\emptyset) = f (\emptyset)$
31	5	bnj918	$⊢ G \in V$
32	1 2 3 31	bnj934	Could not format ( ( ph /\ ( G ` (/) ) = ( f ` (/) ) ) -> ph" ) : No typesetting found for \|- ( ( ph /\ ( G ` (/) ) = ( f ` (/) ) ) -> ph" ) with typecode \|-
33	7 30 32	syl2anc	Could not format ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ph" ) : No typesetting found for \|- ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ph" ) with typecode \|-

Metamath Proof Explorer

Theorem bnj929

Proof