bnj1123

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	bnj1123.4	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj1123.3	$⊢ K = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
	bnj1123.1	$⊢ η \leftrightarrow ((f \in K \land i \in dom f) \to f (i) \subseteq B)$
	bnj1123.2	No typesetting found for \|- ( et' <-> [. j / i ]. et ) with typecode \|-
Assertion	bnj1123	Could not format assertion : No typesetting found for \|- ( et' <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		bnj1123.4	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
2		bnj1123.3	$⊢ K = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
3		bnj1123.1	$⊢ η \leftrightarrow ((f \in K \land i \in dom f) \to f (i) \subseteq B)$
4		bnj1123.2	Could not format ( et' <-> [. j / i ]. et ) : No typesetting found for \|- ( et' <-> [. j / i ]. et ) with typecode \|-
5	3	sbcbii	$⊢ \underset{˙}{[} j / i \underset{˙}{]} η \leftrightarrow \underset{˙}{[} j / i \underset{˙}{]} ((f \in K \land i \in dom f) \to f (i) \subseteq B)$
6		nfcv	$⊢ \underline{Ⅎ} i D$
7		nfv	$⊢ Ⅎ i f Fn n$
8		nfv	$⊢ Ⅎ i φ$
9	1	bnj1095	$⊢ ψ \to \forall i ψ$
10	9	nf5i	$⊢ Ⅎ i ψ$
11	7 8 10	nf3an	$⊢ Ⅎ i (f Fn n \land φ \land ψ)$
12	6 11	nfrexw	$⊢ Ⅎ i \exists n \in D (f Fn n \land φ \land ψ)$
13	12	nfab	$⊢ \underline{Ⅎ} i \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
14	2 13	nfcxfr	$⊢ \underline{Ⅎ} i K$
15	14	nfcri	$⊢ Ⅎ i f \in K$
16		nfv	$⊢ Ⅎ i j \in dom f$
17	15 16	nfan	$⊢ Ⅎ i (f \in K \land j \in dom f)$
18		nfv	$⊢ Ⅎ i f (j) \subseteq B$
19	17 18	nfim	$⊢ Ⅎ i ((f \in K \land j \in dom f) \to f (j) \subseteq B)$
20		eleq1w	$⊢ i = j \to (i \in dom f \leftrightarrow j \in dom f)$
21	20	anbi2d	$⊢ i = j \to ((f \in K \land i \in dom f) \leftrightarrow (f \in K \land j \in dom f))$
22		fveq2	$⊢ i = j \to f (i) = f (j)$
23	22	sseq1d	$⊢ i = j \to (f (i) \subseteq B \leftrightarrow f (j) \subseteq B)$
24	21 23	imbi12d	$⊢ i = j \to (((f \in K \land i \in dom f) \to f (i) \subseteq B) \leftrightarrow ((f \in K \land j \in dom f) \to f (j) \subseteq B))$
25	19 24	sbciegf	$⊢ j \in V \to (\underset{˙}{[} j / i \underset{˙}{]} ((f \in K \land i \in dom f) \to f (i) \subseteq B) \leftrightarrow ((f \in K \land j \in dom f) \to f (j) \subseteq B))$
26	25	elv	$⊢ \underset{˙}{[} j / i \underset{˙}{]} ((f \in K \land i \in dom f) \to f (i) \subseteq B) \leftrightarrow ((f \in K \land j \in dom f) \to f (j) \subseteq B)$
27	4 5 26	3bitri	Could not format ( et' <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) ) : No typesetting found for \|- ( et' <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) ) with typecode \|-

Metamath Proof Explorer

Theorem bnj1123

Proof