bnj983

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

Proof

Step	Hyp	Ref	Expression
1		bnj983.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj983.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj983.3	$⊢ D = ω ∖ \{\emptyset\}$
4		bnj983.4	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
5		bnj983.5	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
6	1 2 3 4	bnj882	$⊢ trCl (X, A, R) = ⋃_{f \in B} ⋃_{i \in dom f} f (i)$
7	6	eleq2i	$⊢ Z \in trCl (X, A, R) \leftrightarrow Z \in ⋃_{f \in B} ⋃_{i \in dom f} f (i)$
8		eliun	$⊢ Z \in ⋃_{f \in B} ⋃_{i \in dom f} f (i) \leftrightarrow \exists f \in B Z \in ⋃_{i \in dom f} f (i)$
9		eliun	$⊢ Z \in ⋃_{i \in dom f} f (i) \leftrightarrow \exists i \in dom f Z \in f (i)$
10	9	rexbii	$⊢ \exists f \in B Z \in ⋃_{i \in dom f} f (i) \leftrightarrow \exists f \in B \exists i \in dom f Z \in f (i)$
11	8 10	bitri	$⊢ Z \in ⋃_{f \in B} ⋃_{i \in dom f} f (i) \leftrightarrow \exists f \in B \exists i \in dom f Z \in f (i)$
12		df-rex	$⊢ \exists f \in B \exists i \in dom f Z \in f (i) \leftrightarrow \exists f (f \in B \land \exists i \in dom f Z \in f (i))$
13	4	abeq2i	$⊢ f \in B \leftrightarrow \exists n \in D (f Fn n \land φ \land ψ)$
14	13	anbi1i	$⊢ (f \in B \land \exists i \in dom f Z \in f (i)) \leftrightarrow (\exists n \in D (f Fn n \land φ \land ψ) \land \exists i \in dom f Z \in f (i))$
15	14	exbii	$⊢ \exists f (f \in B \land \exists i \in dom f Z \in f (i)) \leftrightarrow \exists f (\exists n \in D (f Fn n \land φ \land ψ) \land \exists i \in dom f Z \in f (i))$
16	12 15	bitri	$⊢ \exists f \in B \exists i \in dom f Z \in f (i) \leftrightarrow \exists f (\exists n \in D (f Fn n \land φ \land ψ) \land \exists i \in dom f Z \in f (i))$
17	7 11 16	3bitri	$⊢ Z \in trCl (X, A, R) \leftrightarrow \exists f (\exists n \in D (f Fn n \land φ \land ψ) \land \exists i \in dom f Z \in f (i))$
18		bnj252	$⊢ (n \in D \land f Fn n \land φ \land ψ) \leftrightarrow (n \in D \land (f Fn n \land φ \land ψ))$
19	5 18	bitri	$⊢ χ \leftrightarrow (n \in D \land (f Fn n \land φ \land ψ))$
20	19	exbii	$⊢ \exists n χ \leftrightarrow \exists n (n \in D \land (f Fn n \land φ \land ψ))$
21	20	anbi1i	$⊢ (\exists n χ \land \exists i (i \in dom f \land Z \in f (i))) \leftrightarrow (\exists n (n \in D \land (f Fn n \land φ \land ψ)) \land \exists i (i \in dom f \land Z \in f (i)))$
22		df-rex	$⊢ \exists n \in D (f Fn n \land φ \land ψ) \leftrightarrow \exists n (n \in D \land (f Fn n \land φ \land ψ))$
23		df-rex	$⊢ \exists i \in dom f Z \in f (i) \leftrightarrow \exists i (i \in dom f \land Z \in f (i))$
24	22 23	anbi12i	$⊢ (\exists n \in D (f Fn n \land φ \land ψ) \land \exists i \in dom f Z \in f (i)) \leftrightarrow (\exists n (n \in D \land (f Fn n \land φ \land ψ)) \land \exists i (i \in dom f \land Z \in f (i)))$
25	21 24	bitr4i	$⊢ (\exists n χ \land \exists i (i \in dom f \land Z \in f (i))) \leftrightarrow (\exists n \in D (f Fn n \land φ \land ψ) \land \exists i \in dom f Z \in f (i))$
26	17 25	bnj133	$⊢ Z \in trCl (X, A, R) \leftrightarrow \exists f (\exists n χ \land \exists i (i \in dom f \land Z \in f (i)))$
27		19.41v	$⊢ \exists n (χ \land \exists i (i \in dom f \land Z \in f (i))) \leftrightarrow (\exists n χ \land \exists i (i \in dom f \land Z \in f (i)))$
28	26 27	bnj133	$⊢ Z \in trCl (X, A, R) \leftrightarrow \exists f \exists n (χ \land \exists i (i \in dom f \land Z \in f (i)))$
29	2	bnj1095	$⊢ ψ \to \forall i ψ$
30	29 5	bnj1096	$⊢ χ \to \forall i χ$
31	30	nf5i	$⊢ Ⅎ i χ$
32	31	19.42	$⊢ \exists i (χ \land (i \in dom f \land Z \in f (i))) \leftrightarrow (χ \land \exists i (i \in dom f \land Z \in f (i)))$
33	32	2exbii	$⊢ \exists f \exists n \exists i (χ \land (i \in dom f \land Z \in f (i))) \leftrightarrow \exists f \exists n (χ \land \exists i (i \in dom f \land Z \in f (i)))$
34	28 33	bitr4i	$⊢ Z \in trCl (X, A, R) \leftrightarrow \exists f \exists n \exists i (χ \land (i \in dom f \land Z \in f (i)))$
35		3anass	$⊢ (χ \land i \in dom f \land Z \in f (i)) \leftrightarrow (χ \land (i \in dom f \land Z \in f (i)))$
36	35	3exbii	$⊢ \exists f \exists n \exists i (χ \land i \in dom f \land Z \in f (i)) \leftrightarrow \exists f \exists n \exists i (χ \land (i \in dom f \land Z \in f (i)))$
37		fndm	$⊢ f Fn n \to dom f = n$
38	5 37	bnj770	$⊢ χ \to dom f = n$
39		eleq2	$⊢ dom f = n \to (i \in dom f \leftrightarrow i \in n)$
40	39	3anbi2d	$⊢ dom f = n \to ((χ \land i \in dom f \land Z \in f (i)) \leftrightarrow (χ \land i \in n \land Z \in f (i)))$
41	38 40	syl	$⊢ χ \to ((χ \land i \in dom f \land Z \in f (i)) \leftrightarrow (χ \land i \in n \land Z \in f (i)))$
42	41	3ad2ant1	$⊢ (χ \land i \in dom f \land Z \in f (i)) \to ((χ \land i \in dom f \land Z \in f (i)) \leftrightarrow (χ \land i \in n \land Z \in f (i)))$
43	42	ibi	$⊢ (χ \land i \in dom f \land Z \in f (i)) \to (χ \land i \in n \land Z \in f (i))$
44	41	3ad2ant1	$⊢ (χ \land i \in n \land Z \in f (i)) \to ((χ \land i \in dom f \land Z \in f (i)) \leftrightarrow (χ \land i \in n \land Z \in f (i)))$
45	44	ibir	$⊢ (χ \land i \in n \land Z \in f (i)) \to (χ \land i \in dom f \land Z \in f (i))$
46	43 45	impbii	$⊢ (χ \land i \in dom f \land Z \in f (i)) \leftrightarrow (χ \land i \in n \land Z \in f (i))$
47	46	3exbii	$⊢ \exists f \exists n \exists i (χ \land i \in dom f \land Z \in f (i)) \leftrightarrow \exists f \exists n \exists i (χ \land i \in n \land Z \in f (i))$
48	34 36 47	3bitr2i	$⊢ Z \in trCl (X, A, R) \leftrightarrow \exists f \exists n \exists i (χ \land i \in n \land Z \in f (i))$

Metamath Proof Explorer

Theorem bnj983

Proof