bnj1014

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	bnj1014.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
	bnj1014.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj1014.13	$⊢ D = ω ∖ \{\emptyset\}$
	bnj1014.14	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
Assertion	bnj1014	$⊢ (g \in B \land j \in dom g) \to g (j) \subseteq trCl (X, A, R)$

Proof

Step	Hyp	Ref	Expression
1		bnj1014.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj1014.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj1014.13	$⊢ D = ω ∖ \{\emptyset\}$
4		bnj1014.14	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
5		nfcv	$⊢ \underline{Ⅎ} i D$
6	1 2	bnj911	$⊢ (f Fn n \land φ \land ψ) \to \forall i (f Fn n \land φ \land ψ)$
7	6	nf5i	$⊢ Ⅎ i (f Fn n \land φ \land ψ)$
8	5 7	nfrexw	$⊢ Ⅎ i \exists n \in D (f Fn n \land φ \land ψ)$
9	8	nfab	$⊢ \underline{Ⅎ} i \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
10	4 9	nfcxfr	$⊢ \underline{Ⅎ} i B$
11	10	nfcri	$⊢ Ⅎ i g \in B$
12		nfv	$⊢ Ⅎ i j \in dom g$
13	11 12	nfan	$⊢ Ⅎ i (g \in B \land j \in dom g)$
14		nfv	$⊢ Ⅎ i g (j) \subseteq trCl (X, A, R)$
15	13 14	nfim	$⊢ Ⅎ i ((g \in B \land j \in dom g) \to g (j) \subseteq trCl (X, A, R))$
16	15	nf5ri	$⊢ ((g \in B \land j \in dom g) \to g (j) \subseteq trCl (X, A, R)) \to \forall i ((g \in B \land j \in dom g) \to g (j) \subseteq trCl (X, A, R))$
17		eleq1w	$⊢ j = i \to (j \in dom g \leftrightarrow i \in dom g)$
18	17	anbi2d	$⊢ j = i \to ((g \in B \land j \in dom g) \leftrightarrow (g \in B \land i \in dom g))$
19		fveq2	$⊢ j = i \to g (j) = g (i)$
20	19	sseq1d	$⊢ j = i \to (g (j) \subseteq trCl (X, A, R) \leftrightarrow g (i) \subseteq trCl (X, A, R))$
21	18 20	imbi12d	$⊢ j = i \to (((g \in B \land j \in dom g) \to g (j) \subseteq trCl (X, A, R)) \leftrightarrow ((g \in B \land i \in dom g) \to g (i) \subseteq trCl (X, A, R)))$
22	21	equcoms	$⊢ i = j \to (((g \in B \land j \in dom g) \to g (j) \subseteq trCl (X, A, R)) \leftrightarrow ((g \in B \land i \in dom g) \to g (i) \subseteq trCl (X, A, R)))$
23	4	bnj1317	$⊢ g \in B \to \forall f g \in B$
24	23	nf5i	$⊢ Ⅎ f g \in B$
25		nfv	$⊢ Ⅎ f i \in dom g$
26	24 25	nfan	$⊢ Ⅎ f (g \in B \land i \in dom g)$
27		nfv	$⊢ Ⅎ f g (i) \subseteq trCl (X, A, R)$
28	26 27	nfim	$⊢ Ⅎ f ((g \in B \land i \in dom g) \to g (i) \subseteq trCl (X, A, R))$
29		eleq1w	$⊢ f = g \to (f \in B \leftrightarrow g \in B)$
30		dmeq	$⊢ f = g \to dom f = dom g$
31	30	eleq2d	$⊢ f = g \to (i \in dom f \leftrightarrow i \in dom g)$
32	29 31	anbi12d	$⊢ f = g \to ((f \in B \land i \in dom f) \leftrightarrow (g \in B \land i \in dom g))$
33		fveq1	$⊢ f = g \to f (i) = g (i)$
34	33	sseq1d	$⊢ f = g \to (f (i) \subseteq trCl (X, A, R) \leftrightarrow g (i) \subseteq trCl (X, A, R))$
35	32 34	imbi12d	$⊢ f = g \to (((f \in B \land i \in dom f) \to f (i) \subseteq trCl (X, A, R)) \leftrightarrow ((g \in B \land i \in dom g) \to g (i) \subseteq trCl (X, A, R)))$
36		ssiun2	$⊢ i \in dom f \to f (i) \subseteq ⋃_{i \in dom f} f (i)$
37		ssiun2	$⊢ f \in B \to ⋃_{i \in dom f} f (i) \subseteq ⋃_{f \in B} ⋃_{i \in dom f} f (i)$
38	1 2 3 4	bnj882	$⊢ trCl (X, A, R) = ⋃_{f \in B} ⋃_{i \in dom f} f (i)$
39	37 38	sseqtrrdi	$⊢ f \in B \to ⋃_{i \in dom f} f (i) \subseteq trCl (X, A, R)$
40	36 39	sylan9ssr	$⊢ (f \in B \land i \in dom f) \to f (i) \subseteq trCl (X, A, R)$
41	28 35 40	chvarfv	$⊢ (g \in B \land i \in dom g) \to g (i) \subseteq trCl (X, A, R)$
42	22 41	speivw	$⊢ \exists i ((g \in B \land j \in dom g) \to g (j) \subseteq trCl (X, A, R))$
43	16 42	bnj1131	$⊢ (g \in B \land j \in dom g) \to g (j) \subseteq trCl (X, A, R)$

Metamath Proof Explorer

Theorem bnj1014

Proof