bnj916

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

Proof

Step	Hyp	Ref	Expression
1		bnj916.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj916.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj916.3	$⊢ D = ω ∖ \{\emptyset\}$
4		bnj916.4	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
5		bnj916.5	$⊢ χ \leftrightarrow (f Fn n \land φ \land ψ)$
6		bnj256	$⊢ (n \in D \land (f Fn n \land φ \land ψ) \land i \in dom f \land y \in f (i)) \leftrightarrow ((n \in D \land (f Fn n \land φ \land ψ)) \land (i \in dom f \land y \in f (i)))$
7	6	2exbii	$⊢ \exists n \exists i (n \in D \land (f Fn n \land φ \land ψ) \land i \in dom f \land y \in f (i)) \leftrightarrow \exists n \exists i ((n \in D \land (f Fn n \land φ \land ψ)) \land (i \in dom f \land y \in f (i)))$
8		19.41v	$⊢ \exists n ((n \in D \land (f Fn n \land φ \land ψ)) \land \exists i (i \in dom f \land y \in f (i))) \leftrightarrow (\exists n (n \in D \land (f Fn n \land φ \land ψ)) \land \exists i (i \in dom f \land y \in f (i)))$
9		nfv	$⊢ Ⅎ i n \in D$
10	1 2	bnj911	$⊢ (f Fn n \land φ \land ψ) \to \forall i (f Fn n \land φ \land ψ)$
11	10	nf5i	$⊢ Ⅎ i (f Fn n \land φ \land ψ)$
12	9 11	nfan	$⊢ Ⅎ i (n \in D \land (f Fn n \land φ \land ψ))$
13	12	19.42	$⊢ \exists i ((n \in D \land (f Fn n \land φ \land ψ)) \land (i \in dom f \land y \in f (i))) \leftrightarrow ((n \in D \land (f Fn n \land φ \land ψ)) \land \exists i (i \in dom f \land y \in f (i)))$
14	13	exbii	$⊢ \exists n \exists i ((n \in D \land (f Fn n \land φ \land ψ)) \land (i \in dom f \land y \in f (i))) \leftrightarrow \exists n ((n \in D \land (f Fn n \land φ \land ψ)) \land \exists i (i \in dom f \land y \in f (i)))$
15		df-rex	$⊢ \exists n \in D (f Fn n \land φ \land ψ) \leftrightarrow \exists n (n \in D \land (f Fn n \land φ \land ψ))$
16		df-rex	$⊢ \exists i \in dom f y \in f (i) \leftrightarrow \exists i (i \in dom f \land y \in f (i))$
17	15 16	anbi12i	$⊢ (\exists n \in D (f Fn n \land φ \land ψ) \land \exists i \in dom f y \in f (i)) \leftrightarrow (\exists n (n \in D \land (f Fn n \land φ \land ψ)) \land \exists i (i \in dom f \land y \in f (i)))$
18	8 14 17	3bitr4i	$⊢ \exists n \exists i ((n \in D \land (f Fn n \land φ \land ψ)) \land (i \in dom f \land y \in f (i))) \leftrightarrow (\exists n \in D (f Fn n \land φ \land ψ) \land \exists i \in dom f y \in f (i))$
19	7 18	bitri	$⊢ \exists n \exists i (n \in D \land (f Fn n \land φ \land ψ) \land i \in dom f \land y \in f (i)) \leftrightarrow (\exists n \in D (f Fn n \land φ \land ψ) \land \exists i \in dom f y \in f (i))$
20	19	exbii	$⊢ \exists f \exists n \exists i (n \in D \land (f Fn n \land φ \land ψ) \land i \in dom f \land y \in f (i)) \leftrightarrow \exists f (\exists n \in D (f Fn n \land φ \land ψ) \land \exists i \in dom f y \in f (i))$
21	5	3anbi2i	$⊢ (n \in D \land χ \land i \in dom f) \leftrightarrow (n \in D \land (f Fn n \land φ \land ψ) \land i \in dom f)$
22	21	anbi1i	$⊢ ((n \in D \land χ \land i \in dom f) \land y \in f (i)) \leftrightarrow ((n \in D \land (f Fn n \land φ \land ψ) \land i \in dom f) \land y \in f (i))$
23		df-bnj17	$⊢ (n \in D \land χ \land i \in dom f \land y \in f (i)) \leftrightarrow ((n \in D \land χ \land i \in dom f) \land y \in f (i))$
24		df-bnj17	$⊢ (n \in D \land (f Fn n \land φ \land ψ) \land i \in dom f \land y \in f (i)) \leftrightarrow ((n \in D \land (f Fn n \land φ \land ψ) \land i \in dom f) \land y \in f (i))$
25	22 23 24	3bitr4i	$⊢ (n \in D \land χ \land i \in dom f \land y \in f (i)) \leftrightarrow (n \in D \land (f Fn n \land φ \land ψ) \land i \in dom f \land y \in f (i))$
26	25	3exbii	$⊢ \exists f \exists n \exists i (n \in D \land χ \land i \in dom f \land y \in f (i)) \leftrightarrow \exists f \exists n \exists i (n \in D \land (f Fn n \land φ \land ψ) \land i \in dom f \land y \in f (i))$
27	1 2 3 4	bnj882	$⊢ trCl (X, A, R) = ⋃_{f \in B} ⋃_{i \in dom f} f (i)$
28	27	eleq2i	$⊢ y \in trCl (X, A, R) \leftrightarrow y \in ⋃_{f \in B} ⋃_{i \in dom f} f (i)$
29		eliun	$⊢ y \in ⋃_{f \in B} ⋃_{i \in dom f} f (i) \leftrightarrow \exists f \in B y \in ⋃_{i \in dom f} f (i)$
30		eliun	$⊢ y \in ⋃_{i \in dom f} f (i) \leftrightarrow \exists i \in dom f y \in f (i)$
31	30	rexbii	$⊢ \exists f \in B y \in ⋃_{i \in dom f} f (i) \leftrightarrow \exists f \in B \exists i \in dom f y \in f (i)$
32	28 29 31	3bitri	$⊢ y \in trCl (X, A, R) \leftrightarrow \exists f \in B \exists i \in dom f y \in f (i)$
33		df-rex	$⊢ \exists f \in B \exists i \in dom f y \in f (i) \leftrightarrow \exists f (f \in B \land \exists i \in dom f y \in f (i))$
34	4	eqabri	$⊢ f \in B \leftrightarrow \exists n \in D (f Fn n \land φ \land ψ)$
35	34	anbi1i	$⊢ (f \in B \land \exists i \in dom f y \in f (i)) \leftrightarrow (\exists n \in D (f Fn n \land φ \land ψ) \land \exists i \in dom f y \in f (i))$
36	35	exbii	$⊢ \exists f (f \in B \land \exists i \in dom f y \in f (i)) \leftrightarrow \exists f (\exists n \in D (f Fn n \land φ \land ψ) \land \exists i \in dom f y \in f (i))$
37	32 33 36	3bitri	$⊢ y \in trCl (X, A, R) \leftrightarrow \exists f (\exists n \in D (f Fn n \land φ \land ψ) \land \exists i \in dom f y \in f (i))$
38	20 26 37	3bitr4ri	$⊢ y \in trCl (X, A, R) \leftrightarrow \exists f \exists n \exists i (n \in D \land χ \land i \in dom f \land y \in f (i))$
39		bnj643	$⊢ (n \in D \land χ \land i \in dom f \land y \in f (i)) \to χ$
40	5	bnj564	$⊢ χ \to dom f = n$
41	40	eleq2d	$⊢ χ \to (i \in dom f \leftrightarrow i \in n)$
42		anbi1	$⊢ (i \in dom f \leftrightarrow i \in n) \to ((i \in dom f \land (n \in D \land χ \land y \in f (i))) \leftrightarrow (i \in n \land (n \in D \land χ \land y \in f (i))))$
43		bnj334	$⊢ (n \in D \land χ \land i \in dom f \land y \in f (i)) \leftrightarrow (i \in dom f \land n \in D \land χ \land y \in f (i))$
44		bnj252	$⊢ (i \in dom f \land n \in D \land χ \land y \in f (i)) \leftrightarrow (i \in dom f \land (n \in D \land χ \land y \in f (i)))$
45	43 44	bitri	$⊢ (n \in D \land χ \land i \in dom f \land y \in f (i)) \leftrightarrow (i \in dom f \land (n \in D \land χ \land y \in f (i)))$
46		bnj334	$⊢ (n \in D \land χ \land i \in n \land y \in f (i)) \leftrightarrow (i \in n \land n \in D \land χ \land y \in f (i))$
47		bnj252	$⊢ (i \in n \land n \in D \land χ \land y \in f (i)) \leftrightarrow (i \in n \land (n \in D \land χ \land y \in f (i)))$
48	46 47	bitri	$⊢ (n \in D \land χ \land i \in n \land y \in f (i)) \leftrightarrow (i \in n \land (n \in D \land χ \land y \in f (i)))$
49	42 45 48	3bitr4g	$⊢ (i \in dom f \leftrightarrow i \in n) \to ((n \in D \land χ \land i \in dom f \land y \in f (i)) \leftrightarrow (n \in D \land χ \land i \in n \land y \in f (i)))$
50	39 41 49	3syl	$⊢ (n \in D \land χ \land i \in dom f \land y \in f (i)) \to ((n \in D \land χ \land i \in dom f \land y \in f (i)) \leftrightarrow (n \in D \land χ \land i \in n \land y \in f (i)))$
51	50	ibi	$⊢ (n \in D \land χ \land i \in dom f \land y \in f (i)) \to (n \in D \land χ \land i \in n \land y \in f (i))$
52	51	2eximi	$⊢ \exists n \exists i (n \in D \land χ \land i \in dom f \land y \in f (i)) \to \exists n \exists i (n \in D \land χ \land i \in n \land y \in f (i))$
53	52	eximi	$⊢ \exists f \exists n \exists i (n \in D \land χ \land i \in dom f \land y \in f (i)) \to \exists f \exists n \exists i (n \in D \land χ \land i \in n \land y \in f (i))$
54	38 53	sylbi	$⊢ y \in trCl (X, A, R) \to \exists f \exists n \exists i (n \in D \land χ \land i \in n \land y \in f (i))$

Metamath Proof Explorer

Theorem bnj916

Proof