trpredmintr - Mathbox for Scott Fenton

	Mathbox for Scott Fenton		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > trpredmintr		Structured version Visualization version GIF version

Theorem trpredmintr 32631

Description: The transitive predecessors form the smallest class transitive in 𝑅 and 𝐴. That is, if 𝐵 is another 𝑅, 𝐴 transitive class containing Pred(𝑅, 𝐴, 𝑋), then TrPred(𝑅, 𝐴, 𝑋) ⊆ 𝐵 (Contributed by Scott Fenton, 25-Apr-2012.) (Revised by Mario Carneiro, 26-Jun-2015.)

**Assertion**
Ref	Expression
trpredmintr	⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → TrPred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)

Distinct variable groups: 𝑦,𝐴 𝑦,𝐵 𝑦,𝑅 𝑦,𝑋

Proof of Theorem trpredmintr Dummy variables 𝑎 𝑐 𝑑 𝑖 𝑗 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dftrpred2 32619	. 2 ⊢ TrPred(𝑅, 𝐴, 𝑋) = ∪ 𝑖 ∈ ω ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)
2		fveq2 6504	. . . . . . . 8 ⊢ (𝑗 = ∅ → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) = ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅))
3	2	sseq1d 3890	. . . . . . 7 ⊢ (𝑗 = ∅ → (((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵 ↔ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) ⊆ 𝐵))
4	3	imbi2d 333	. . . . . 6 ⊢ (𝑗 = ∅ → ((((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵) ↔ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) ⊆ 𝐵)))
5		fveq2 6504	. . . . . . . 8 ⊢ (𝑗 = 𝑘 → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) = ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘))
6	5	sseq1d 3890	. . . . . . 7 ⊢ (𝑗 = 𝑘 → (((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵 ↔ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵))
7	6	imbi2d 333	. . . . . 6 ⊢ (𝑗 = 𝑘 → ((((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵) ↔ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)))
8		fveq2 6504	. . . . . . . 8 ⊢ (𝑗 = suc 𝑘 → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) = ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘))
9	8	sseq1d 3890	. . . . . . 7 ⊢ (𝑗 = suc 𝑘 → (((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵 ↔ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘) ⊆ 𝐵))
10	9	imbi2d 333	. . . . . 6 ⊢ (𝑗 = suc 𝑘 → ((((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵) ↔ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘) ⊆ 𝐵)))
11		fveq2 6504	. . . . . . . 8 ⊢ (𝑗 = 𝑖 → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) = ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖))
12	11	sseq1d 3890	. . . . . . 7 ⊢ (𝑗 = 𝑖 → (((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵 ↔ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵))
13	12	imbi2d 333	. . . . . 6 ⊢ (𝑗 = 𝑖 → ((((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵) ↔ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵)))
14		setlikespec 6012	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑋) ∈ V)
15		fr0g 7881	. . . . . . . . 9 ⊢ (Pred(𝑅, 𝐴, 𝑋) ∈ V → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) = Pred(𝑅, 𝐴, 𝑋))
16	14, 15	syl 17	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) = Pred(𝑅, 𝐴, 𝑋))
17	16	adantr 473	. . . . . . 7 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) = Pred(𝑅, 𝐴, 𝑋))
18		simprr 761	. . . . . . 7 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)
19	17, 18	eqsstrd 3897	. . . . . 6 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) ⊆ 𝐵)
20		fvex 6517	. . . . . . . . . . 11 ⊢ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ∈ V
21		trpredlem1 32627	. . . . . . . . . . . . . . . 16 ⊢ (Pred(𝑅, 𝐴, 𝑋) ∈ V → ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐴)
22	14, 21	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐴)
23	22	sseld 3859	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) → 𝑦 ∈ 𝐴))
24		setlikespec 6012	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑦) ∈ V)
25	24	expcom 406	. . . . . . . . . . . . . . 15 ⊢ (𝑅 Se 𝐴 → (𝑦 ∈ 𝐴 → Pred(𝑅, 𝐴, 𝑦) ∈ V))
26	25	adantl 474	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑦 ∈ 𝐴 → Pred(𝑅, 𝐴, 𝑦) ∈ V))
27	23, 26	syld 47	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) → Pred(𝑅, 𝐴, 𝑦) ∈ V))
28	27	ralrimiv 3133	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ∈ V)
29	28	ad2antrr 714	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵) → ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ∈ V)
30		iunexg 7482	. . . . . . . . . . 11 ⊢ ((((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ∈ V ∧ ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ∈ V) → ∪ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ∈ V)
31	20, 29, 30	sylancr 579	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵) → ∪ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ∈ V)
32		nfcv 2934	. . . . . . . . . . 11 ⊢ Ⅎ𝑎Pred(𝑅, 𝐴, 𝑋)
33		nfcv 2934	. . . . . . . . . . 11 ⊢ Ⅎ𝑎𝑘
34		nfcv 2934	. . . . . . . . . . 11 ⊢ Ⅎ𝑎∪ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦)
35		eqid 2780	. . . . . . . . . . 11 ⊢ (rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω) = (rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)
36		predeq3 5995	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑑 → Pred(𝑅, 𝐴, 𝑦) = Pred(𝑅, 𝐴, 𝑑))
37	36	cbviunv 4838	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦) = ∪ 𝑑 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑑)
38		iuneq1 4812	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑐 → ∪ 𝑑 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑑) = ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑))
39	37, 38	syl5eq 2828	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑐 → ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦) = ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑))
40	39	cbvmptv 5033	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)) = (𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑))
41		rdgeq1 7857	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)) = (𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)) → rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) = rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)))
42		reseq1 5694	. . . . . . . . . . . . . . 15 ⊢ (rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) = rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) → (rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω) = (rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω))
43	40, 41, 42	mp2b 10	. . . . . . . . . . . . . 14 ⊢ (rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω) = (rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)
44	43	fveq1i 6505	. . . . . . . . . . . . 13 ⊢ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) = ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)
45	44	eqeq2i 2792	. . . . . . . . . . . 12 ⊢ (𝑎 = ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ↔ 𝑎 = ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘))
46		iuneq1 4812	. . . . . . . . . . . 12 ⊢ (𝑎 = ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) → ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦) = ∪ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦))
47	45, 46	sylbi 209	. . . . . . . . . . 11 ⊢ (𝑎 = ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) → ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦) = ∪ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦))
48	32, 33, 34, 35, 47	frsucmpt 7883	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ω ∧ ∪ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ∈ V) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘) = ∪ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦))
49	31, 48	sylan2 584	. . . . . . . . 9 ⊢ ((𝑘 ∈ ω ∧ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘) = ∪ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦))
50	44	sseq1i 3887	. . . . . . . . . . . 12 ⊢ (((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵 ↔ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)
51	50	anbi2i 614	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵) ↔ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵))
52		nfv 1874	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦(𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴)
53		nfra1 3171	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵
54		nfv 1874	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵
55	53, 54	nfan 1863	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦(∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)
56	52, 55	nfan 1863	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵))
57		nfv 1874	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵
58	56, 57	nfan 1863	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)
59		ssel 3854	. . . . . . . . . . . . . 14 ⊢ (((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵 → (𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) → 𝑦 ∈ 𝐵))
60		rsp 3157	. . . . . . . . . . . . . . 15 ⊢ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → (𝑦 ∈ 𝐵 → Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵))
61	60	ad2antrl 716	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → (𝑦 ∈ 𝐵 → Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵))
62	59, 61	sylan9r 501	. . . . . . . . . . . . 13 ⊢ ((((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵) → (𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) → Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵))
63	58, 62	ralrimi 3168	. . . . . . . . . . . 12 ⊢ ((((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵) → ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵)
64	63	adantl 474	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ω ∧ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)) → ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵)
65	51, 64	sylan2b 585	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ω ∧ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)) → ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵)
66		iunss 4840	. . . . . . . . . 10 ⊢ (∪ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ↔ ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵)
67	65, 66	sylibr 226	. . . . . . . . 9 ⊢ ((𝑘 ∈ ω ∧ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)) → ∪ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵)
68	49, 67	eqsstrd 3897	. . . . . . . 8 ⊢ ((𝑘 ∈ ω ∧ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘) ⊆ 𝐵)
69	68	exp32 413	. . . . . . 7 ⊢ (𝑘 ∈ ω → (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → (((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵 → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘) ⊆ 𝐵)))
70	69	a2d 29	. . . . . 6 ⊢ (𝑘 ∈ ω → ((((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵) → (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘) ⊆ 𝐵)))
71	4, 7, 10, 13, 19, 70	finds 7429	. . . . 5 ⊢ (𝑖 ∈ ω → (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵))
72	71	com12 32	. . . 4 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → (𝑖 ∈ ω → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵))
73	72	ralrimiv 3133	. . 3 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ∀𝑖 ∈ ω ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵)
74		iunss 4840	. . 3 ⊢ (∪ 𝑖 ∈ ω ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵 ↔ ∀𝑖 ∈ ω ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵)
75	73, 74	sylibr 226	. 2 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ∪ 𝑖 ∈ ω ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵)
76	1, 75	syl5eqss 3907	1 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → TrPred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 387 = wceq 1508 ∈ wcel 2051 ∀wral 3090 Vcvv 3417 ⊆ wss 3831 ∅c0 4181 ∪ ciun 4797 ↦ cmpt 5013 Se wse 5368 ↾ cres 5413 Predcpred 5990 suc csuc 6036 ‘cfv 6193 ωcom 7402 reccrdg 7855 TrPredctrpred 32617

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2752 ax-rep 5053 ax-sep 5064 ax-nul 5071 ax-pow 5123 ax-pr 5190 ax-un 7285

