trpredrec

Description: If Y is an R , A transitive predecessor, then it is either an immediate predecessor or there is a transitive predecessor between Y and X . (Contributed by Scott Fenton, 9-May-2012) (Revised by Mario Carneiro, 26-Jun-2015)

		Ref	Expression
	Assertion	trpredrec	$⊢ (X \in A \land R Se A) \to (Y \in TrPred (R, A, X) \to (Y \in Pred (R, A, X) \lor \exists z \in TrPred (R, A, X) Y R z))$

Proof

Step	Hyp	Ref	Expression
1		eltrpred	$⊢ Y \in TrPred (R, A, X) \leftrightarrow \exists i \in ω Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)$
2		nn0suc	$⊢ i \in ω \to (i = \emptyset \lor \exists j \in ω i = suc j)$
3		fveq2	$⊢ i = \emptyset \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) = ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (\emptyset)$
4	3	eleq2d	$⊢ i = \emptyset \to (Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \leftrightarrow Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (\emptyset))$
5	4	anbi2d	$⊢ i = \emptyset \to (((X \in A \land R Se A) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)) \leftrightarrow ((X \in A \land R Se A) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (\emptyset)))$
6	5	biimpd	$⊢ i = \emptyset \to (((X \in A \land R Se A) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)) \to ((X \in A \land R Se A) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (\emptyset)))$
7		setlikespec	$⊢ (X \in A \land R Se A) \to Pred (R, A, X) \in V$
8		fr0g	$⊢ Pred (R, A, X) \in V \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (\emptyset) = Pred (R, A, X)$
9	7 8	syl	$⊢ (X \in A \land R Se A) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (\emptyset) = Pred (R, A, X)$
10	9	eleq2d	$⊢ (X \in A \land R Se A) \to (Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (\emptyset) \leftrightarrow Y \in Pred (R, A, X))$
11	10	biimpa	$⊢ ((X \in A \land R Se A) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (\emptyset)) \to Y \in Pred (R, A, X)$
12	6 11	syl6com	$⊢ ((X \in A \land R Se A) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)) \to (i = \emptyset \to Y \in Pred (R, A, X))$
13		fveq2	$⊢ i = suc j \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) = ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j)$
14	13	eleq2d	$⊢ i = suc j \to (Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \leftrightarrow Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j))$
15	14	anbi2d	$⊢ i = suc j \to (((X \in A \land R Se A) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)) \leftrightarrow ((X \in A \land R Se A) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j)))$
16	15	biimpd	$⊢ i = suc j \to (((X \in A \land R Se A) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)) \to ((X \in A \land R Se A) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j)))$
17		fvex	$⊢ ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \in V$
18		trpredlem1	$⊢ Pred (R, A, X) \in V \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \subseteq A$
19	7 18	syl	$⊢ (X \in A \land R Se A) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \subseteq A$
20	19	sseld	$⊢ (X \in A \land R Se A) \to (z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \to z \in A)$
21		setlikespec	$⊢ (z \in A \land R Se A) \to Pred (R, A, z) \in V$
22	21	expcom	$⊢ R Se A \to (z \in A \to Pred (R, A, z) \in V)$
23	22	adantl	$⊢ (X \in A \land R Se A) \to (z \in A \to Pred (R, A, z) \in V)$
24	20 23	syld	$⊢ (X \in A \land R Se A) \to (z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \to Pred (R, A, z) \in V)$
25	24	ralrimiv	$⊢ (X \in A \land R Se A) \to \forall z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) Pred (R, A, z) \in V$
26		iunexg	$⊢ (({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \in V \land \forall z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) Pred (R, A, z) \in V) \to ⋃_{z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, z) \in V$
27	17 25 26	sylancr	$⊢ (X \in A \land R Se A) \to ⋃_{z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, z) \in V$
28		nfcv	$⊢ \underline{Ⅎ} a Pred (R, A, X)$
29		nfcv	$⊢ \underline{Ⅎ} a j$
30		nfmpt1	$⊢ \underline{Ⅎ} a (a \in V ⟼ ⋃_{y \in a} Pred (R, A, y))$
31	30 28	nfrdg	$⊢ \underline{Ⅎ} a rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X))$
32		nfcv	$⊢ \underline{Ⅎ} a ω$
33	31 32	nfres	$⊢ \underline{Ⅎ} a ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω})$
34	33 29	nffv	$⊢ \underline{Ⅎ} a ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)$
35		nfcv	$⊢ \underline{Ⅎ} a Pred (R, A, z)$
36	34 35	nfiun	$⊢ \underline{Ⅎ} a ⋃_{z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, z)$
37		eqid	$⊢ {rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω} = {rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}$
38		predeq3	$⊢ y = z \to Pred (R, A, y) = Pred (R, A, z)$
39	38	cbviunv	$⊢ ⋃_{y \in a} Pred (R, A, y) = ⋃_{z \in a} Pred (R, A, z)$
40		iuneq1	$⊢ a = ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \to ⋃_{z \in a} Pred (R, A, z) = ⋃_{z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, z)$
41	39 40	syl5eq	$⊢ a = ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \to ⋃_{y \in a} Pred (R, A, y) = ⋃_{z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, z)$
42	28 29 36 37 41	frsucmpt	$⊢ (j \in ω \land ⋃_{z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, z) \in V) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j) = ⋃_{z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, z)$
43	27 42	sylan2	$⊢ (j \in ω \land (X \in A \land R Se A)) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j) = ⋃_{z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, z)$
44	43	eleq2d	$⊢ (j \in ω \land (X \in A \land R Se A)) \to (Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j) \leftrightarrow Y \in ⋃_{z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, z))$
45	44	biimpd	$⊢ (j \in ω \land (X \in A \land R Se A)) \to (Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j) \to Y \in ⋃_{z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, z))$
46	45	expimpd	$⊢ j \in ω \to (((X \in A \land R Se A) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j)) \to Y \in ⋃_{z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, z))$
47		eliun	$⊢ Y \in ⋃_{z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, z) \leftrightarrow \exists z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) Y \in Pred (R, A, z)$
48		ssiun2	$⊢ j \in ω \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \subseteq ⋃_{j \in ω} ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)$
49		dftrpred2	$⊢ TrPred (R, A, X) = ⋃_{j \in ω} ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)$
50	48 49	sseqtrrdi	$⊢ j \in ω \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \subseteq TrPred (R, A, X)$
51	50	sseld	$⊢ j \in ω \to (z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \to z \in TrPred (R, A, X))$
52		vex	$⊢ z \in V$
53	52	elpredim	$⊢ Y \in Pred (R, A, z) \to Y R z$
54	53	a1i	$⊢ j \in ω \to (Y \in Pred (R, A, z) \to Y R z)$
55	51 54	anim12d	$⊢ j \in ω \to ((z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \land Y \in Pred (R, A, z)) \to (z \in TrPred (R, A, X) \land Y R z))$
56	55	reximdv2	$⊢ j \in ω \to (\exists z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) Y \in Pred (R, A, z) \to \exists z \in TrPred (R, A, X) Y R z)$
57	56	com12	$⊢ \exists z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) Y \in Pred (R, A, z) \to (j \in ω \to \exists z \in TrPred (R, A, X) Y R z)$
58	47 57	sylbi	$⊢ Y \in ⋃_{z \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, z) \to (j \in ω \to \exists z \in TrPred (R, A, X) Y R z)$
59	46 58	syl6com	$⊢ ((X \in A \land R Se A) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j)) \to (j \in ω \to (j \in ω \to \exists z \in TrPred (R, A, X) Y R z))$
60	59	pm2.43d	$⊢ ((X \in A \land R Se A) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j)) \to (j \in ω \to \exists z \in TrPred (R, A, X) Y R z)$
61	16 60	syl6com	$⊢ ((X \in A \land R Se A) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)) \to (i = suc j \to (j \in ω \to \exists z \in TrPred (R, A, X) Y R z))$
62	61	com23	$⊢ ((X \in A \land R Se A) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)) \to (j \in ω \to (i = suc j \to \exists z \in TrPred (R, A, X) Y R z))$
63	62	rexlimdv	$⊢ ((X \in A \land R Se A) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)) \to (\exists j \in ω i = suc j \to \exists z \in TrPred (R, A, X) Y R z)$
64	12 63	orim12d	$⊢ ((X \in A \land R Se A) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)) \to ((i = \emptyset \lor \exists j \in ω i = suc j) \to (Y \in Pred (R, A, X) \lor \exists z \in TrPred (R, A, X) Y R z))$
65	64	ex	$⊢ (X \in A \land R Se A) \to (Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \to ((i = \emptyset \lor \exists j \in ω i = suc j) \to (Y \in Pred (R, A, X) \lor \exists z \in TrPred (R, A, X) Y R z)))$
66	65	com23	$⊢ (X \in A \land R Se A) \to ((i = \emptyset \lor \exists j \in ω i = suc j) \to (Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \to (Y \in Pred (R, A, X) \lor \exists z \in TrPred (R, A, X) Y R z)))$
67	2 66	syl5	$⊢ (X \in A \land R Se A) \to (i \in ω \to (Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \to (Y \in Pred (R, A, X) \lor \exists z \in TrPred (R, A, X) Y R z)))$
68	67	rexlimdv	$⊢ (X \in A \land R Se A) \to (\exists i \in ω Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \to (Y \in Pred (R, A, X) \lor \exists z \in TrPred (R, A, X) Y R z))$
69	1 68	syl5bi	$⊢ (X \in A \land R Se A) \to (Y \in TrPred (R, A, X) \to (Y \in Pred (R, A, X) \lor \exists z \in TrPred (R, A, X) Y R z))$

Metamath Proof Explorer

Theorem trpredrec

Proof