wfrdmcl

Description: Given F = wrecs ( R , A , X ) /\ X e. dom F , then its predecessor class is a subset of dom F . (Contributed by Scott Fenton, 21-Apr-2011)

		Ref	Expression
	Hypothesis	wfrlem6.1	$⊢ F = wrecs (R, A, G)$
	Assertion	wfrdmcl	$⊢ X \in dom F \to Pred (R, A, X) \subseteq dom F$

Proof

Step	Hyp	Ref	Expression
1		wfrlem6.1	$⊢ F = wrecs (R, A, G)$
2		df-wrecs	$⊢ wrecs (R, A, G) = ⋃ \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}$
3	1 2	eqtri	$⊢ F = ⋃ \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}$
4	3	dmeqi	$⊢ dom F = dom ⋃ \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}$
5		dmuni	$⊢ dom ⋃ \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\} = ⋃_{g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}} dom g$
6	4 5	eqtri	$⊢ dom F = ⋃_{g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}} dom g$
7	6	eleq2i	$⊢ X \in dom F \leftrightarrow X \in ⋃_{g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}} dom g$
8		eliun	$⊢ X \in ⋃_{g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}} dom g \leftrightarrow \exists g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\} X \in dom g$
9	7 8	bitri	$⊢ X \in dom F \leftrightarrow \exists g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\} X \in dom g$
10		eqid	$⊢ \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\} = \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}$
11	10	wfrlem1	$⊢ \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\} = \{g \| \exists z (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z) \land \forall w \in z g (w) = G ({g ↾}_{Pred (R, A, w)}))\}$
12	11	abeq2i	$⊢ g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\} \leftrightarrow \exists z (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z) \land \forall w \in z g (w) = G ({g ↾}_{Pred (R, A, w)}))$
13		predeq3	$⊢ w = X \to Pred (R, A, w) = Pred (R, A, X)$
14	13	sseq1d	$⊢ w = X \to (Pred (R, A, w) \subseteq z \leftrightarrow Pred (R, A, X) \subseteq z)$
15	14	rspccv	$⊢ \forall w \in z Pred (R, A, w) \subseteq z \to (X \in z \to Pred (R, A, X) \subseteq z)$
16	15	adantl	$⊢ (g Fn z \land \forall w \in z Pred (R, A, w) \subseteq z) \to (X \in z \to Pred (R, A, X) \subseteq z)$
17		fndm	$⊢ g Fn z \to dom g = z$
18	17	eleq2d	$⊢ g Fn z \to (X \in dom g \leftrightarrow X \in z)$
19	17	sseq2d	$⊢ g Fn z \to (Pred (R, A, X) \subseteq dom g \leftrightarrow Pred (R, A, X) \subseteq z)$
20	18 19	imbi12d	$⊢ g Fn z \to ((X \in dom g \to Pred (R, A, X) \subseteq dom g) \leftrightarrow (X \in z \to Pred (R, A, X) \subseteq z))$
21	20	adantr	$⊢ (g Fn z \land \forall w \in z Pred (R, A, w) \subseteq z) \to ((X \in dom g \to Pred (R, A, X) \subseteq dom g) \leftrightarrow (X \in z \to Pred (R, A, X) \subseteq z))$
22	16 21	mpbird	$⊢ (g Fn z \land \forall w \in z Pred (R, A, w) \subseteq z) \to (X \in dom g \to Pred (R, A, X) \subseteq dom g)$
23	22	adantrl	$⊢ (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)) \to (X \in dom g \to Pred (R, A, X) \subseteq dom g)$
24	23	3adant3	$⊢ (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z) \land \forall w \in z g (w) = G ({g ↾}_{Pred (R, A, w)})) \to (X \in dom g \to Pred (R, A, X) \subseteq dom g)$
25	24	exlimiv	$⊢ \exists z (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z) \land \forall w \in z g (w) = G ({g ↾}_{Pred (R, A, w)})) \to (X \in dom g \to Pred (R, A, X) \subseteq dom g)$
26	12 25	sylbi	$⊢ g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\} \to (X \in dom g \to Pred (R, A, X) \subseteq dom g)$
27	26	reximia	$⊢ \exists g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\} X \in dom g \to \exists g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\} Pred (R, A, X) \subseteq dom g$
28		ssiun	$⊢ \exists g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\} Pred (R, A, X) \subseteq dom g \to Pred (R, A, X) \subseteq ⋃_{g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}} dom g$
29	27 28	syl	$⊢ \exists g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\} X \in dom g \to Pred (R, A, X) \subseteq ⋃_{g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}} dom g$
30	9 29	sylbi	$⊢ X \in dom F \to Pred (R, A, X) \subseteq ⋃_{g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}} dom g$
31	30 6	sseqtrrdi	$⊢ X \in dom F \to Pred (R, A, X) \subseteq dom F$

Metamath Proof Explorer

Theorem wfrdmcl

Proof