This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3or 1070 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2551 df-eu 2589 df-clab 2761 df-cleq 2773 df-clel 2848 df-nfc 2920 df-ne 2970 df-ral 3095 df-rex 3096 df-reu 3097 df-rab 3099 df-v 3419 df-sbc 3684 df-csb 3789 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-pss 3847 df-nul 4182 df-if 4354 df-pw 4427 df-sn 4445 df-pr 4447 df-tp 4449 df-op 4451 df-uni 4718 df-iun 4799 df-br 4935 df-opab 4997 df-mpt 5014 df-tr 5036 df-id 5316 df-eprel 5321 df-po 5330 df-so 5331 df-fr 5370 df-se 5371 df-we 5372 df-xp 5417 df-rel 5418 df-cnv 5419 df-co 5420 df-dm 5421 df-rn 5422 df-res 5423 df-ima 5424 df-pred 5991 df-ord 6037 df-on 6038 df-lim 6039 df-suc 6040 df-iota 6157 df-fun 6195 df-fn 6196 df-f 6197 df-f1 6198 df-fo 6199 df-f1o 6200 df-fv 6201 df-om 7403 df-wrecs 7756 df-recs 7818 df-rdg 7856 df-trpred 32618

This theorem is referenced by: trpredelss 32632 dftrpred3g 32633 trpredpo 32635

W3C validator