bnj945

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
	Hypothesis	bnj945.1	$⊢ G = f \cup \{⟨n, C⟩\}$
	Assertion	bnj945	$⊢ (C \in V \land f Fn n \land p = suc n \land A \in n) \to G (A) = f (A)$

Proof

Step	Hyp	Ref	Expression
1		bnj945.1	$⊢ G = f \cup \{⟨n, C⟩\}$
2		fndm	$⊢ f Fn n \to dom f = n$
3	2	ad2antll	$⊢ (C \in V \land (p = suc n \land f Fn n)) \to dom f = n$
4	3	eleq2d	$⊢ (C \in V \land (p = suc n \land f Fn n)) \to (A \in dom f \leftrightarrow A \in n)$
5	4	pm5.32i	$⊢ ((C \in V \land (p = suc n \land f Fn n)) \land A \in dom f) \leftrightarrow ((C \in V \land (p = suc n \land f Fn n)) \land A \in n)$
6	1	bnj941	$⊢ C \in V \to ((p = suc n \land f Fn n) \to G Fn p)$
7	6	imp	$⊢ (C \in V \land (p = suc n \land f Fn n)) \to G Fn p$
8	7	fnfund	$⊢ (C \in V \land (p = suc n \land f Fn n)) \to Fun G$
9	1	bnj931	$⊢ f \subseteq G$
10	8 9	jctir	$⊢ (C \in V \land (p = suc n \land f Fn n)) \to (Fun G \land f \subseteq G)$
11	10	anim1i	$⊢ ((C \in V \land (p = suc n \land f Fn n)) \land A \in dom f) \to ((Fun G \land f \subseteq G) \land A \in dom f)$
12	5 11	sylbir	$⊢ ((C \in V \land (p = suc n \land f Fn n)) \land A \in n) \to ((Fun G \land f \subseteq G) \land A \in dom f)$
13		df-bnj17	$⊢ (C \in V \land f Fn n \land p = suc n \land A \in n) \leftrightarrow ((C \in V \land f Fn n \land p = suc n) \land A \in n)$
14		3ancomb	$⊢ (C \in V \land f Fn n \land p = suc n) \leftrightarrow (C \in V \land p = suc n \land f Fn n)$
15		3anass	$⊢ (C \in V \land p = suc n \land f Fn n) \leftrightarrow (C \in V \land (p = suc n \land f Fn n))$
16	14 15	bitri	$⊢ (C \in V \land f Fn n \land p = suc n) \leftrightarrow (C \in V \land (p = suc n \land f Fn n))$
17	16	anbi1i	$⊢ ((C \in V \land f Fn n \land p = suc n) \land A \in n) \leftrightarrow ((C \in V \land (p = suc n \land f Fn n)) \land A \in n)$
18	13 17	bitri	$⊢ (C \in V \land f Fn n \land p = suc n \land A \in n) \leftrightarrow ((C \in V \land (p = suc n \land f Fn n)) \land A \in n)$
19		df-3an	$⊢ (Fun G \land f \subseteq G \land A \in dom f) \leftrightarrow ((Fun G \land f \subseteq G) \land A \in dom f)$
20	12 18 19	3imtr4i	$⊢ (C \in V \land f Fn n \land p = suc n \land A \in n) \to (Fun G \land f \subseteq G \land A \in dom f)$
21		funssfv	$⊢ (Fun G \land f \subseteq G \land A \in dom f) \to G (A) = f (A)$
22	20 21	syl	$⊢ (C \in V \land f Fn n \land p = suc n \land A \in n) \to G (A) = f (A)$

Metamath Proof Explorer

Theorem bnj945

Proof