bnj893

Description: Property of _trCl . Under certain conditions, the transitive closure of X in A by R is a set. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

		Ref	Expression
	Assertion	bnj893	$⊢ (R FrSe A \land X \in A) \to trCl (X, A, R) \in V$

Proof

Step	Hyp	Ref	Expression
1		biid	$⊢ f (\emptyset) = pred (X, A, R) \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		biid	$⊢ \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)) \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		eqid	$⊢ ω ∖ \{\emptyset\} = ω ∖ \{\emptyset\}$
4		eqid	$⊢ \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\} = \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\}$
5	1 2 3 4	bnj882	$⊢ trCl (X, A, R) = ⋃_{f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\}} ⋃_{i \in dom f} f (i)$
6		vex	$⊢ g \in V$
7		fveq1	$⊢ f = g \to f (\emptyset) = g (\emptyset)$
8	7	eqeq1d	$⊢ f = g \to (f (\emptyset) = pred (X, A, R) \leftrightarrow g (\emptyset) = pred (X, A, R))$
9	6 8	sbcie	$⊢ \underset{˙}{[} g / f \underset{˙}{]} f (\emptyset) = pred (X, A, R) \leftrightarrow g (\emptyset) = pred (X, A, R)$
10	9	bicomi	$⊢ g (\emptyset) = pred (X, A, R) \leftrightarrow \underset{˙}{[} g / f \underset{˙}{]} f (\emptyset) = pred (X, A, R)$
11		fveq1	$⊢ f = g \to f (suc i) = g (suc i)$
12		fveq1	$⊢ f = g \to f (i) = g (i)$
13	12	iuneq1d	$⊢ f = g \to ⋃_{y \in f (i)} pred (y, A, R) = ⋃_{y \in g (i)} pred (y, A, R)$
14	11 13	eqeq12d	$⊢ f = g \to (f (suc i) = ⋃_{y \in f (i)} pred (y, A, R) \leftrightarrow g (suc i) = ⋃_{y \in g (i)} pred (y, A, R))$
15	14	imbi2d	$⊢ f = g \to ((suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)) \leftrightarrow (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))$
16	15	ralbidv	$⊢ f = g \to (\forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)) \leftrightarrow \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))$
17	6 16	sbcie	$⊢ \underset{˙}{[} g / f \underset{˙}{]} \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)) \leftrightarrow \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R))$
18	17	bicomi	$⊢ \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)) \leftrightarrow \underset{˙}{[} g / f \underset{˙}{]} \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
19	4 10 18	bnj873	$⊢ \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\} = \{g \| \exists n \in (ω ∖ \{\emptyset\}) (g Fn n \land g (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))\}$
20	19	eleq2i	$⊢ f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\} \leftrightarrow f \in \{g \| \exists n \in (ω ∖ \{\emptyset\}) (g Fn n \land g (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))\}$
21	20	anbi1i	$⊢ (f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\} \land w \in ⋃_{i \in dom f} f (i)) \leftrightarrow (f \in \{g \| \exists n \in (ω ∖ \{\emptyset\}) (g Fn n \land g (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))\} \land w \in ⋃_{i \in dom f} f (i))$
22	21	rexbii2	$⊢ \exists f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\} w \in ⋃_{i \in dom f} f (i) \leftrightarrow \exists f \in \{g \| \exists n \in (ω ∖ \{\emptyset\}) (g Fn n \land g (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))\} w \in ⋃_{i \in dom f} f (i)$
23	22	abbii	$⊢ \{w \| \exists f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\} w \in ⋃_{i \in dom f} f (i)\} = \{w \| \exists f \in \{g \| \exists n \in (ω ∖ \{\emptyset\}) (g Fn n \land g (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))\} w \in ⋃_{i \in dom f} f (i)\}$
24		df-iun	$⊢ ⋃_{f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\}} ⋃_{i \in dom f} f (i) = \{w \| \exists f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\} w \in ⋃_{i \in dom f} f (i)\}$
25		df-iun	$⊢ ⋃_{f \in \{g \| \exists n \in (ω ∖ \{\emptyset\}) (g Fn n \land g (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))\}} ⋃_{i \in dom f} f (i) = \{w \| \exists f \in \{g \| \exists n \in (ω ∖ \{\emptyset\}) (g Fn n \land g (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))\} w \in ⋃_{i \in dom f} f (i)\}$
26	23 24 25	3eqtr4i	$⊢ ⋃_{f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\}} ⋃_{i \in dom f} f (i) = ⋃_{f \in \{g \| \exists n \in (ω ∖ \{\emptyset\}) (g Fn n \land g (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))\}} ⋃_{i \in dom f} f (i)$
27		biid	$⊢ g (\emptyset) = pred (X, A, R) \leftrightarrow g (\emptyset) = pred (X, A, R)$
28		biid	$⊢ \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)) \leftrightarrow \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R))$
29		eqid	$⊢ \{g \| \exists n \in (ω ∖ \{\emptyset\}) (g Fn n \land g (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))\} = \{g \| \exists n \in (ω ∖ \{\emptyset\}) (g Fn n \land g (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))\}$
30		biid	$⊢ (R FrSe A \land X \in A \land n \in (ω ∖ \{\emptyset\})) \leftrightarrow (R FrSe A \land X \in A \land n \in (ω ∖ \{\emptyset\}))$
31		biid	$⊢ (g Fn n \land g (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R))) \leftrightarrow (g Fn n \land g (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))$
32		biid	$⊢ \underset{˙}{[} z / g \underset{˙}{]} g (\emptyset) = pred (X, A, R) \leftrightarrow \underset{˙}{[} z / g \underset{˙}{]} g (\emptyset) = pred (X, A, R)$
33		biid	$⊢ \underset{˙}{[} z / g \underset{˙}{]} \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)) \leftrightarrow \underset{˙}{[} z / g \underset{˙}{]} \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R))$
34		biid	$⊢ \underset{˙}{[} z / g \underset{˙}{]} (g Fn n \land g (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R))) \leftrightarrow \underset{˙}{[} z / g \underset{˙}{]} (g Fn n \land g (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))$
35		biid	$⊢ (R FrSe A \land X \in A) \leftrightarrow (R FrSe A \land X \in A)$
36	27 28 3 29 30 31 32 33 34 35	bnj849	$⊢ (R FrSe A \land X \in A) \to \{g \| \exists n \in (ω ∖ \{\emptyset\}) (g Fn n \land g (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))\} \in V$
37		vex	$⊢ f \in V$
38	37	dmex	$⊢ dom f \in V$
39		fvex	$⊢ f (i) \in V$
40	38 39	iunex	$⊢ ⋃_{i \in dom f} f (i) \in V$
41	40	rgenw	$⊢ \forall f \in \{g \| \exists n \in (ω ∖ \{\emptyset\}) (g Fn n \land g (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))\} ⋃_{i \in dom f} f (i) \in V$
42		iunexg	$⊢ (\{g \| \exists n \in (ω ∖ \{\emptyset\}) (g Fn n \land g (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))\} \in V \land \forall f \in \{g \| \exists n \in (ω ∖ \{\emptyset\}) (g Fn n \land g (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))\} ⋃_{i \in dom f} f (i) \in V) \to ⋃_{f \in \{g \| \exists n \in (ω ∖ \{\emptyset\}) (g Fn n \land g (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))\}} ⋃_{i \in dom f} f (i) \in V$
43	36 41 42	sylancl	$⊢ (R FrSe A \land X \in A) \to ⋃_{f \in \{g \| \exists n \in (ω ∖ \{\emptyset\}) (g Fn n \land g (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))\}} ⋃_{i \in dom f} f (i) \in V$
44	26 43	eqeltrid	$⊢ (R FrSe A \land X \in A) \to ⋃_{f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\}} ⋃_{i \in dom f} f (i) \in V$
45	5 44	eqeltrid	$⊢ (R FrSe A \land X \in A) \to trCl (X, A, R) \in V$

Metamath Proof Explorer

Theorem bnj893

Proof