trpred0

Description: The class of transitive predecessors is empty when A is empty. (Contributed by Scott Fenton, 30-Apr-2012)

		Ref	Expression
	Assertion	trpred0	$⊢ TrPred (R, \emptyset, X) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		dftrpred2	$⊢ TrPred (R, \emptyset, X) = ⋃_{i \in ω} ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, \emptyset, y)), Pred (R, \emptyset, X)) ↾}_{ω}) (i)$
2		pred0	$⊢ Pred (R, \emptyset, y) = \emptyset$
3	2	a1i	$⊢ y \in a \to Pred (R, \emptyset, y) = \emptyset$
4	3	iuneq2i	$⊢ ⋃_{y \in a} Pred (R, \emptyset, y) = ⋃_{y \in a} \emptyset$
5		iun0	$⊢ ⋃_{y \in a} \emptyset = \emptyset$
6	4 5	eqtri	$⊢ ⋃_{y \in a} Pred (R, \emptyset, y) = \emptyset$
7	6	mpteq2i	$⊢ (a \in V ⟼ ⋃_{y \in a} Pred (R, \emptyset, y)) = (a \in V ⟼ \emptyset)$
8		pred0	$⊢ Pred (R, \emptyset, X) = \emptyset$
9		rdgeq12	$⊢ ((a \in V ⟼ ⋃_{y \in a} Pred (R, \emptyset, y)) = (a \in V ⟼ \emptyset) \land Pred (R, \emptyset, X) = \emptyset) \to rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, \emptyset, y)), Pred (R, \emptyset, X)) = rec ((a \in V ⟼ \emptyset), \emptyset)$
10	7 8 9	mp2an	$⊢ rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, \emptyset, y)), Pred (R, \emptyset, X)) = rec ((a \in V ⟼ \emptyset), \emptyset)$
11	10	reseq1i	$⊢ {rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, \emptyset, y)), Pred (R, \emptyset, X)) ↾}_{ω} = {rec ((a \in V ⟼ \emptyset), \emptyset) ↾}_{ω}$
12	11	fveq1i	$⊢ ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, \emptyset, y)), Pred (R, \emptyset, X)) ↾}_{ω}) (i) = ({rec ((a \in V ⟼ \emptyset), \emptyset) ↾}_{ω}) (i)$
13		nn0suc	$⊢ i \in ω \to (i = \emptyset \lor \exists j \in ω i = suc j)$
14		fveq2	$⊢ i = \emptyset \to ({rec ((a \in V ⟼ \emptyset), \emptyset) ↾}_{ω}) (i) = ({rec ((a \in V ⟼ \emptyset), \emptyset) ↾}_{ω}) (\emptyset)$
15		0ex	$⊢ \emptyset \in V$
16		fr0g	$⊢ \emptyset \in V \to ({rec ((a \in V ⟼ \emptyset), \emptyset) ↾}_{ω}) (\emptyset) = \emptyset$
17	15 16	ax-mp	$⊢ ({rec ((a \in V ⟼ \emptyset), \emptyset) ↾}_{ω}) (\emptyset) = \emptyset$
18	14 17	eqtrdi	$⊢ i = \emptyset \to ({rec ((a \in V ⟼ \emptyset), \emptyset) ↾}_{ω}) (i) = \emptyset$
19		nfcv	$⊢ \underline{Ⅎ} a \emptyset$
20		nfcv	$⊢ \underline{Ⅎ} a j$
21		eqid	$⊢ {rec ((a \in V ⟼ \emptyset), \emptyset) ↾}_{ω} = {rec ((a \in V ⟼ \emptyset), \emptyset) ↾}_{ω}$
22		eqidd	$⊢ a = ({rec ((a \in V ⟼ \emptyset), \emptyset) ↾}_{ω}) (j) \to \emptyset = \emptyset$
23	19 20 19 21 22	frsucmpt	$⊢ (j \in ω \land \emptyset \in V) \to ({rec ((a \in V ⟼ \emptyset), \emptyset) ↾}_{ω}) (suc j) = \emptyset$
24	15 23	mpan2	$⊢ j \in ω \to ({rec ((a \in V ⟼ \emptyset), \emptyset) ↾}_{ω}) (suc j) = \emptyset$
25		fveqeq2	$⊢ i = suc j \to (({rec ((a \in V ⟼ \emptyset), \emptyset) ↾}_{ω}) (i) = \emptyset \leftrightarrow ({rec ((a \in V ⟼ \emptyset), \emptyset) ↾}_{ω}) (suc j) = \emptyset)$
26	24 25	syl5ibrcom	$⊢ j \in ω \to (i = suc j \to ({rec ((a \in V ⟼ \emptyset), \emptyset) ↾}_{ω}) (i) = \emptyset)$
27	26	rexlimiv	$⊢ \exists j \in ω i = suc j \to ({rec ((a \in V ⟼ \emptyset), \emptyset) ↾}_{ω}) (i) = \emptyset$
28	18 27	jaoi	$⊢ (i = \emptyset \lor \exists j \in ω i = suc j) \to ({rec ((a \in V ⟼ \emptyset), \emptyset) ↾}_{ω}) (i) = \emptyset$
29	13 28	syl	$⊢ i \in ω \to ({rec ((a \in V ⟼ \emptyset), \emptyset) ↾}_{ω}) (i) = \emptyset$
30	12 29	syl5eq	$⊢ i \in ω \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, \emptyset, y)), Pred (R, \emptyset, X)) ↾}_{ω}) (i) = \emptyset$
31	30	iuneq2i	$⊢ ⋃_{i \in ω} ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, \emptyset, y)), Pred (R, \emptyset, X)) ↾}_{ω}) (i) = ⋃_{i \in ω} \emptyset$
32		iun0	$⊢ ⋃_{i \in ω} \emptyset = \emptyset$
33	1 31 32	3eqtri	$⊢ TrPred (R, \emptyset, X) = \emptyset$

Metamath Proof Explorer

Theorem trpred0

Proof