bnj906

Description: Property of _trCl . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

		Ref	Expression
	Assertion	bnj906	$⊢ (R FrSe A \land X \in A) \to pred (X, A, R) \subseteq trCl (X, A, R)$

Proof

Step	Hyp	Ref	Expression
1		1onn	$⊢ 1_{𝑜} \in ω$
2		1n0	$⊢ 1_{𝑜} \neq \emptyset$
3		eldifsn	$⊢ 1_{𝑜} \in (ω ∖ \{\emptyset\}) \leftrightarrow (1_{𝑜} \in ω \land 1_{𝑜} \neq \emptyset)$
4	1 2 3	mpbir2an	$⊢ 1_{𝑜} \in (ω ∖ \{\emptyset\})$
5	4	ne0ii	$⊢ ω ∖ \{\emptyset\} \neq \emptyset$
6		biid	$⊢ f (\emptyset) = pred (X, A, R) \leftrightarrow f (\emptyset) = pred (X, A, R)$
7		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))$
8		eqid	$⊢ ω ∖ \{\emptyset\} = ω ∖ \{\emptyset\}$
9	6 7 8	bnj852	$⊢ (R FrSe A \land X \in A) \to \forall n \in (ω ∖ \{\emptyset\}) \exists! f (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)))$
10		r19.2z	$⊢ (ω ∖ \{\emptyset\} \neq \emptyset \land \forall n \in (ω ∖ \{\emptyset\}) \exists! f (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)))) \to \exists n \in (ω ∖ \{\emptyset\}) \exists! f (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)))$
11	5 9 10	sylancr	$⊢ (R FrSe A \land X \in A) \to \exists n \in (ω ∖ \{\emptyset\}) \exists! f (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)))$
12		euex	$⊢ \exists! f (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))) \to \exists f (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)))$
13	11 12	bnj31	$⊢ (R FrSe A \land X \in A) \to \exists n \in (ω ∖ \{\emptyset\}) \exists f (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)))$
14		rexcom4	$⊢ \exists n \in (ω ∖ \{\emptyset\}) \exists f (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 \exists 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)))$
15	13 14	sylib	$⊢ (R FrSe A \land X \in A) \to \exists 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)))$
16		abid	$⊢ 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 \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)))$
17	15 16	bnj1198	$⊢ (R FrSe A \land X \in A) \to \exists f 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)))\}$
18		simp2	$⊢ (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))) \to f (\emptyset) = pred (X, A, R)$
19	18	reximi	$⊢ \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))) \to \exists n \in (ω ∖ \{\emptyset\}) f (\emptyset) = pred (X, A, R)$
20	16 19	sylbi	$⊢ 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)))\} \to \exists n \in (ω ∖ \{\emptyset\}) f (\emptyset) = pred (X, A, R)$
21		df-rex	$⊢ \exists n \in (ω ∖ \{\emptyset\}) f (\emptyset) = pred (X, A, R) \leftrightarrow \exists n (n \in (ω ∖ \{\emptyset\}) \land f (\emptyset) = pred (X, A, R))$
22		19.41v	$⊢ \exists n (n \in (ω ∖ \{\emptyset\}) \land f (\emptyset) = pred (X, A, R)) \leftrightarrow (\exists n n \in (ω ∖ \{\emptyset\}) \land f (\emptyset) = pred (X, A, R))$
23	22	simprbi	$⊢ \exists n (n \in (ω ∖ \{\emptyset\}) \land f (\emptyset) = pred (X, A, R)) \to f (\emptyset) = pred (X, A, R)$
24	21 23	sylbi	$⊢ \exists n \in (ω ∖ \{\emptyset\}) f (\emptyset) = pred (X, A, R) \to f (\emptyset) = pred (X, A, R)$
25	20 24	syl	$⊢ 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)))\} \to f (\emptyset) = pred (X, A, R)$
26		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)))\}$
27	8 26	bnj900	$⊢ 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)))\} \to \emptyset \in dom f$
28		fveq2	$⊢ i = \emptyset \to f (i) = f (\emptyset)$
29	28	ssiun2s	$⊢ \emptyset \in dom f \to f (\emptyset) \subseteq ⋃_{i \in dom f} f (i)$
30	27 29	syl	$⊢ 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)))\} \to f (\emptyset) \subseteq ⋃_{i \in dom f} f (i)$
31		ssiun2	$⊢ 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)))\} \to ⋃_{i \in dom f} f (i) \subseteq ⋃_{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)$
32	6 7 8 26	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)$
33	31 32	sseqtrrdi	$⊢ 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)))\} \to ⋃_{i \in dom f} f (i) \subseteq trCl (X, A, R)$
34	30 33	sstrd	$⊢ 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)))\} \to f (\emptyset) \subseteq trCl (X, A, R)$
35	25 34	eqsstrrd	$⊢ 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)))\} \to pred (X, A, R) \subseteq trCl (X, A, R)$
36	35	exlimiv	$⊢ \exists f 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)))\} \to pred (X, A, R) \subseteq trCl (X, A, R)$
37	17 36	syl	$⊢ (R FrSe A \land X \in A) \to pred (X, A, R) \subseteq trCl (X, A, R)$

Metamath Proof Explorer

Theorem bnj906

Proof