Theorem trpredpred

Description: Assuming it exists, the predecessor class is a subset of the transitive predecessors. (Contributed by Scott Fenton, 18-Feb-2011)

	Ref	Expression
Assertion	trpredpred	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		fr0g	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
2		frfnom	⊢ ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) Fn ω
3		peano1	⊢ ∅ ∈ ω
4		fnbrfvb	⊢ ( ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) Fn ω ∧ ∅ ∈ ω ) → ( ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ∅ ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
5	2 3 4	mp2an	⊢ ( ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ∅ ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) Pred ( 𝑅 , 𝐴 , 𝑋 ) )
6	1 5	sylib	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → ∅ ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) Pred ( 𝑅 , 𝐴 , 𝑋 ) )
7		0ex	⊢ ∅ ∈ V
8		breq1	⊢ ( 𝑧 = ∅ → ( 𝑧 ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ∅ ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
9	7 8	spcev	⊢ ( ∅ ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) Pred ( 𝑅 , 𝐴 , 𝑋 ) → ∃ 𝑧 𝑧 ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) Pred ( 𝑅 , 𝐴 , 𝑋 ) )
10	6 9	syl	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → ∃ 𝑧 𝑧 ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) Pred ( 𝑅 , 𝐴 , 𝑋 ) )
11		elrng	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ↔ ∃ 𝑧 𝑧 ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
12	10 11	mpbird	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) )
13		elssuni	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) )
14	12 13	syl	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) )
15		df-trpred	⊢ TrPred ( 𝑅 , 𝐴 , 𝑋 ) = ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω )
16	14 15	sseqtrrdi	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) )