Theorem trpredrec 9484

Description: A transitive predecessor of 𝑋 is either an immediate predecessor of 𝑋 or an immediate predecessor of a transitive predecessor of 𝑋. (Contributed by Scott Fenton, 9-May-2012.) (Revised by Mario Carneiro, 26-Jun-2015.)

Assertion

Ref	Expression
trpredrec	⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑌 ∈ TrPred(𝑅, 𝐴, 𝑋) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∨ ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧)))

Distinct variable groups:   𝑧,𝐴   𝑧,𝑅   𝑧,𝑋   𝑧,𝑌

Proof of Theorem trpredrec

Dummy variables 𝑎 𝑖 𝑗 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eltrpred 9473	. 2 ⊢ (𝑌 ∈ TrPred(𝑅, 𝐴, 𝑋) ↔ ∃𝑖 ∈ ω 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖))
2		nn0suc 7736	. . . 4 ⊢ (𝑖 ∈ ω → (𝑖 = ∅ ∨ ∃𝑗 ∈ ω 𝑖 = suc 𝑗))
3		fveq2 6771	. . . . . . . . . . 11 ⊢ (𝑖 = ∅ → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) = ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅))
4	3	eleq2d 2826	. . . . . . . . . 10 ⊢ (𝑖 = ∅ → (𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ↔ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅)))
5	4	anbi2d 629	. . . . . . . . 9 ⊢ (𝑖 = ∅ → (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) ↔ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅))))
6	5	biimpd 228	. . . . . . . 8 ⊢ (𝑖 = ∅ → (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) → ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅))))
7		setlikespec 6227	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑋) ∈ V)
8		fr0g 8258	. . . . . . . . . . 11 ⊢ (Pred(𝑅, 𝐴, 𝑋) ∈ V → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) = Pred(𝑅, 𝐴, 𝑋))
9	7, 8	syl 17	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) = Pred(𝑅, 𝐴, 𝑋))
10	9	eleq2d 2826	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) ↔ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋)))
11	10	biimpa 477	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅)) → 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋))
12	6, 11	syl6com 37	. . . . . . 7 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) → (𝑖 = ∅ → 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋)))
13		fveq2 6771	. . . . . . . . . . . . 13 ⊢ (𝑖 = suc 𝑗 → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) = ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗))
14	13	eleq2d 2826	. . . . . . . . . . . 12 ⊢ (𝑖 = suc 𝑗 → (𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ↔ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗)))
15	14	anbi2d 629	. . . . . . . . . . 11 ⊢ (𝑖 = suc 𝑗 → (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) ↔ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗))))
16	15	biimpd 228	. . . . . . . . . 10 ⊢ (𝑖 = suc 𝑗 → (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) → ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗))))
17		fvex 6784	. . . . . . . . . . . . . . . . 17 ⊢ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ∈ V
18		trpredlem1 9474	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Pred(𝑅, 𝐴, 𝑋) ∈ V → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐴)
19	7, 18	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐴)
20	19	sseld 3925	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) → 𝑧 ∈ 𝐴))
21		setlikespec 6227	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑧) ∈ V)
22	21	expcom 414	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 Se 𝐴 → (𝑧 ∈ 𝐴 → Pred(𝑅, 𝐴, 𝑧) ∈ V))
23	22	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑧 ∈ 𝐴 → Pred(𝑅, 𝐴, 𝑧) ∈ V))
24	20, 23	syld 47	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) → Pred(𝑅, 𝐴, 𝑧) ∈ V))
25	24	ralrimiv 3109	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧) ∈ V)
26		iunexg 7799	. . . . . . . . . . . . . . . . 17 ⊢ ((((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ∈ V ∧ ∀𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧) ∈ V) → ∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧) ∈ V)
27	17, 25, 26	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → ∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧) ∈ V)
28		nfcv 2909	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎Pred(𝑅, 𝐴, 𝑋)
29		nfcv 2909	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎𝑗
30		nfmpt1 5187	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑎(𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦))
31	30, 28	nfrdg 8236	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑎rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋))
32		nfcv 2909	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑎ω
33	31, 32	nfres 5892	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑎(rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)
34	33, 29	nffv 6781	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑎((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)
35		nfcv 2909	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑎Pred(𝑅, 𝐴, 𝑧)
36	34, 35	nfiun 4960	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧)
37		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ (rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω) = (rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)
38		predeq3 6205	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑧 → Pred(𝑅, 𝐴, 𝑦) = Pred(𝑅, 𝐴, 𝑧))
39	38	cbviunv 4975	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦) = ∪ 𝑧 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑧)
40		iuneq1 4946	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) → ∪ 𝑧 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑧) = ∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧))
41	39, 40	eqtrid 2792	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) → ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦) = ∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧))
42	28, 29, 36, 37, 41	frsucmpt 8260	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ ω ∧ ∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧) ∈ V) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗) = ∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧))
43	27, 42	sylan2 593	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ ω ∧ (𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗) = ∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧))
44	43	eleq2d 2826	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ ω ∧ (𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴)) → (𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗) ↔ 𝑌 ∈ ∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧)))
45	44	biimpd 228	. . . . . . . . . . . . 13 ⊢ ((𝑗 ∈ ω ∧ (𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴)) → (𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗) → 𝑌 ∈ ∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧)))
46	45	expimpd 454	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ω → (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗)) → 𝑌 ∈ ∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧)))
47		eliun 4934	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ ∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)𝑌 ∈ Pred(𝑅, 𝐴, 𝑧))
48		ssiun2 4982	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ω → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ ∪ 𝑗 ∈ ω ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗))
49		dftrpred2 9466	. . . . . . . . . . . . . . . . . 18 ⊢ TrPred(𝑅, 𝐴, 𝑋) = ∪ 𝑗 ∈ ω ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)
50	48, 49	sseqtrrdi 3977	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ω → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ TrPred(𝑅, 𝐴, 𝑋))
51	50	sseld 3925	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ω → (𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) → 𝑧 ∈ TrPred(𝑅, 𝐴, 𝑋)))
52		vex 3435	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑧 ∈ V
53	52	elpredim 6217	. . . . . . . . . . . . . . . . 17 ⊢ (𝑌 ∈ Pred(𝑅, 𝐴, 𝑧) → 𝑌𝑅𝑧)
54	53	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ω → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑧) → 𝑌𝑅𝑧))
55	51, 54	anim12d 609	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ω → ((𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑧)) → (𝑧 ∈ TrPred(𝑅, 𝐴, 𝑋) ∧ 𝑌𝑅𝑧)))
56	55	reximdv2 3201	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ω → (∃𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)𝑌 ∈ Pred(𝑅, 𝐴, 𝑧) → ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧))
57	56	com12 32	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)𝑌 ∈ Pred(𝑅, 𝐴, 𝑧) → (𝑗 ∈ ω → ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧))
58	47, 57	sylbi 216	. . . . . . . . . . . 12 ⊢ (𝑌 ∈ ∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧) → (𝑗 ∈ ω → ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧))
59	46, 58	syl6com 37	. . . . . . . . . . 11 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗)) → (𝑗 ∈ ω → (𝑗 ∈ ω → ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧)))
60	59	pm2.43d 53	. . . . . . . . . 10 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗)) → (𝑗 ∈ ω → ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧))
61	16, 60	syl6com 37	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) → (𝑖 = suc 𝑗 → (𝑗 ∈ ω → ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧)))
62	61	com23 86	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) → (𝑗 ∈ ω → (𝑖 = suc 𝑗 → ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧)))
63	62	rexlimdv 3214	. . . . . . 7 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) → (∃𝑗 ∈ ω 𝑖 = suc 𝑗 → ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧))
64	12, 63	orim12d 962	. . . . . 6 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) → ((𝑖 = ∅ ∨ ∃𝑗 ∈ ω 𝑖 = suc 𝑗) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∨ ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧)))
65	64	ex 413	. . . . 5 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) → ((𝑖 = ∅ ∨ ∃𝑗 ∈ ω 𝑖 = suc 𝑗) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∨ ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧))))
66	65	com23 86	. . . 4 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → ((𝑖 = ∅ ∨ ∃𝑗 ∈ ω 𝑖 = suc 𝑗) → (𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∨ ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧))))
67	2, 66	syl5 34	. . 3 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑖 ∈ ω → (𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∨ ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧))))
68	67	rexlimdv 3214	. 2 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (∃𝑖 ∈ ω 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∨ ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧)))
69	1, 68	syl5bi 241	1 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑌 ∈ TrPred(𝑅, 𝐴, 𝑋) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∨ ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧)))

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 844   = wceq 1542   ∈ wcel 2110  ∀wral 3066  ∃wrex 3067  Vcvv 3431   ⊆ wss 3892  ∅c0 4262  ∪ ciun 4930   class class class wbr 5079   ↦ cmpt 5162   Se wse 5543   ↾ cres 5592  Predcpred 6200  suc csuc 6267  ‘cfv 6432  ωcom 7706  reccrdg 8231  TrPredctrpred 9464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-rep 5214  ax-sep 5227  ax-nul 5234  ax-pr 5356  ax-un 7582

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-se 5546  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6201  df-ord 6268  df-on 6269  df-lim 6270  df-suc 6271  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-ov 7274  df-om 7707  df-2nd 7825  df-frecs 8088  df-wrecs 8119  df-recs 8193  df-rdg 8232  df-trpred 9465

This theorem is referenced by: (None)