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 33074

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 33062	. 2 ⊢ TrPred(𝑅, 𝐴, 𝑋) = ∪ 𝑖 ∈ ω ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)
2		fveq2 6673	. . . . . . . 8 ⊢ (𝑗 = ∅ → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) = ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅))
3	2	sseq1d 4001	. . . . . . 7 ⊢ (𝑗 = ∅ → (((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵 ↔ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) ⊆ 𝐵))
4	3	imbi2d 343	. . . . . 6 ⊢ (𝑗 = ∅ → ((((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵) ↔ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) ⊆ 𝐵)))
5		fveq2 6673	. . . . . . . 8 ⊢ (𝑗 = 𝑘 → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) = ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘))
6	5	sseq1d 4001	. . . . . . 7 ⊢ (𝑗 = 𝑘 → (((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵 ↔ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵))
7	6	imbi2d 343	. . . . . 6 ⊢ (𝑗 = 𝑘 → ((((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵) ↔ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)))
8		fveq2 6673	. . . . . . . 8 ⊢ (𝑗 = suc 𝑘 → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) = ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘))
9	8	sseq1d 4001	. . . . . . 7 ⊢ (𝑗 = suc 𝑘 → (((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵 ↔ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘) ⊆ 𝐵))
10	9	imbi2d 343	. . . . . 6 ⊢ (𝑗 = suc 𝑘 → ((((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵) ↔ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘) ⊆ 𝐵)))
11		fveq2 6673	. . . . . . . 8 ⊢ (𝑗 = 𝑖 → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) = ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖))
12	11	sseq1d 4001	. . . . . . 7 ⊢ (𝑗 = 𝑖 → (((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵 ↔ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵))
13	12	imbi2d 343	. . . . . 6 ⊢ (𝑗 = 𝑖 → ((((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵) ↔ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵)))
14		setlikespec 6172	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑋) ∈ V)
15		fr0g 8074	. . . . . . . . 9 ⊢ (Pred(𝑅, 𝐴, 𝑋) ∈ V → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) = Pred(𝑅, 𝐴, 𝑋))
16	14, 15	syl 17	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) = Pred(𝑅, 𝐴, 𝑋))
17	16	adantr 483	. . . . . . 7 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) = Pred(𝑅, 𝐴, 𝑋))
18		simprr 771	. . . . . . 7 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)
19	17, 18	eqsstrd 4008	. . . . . 6 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) ⊆ 𝐵)
20		fvex 6686	. . . . . . . . . . 11 ⊢ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ∈ V
21		trpredlem1 33070	. . . . . . . . . . . . . . . 16 ⊢ (Pred(𝑅, 𝐴, 𝑋) ∈ V → ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐴)
22	14, 21	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐴)
23	22	sseld 3969	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) → 𝑦 ∈ 𝐴))
24		setlikespec 6172	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑦) ∈ V)
25	24	expcom 416	. . . . . . . . . . . . . . 15 ⊢ (𝑅 Se 𝐴 → (𝑦 ∈ 𝐴 → Pred(𝑅, 𝐴, 𝑦) ∈ V))
26	25	adantl 484	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑦 ∈ 𝐴 → Pred(𝑅, 𝐴, 𝑦) ∈ V))
27	23, 26	syld 47	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) → Pred(𝑅, 𝐴, 𝑦) ∈ V))
28	27	ralrimiv 3184	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ∈ V)
29	28	ad2antrr 724	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵) → ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ∈ V)
30		iunexg 7667	. . . . . . . . . . 11 ⊢ ((((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ∈ V ∧ ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ∈ V) → ∪ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ∈ V)
31	20, 29, 30	sylancr 589	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵) → ∪ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ∈ V)
32		nfcv 2980	. . . . . . . . . . 11 ⊢ Ⅎ𝑎Pred(𝑅, 𝐴, 𝑋)
33		nfcv 2980	. . . . . . . . . . 11 ⊢ Ⅎ𝑎𝑘
34		nfcv 2980	. . . . . . . . . . 11 ⊢ Ⅎ𝑎∪ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦)
35		eqid 2824	. . . . . . . . . . 11 ⊢ (rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω) = (rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)
36		predeq3 6155	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑑 → Pred(𝑅, 𝐴, 𝑦) = Pred(𝑅, 𝐴, 𝑑))
37	36	cbviunv 4968	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦) = ∪ 𝑑 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑑)
38		iuneq1 4938	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑐 → ∪ 𝑑 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑑) = ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑))
39	37, 38	syl5eq 2871	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑐 → ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦) = ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑))
40	39	cbvmptv 5172	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)) = (𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑))
41		rdgeq1 8050	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)) = (𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)) → rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) = rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)))
42		reseq1 5850	. . . . . . . . . . . . . . 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 6674	. . . . . . . . . . . . 13 ⊢ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) = ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)
45	44	eqeq2i 2837	. . . . . . . . . . . 12 ⊢ (𝑎 = ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ↔ 𝑎 = ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘))
46		iuneq1 4938	. . . . . . . . . . . 12 ⊢ (𝑎 = ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) → ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦) = ∪ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦))
47	45, 46	sylbi 219	. . . . . . . . . . 11 ⊢ (𝑎 = ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) → ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦) = ∪ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦))
48	32, 33, 34, 35, 47	frsucmpt 8076	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ω ∧ ∪ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ∈ V) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘) = ∪ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦))
49	31, 48	sylan2 594	. . . . . . . . 9 ⊢ ((𝑘 ∈ ω ∧ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘) = ∪ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦))
50	44	sseq1i 3998	. . . . . . . . . . . 12 ⊢ (((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵 ↔ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)
51	50	anbi2i 624	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵) ↔ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵))
52		nfv 1914	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦(𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴)
53		nfra1 3222	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵
54		nfv 1914	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵
55	53, 54	nfan 1899	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦(∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)
56	52, 55	nfan 1899	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵))
57		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵
58	56, 57	nfan 1899	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)
59		ssel 3964	. . . . . . . . . . . . . 14 ⊢ (((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵 → (𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) → 𝑦 ∈ 𝐵))
60		rsp 3208	. . . . . . . . . . . . . . 15 ⊢ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → (𝑦 ∈ 𝐵 → Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵))
61	60	ad2antrl 726	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → (𝑦 ∈ 𝐵 → Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵))
62	59, 61	sylan9r 511	. . . . . . . . . . . . 13 ⊢ ((((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵) → (𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) → Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵))
63	58, 62	ralrimi 3219	. . . . . . . . . . . 12 ⊢ ((((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵) → ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵)
64	63	adantl 484	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ω ∧ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)) → ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵)
65	51, 64	sylan2b 595	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ω ∧ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)) → ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵)
66		iunss 4972	. . . . . . . . . 10 ⊢ (∪ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ↔ ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵)
67	65, 66	sylibr 236	. . . . . . . . 9 ⊢ ((𝑘 ∈ ω ∧ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)) → ∪ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ ∪ 𝑑 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵)
68	49, 67	eqsstrd 4008	. . . . . . . 8 ⊢ ((𝑘 ∈ ω ∧ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘) ⊆ 𝐵)
69	68	exp32 423	. . . . . . 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 7611	. . . . 5 ⊢ (𝑖 ∈ ω → (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵))
72	71	com12 32	. . . 4 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → (𝑖 ∈ ω → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵))
73	72	ralrimiv 3184	. . 3 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ∀𝑖 ∈ ω ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵)
74		iunss 4972	. . 3 ⊢ (∪ 𝑖 ∈ ω ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵 ↔ ∀𝑖 ∈ ω ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵)
75	73, 74	sylibr 236	. 2 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ∪ 𝑖 ∈ ω ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵)
76	1, 75	eqsstrid 4018	1 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → TrPred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 398 = wceq 1536 ∈ wcel 2113 ∀wral 3141 Vcvv 3497 ⊆ wss 3939 ∅c0 4294 ∪ ciun 4922 ↦ cmpt 5149 Se wse 5515 ↾ cres 5560 Predcpred 6150 suc csuc 6196 ‘cfv 6358 ωcom 7583 reccrdg 8048 TrPredctrpred 33060

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-rep 5193 ax-sep 5206 ax-nul 5213 ax-pow 5269 ax-pr 5333 ax-un 7464

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-ne 3020 df-ral 3146 df-rex 3147 df-reu 3148 df-rab 3150 df-v 3499 df-sbc 3776 df-csb 3887 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-pss 3957 df-nul 4295 df-if 4471 df-pw 4544 df-sn 4571 df-pr 4573 df-tp 4575 df-op 4577 df-uni 4842 df-iun 4924 df-br 5070 df-opab 5132 df-mpt 5150 df-tr 5176 df-id 5463 df-eprel 5468 df-po 5477 df-so 5478 df-fr 5517 df-se 5518 df-we 5519 df-xp 5564 df-rel 5565 df-cnv 5566 df-co 5567 df-dm 5568 df-rn 5569 df-res 5570 df-ima 5571 df-pred 6151 df-ord 6197 df-on 6198 df-lim 6199 df-suc 6200 df-iota 6317 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-om 7584 df-wrecs 7950 df-recs 8011 df-rdg 8049 df-trpred 33061

This theorem is referenced by: trpredelss 33075 dftrpred3g 33076 trpredpo 33078

W3C validator