Theorem trpred0

Description: The class of transitive predecessors is empty when A is empty. (Contributed by Scott Fenton, 30-Apr-2012)

	Ref	Expression
Assertion	trpred0	⊢ TrPred ( 𝑅 , ∅ , 𝑋 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		dftrpred2	⊢ TrPred ( 𝑅 , ∅ , 𝑋 ) = ∪ 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , ∅ , 𝑦 ) ) , Pred ( 𝑅 , ∅ , 𝑋 ) ) ↾ ω ) ‘ 𝑖 )
2		pred0	⊢ Pred ( 𝑅 , ∅ , 𝑦 ) = ∅
3	2	a1i	⊢ ( 𝑦 ∈ 𝑎 → Pred ( 𝑅 , ∅ , 𝑦 ) = ∅ )
4	3	iuneq2i	⊢ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , ∅ , 𝑦 ) = ∪ 𝑦 ∈ 𝑎 ∅
5		iun0	⊢ ∪ 𝑦 ∈ 𝑎 ∅ = ∅
6	4 5	eqtri	⊢ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , ∅ , 𝑦 ) = ∅
7	6	mpteq2i	⊢ ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , ∅ , 𝑦 ) ) = ( 𝑎 ∈ V ↦ ∅ )
8		pred0	⊢ Pred ( 𝑅 , ∅ , 𝑋 ) = ∅
9		rdgeq12	⊢ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , ∅ , 𝑦 ) ) = ( 𝑎 ∈ V ↦ ∅ ) ∧ Pred ( 𝑅 , ∅ , 𝑋 ) = ∅ ) → rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , ∅ , 𝑦 ) ) , Pred ( 𝑅 , ∅ , 𝑋 ) ) = rec ( ( 𝑎 ∈ V ↦ ∅ ) , ∅ ) )
10	7 8 9	mp2an	⊢ rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , ∅ , 𝑦 ) ) , Pred ( 𝑅 , ∅ , 𝑋 ) ) = rec ( ( 𝑎 ∈ V ↦ ∅ ) , ∅ )
11	10	reseq1i	⊢ ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , ∅ , 𝑦 ) ) , Pred ( 𝑅 , ∅ , 𝑋 ) ) ↾ ω ) = ( rec ( ( 𝑎 ∈ V ↦ ∅ ) , ∅ ) ↾ ω )
12	11	fveq1i	⊢ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , ∅ , 𝑦 ) ) , Pred ( 𝑅 , ∅ , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) = ( ( rec ( ( 𝑎 ∈ V ↦ ∅ ) , ∅ ) ↾ ω ) ‘ 𝑖 )
13		nn0suc	⊢ ( 𝑖 ∈ ω → ( 𝑖 = ∅ ∨ ∃ 𝑗 ∈ ω 𝑖 = suc 𝑗 ) )
14		fveq2	⊢ ( 𝑖 = ∅ → ( ( rec ( ( 𝑎 ∈ V ↦ ∅ ) , ∅ ) ↾ ω ) ‘ 𝑖 ) = ( ( rec ( ( 𝑎 ∈ V ↦ ∅ ) , ∅ ) ↾ ω ) ‘ ∅ ) )
15		0ex	⊢ ∅ ∈ V
16		fr0g	⊢ ( ∅ ∈ V → ( ( rec ( ( 𝑎 ∈ V ↦ ∅ ) , ∅ ) ↾ ω ) ‘ ∅ ) = ∅ )
17	15 16	ax-mp	⊢ ( ( rec ( ( 𝑎 ∈ V ↦ ∅ ) , ∅ ) ↾ ω ) ‘ ∅ ) = ∅
18	14 17	eqtrdi	⊢ ( 𝑖 = ∅ → ( ( rec ( ( 𝑎 ∈ V ↦ ∅ ) , ∅ ) ↾ ω ) ‘ 𝑖 ) = ∅ )
19		nfcv	⊢ Ⅎ 𝑎 ∅
20		nfcv	⊢ Ⅎ 𝑎 𝑗
21		eqid	⊢ ( rec ( ( 𝑎 ∈ V ↦ ∅ ) , ∅ ) ↾ ω ) = ( rec ( ( 𝑎 ∈ V ↦ ∅ ) , ∅ ) ↾ ω )
22		eqidd	⊢ ( 𝑎 = ( ( rec ( ( 𝑎 ∈ V ↦ ∅ ) , ∅ ) ↾ ω ) ‘ 𝑗 ) → ∅ = ∅ )
23	19 20 19 21 22	frsucmpt	⊢ ( ( 𝑗 ∈ ω ∧ ∅ ∈ V ) → ( ( rec ( ( 𝑎 ∈ V ↦ ∅ ) , ∅ ) ↾ ω ) ‘ suc 𝑗 ) = ∅ )
24	15 23	mpan2	⊢ ( 𝑗 ∈ ω → ( ( rec ( ( 𝑎 ∈ V ↦ ∅ ) , ∅ ) ↾ ω ) ‘ suc 𝑗 ) = ∅ )
25		fveqeq2	⊢ ( 𝑖 = suc 𝑗 → ( ( ( rec ( ( 𝑎 ∈ V ↦ ∅ ) , ∅ ) ↾ ω ) ‘ 𝑖 ) = ∅ ↔ ( ( rec ( ( 𝑎 ∈ V ↦ ∅ ) , ∅ ) ↾ ω ) ‘ suc 𝑗 ) = ∅ ) )
26	24 25	syl5ibrcom	⊢ ( 𝑗 ∈ ω → ( 𝑖 = suc 𝑗 → ( ( rec ( ( 𝑎 ∈ V ↦ ∅ ) , ∅ ) ↾ ω ) ‘ 𝑖 ) = ∅ ) )
27	26	rexlimiv	⊢ ( ∃ 𝑗 ∈ ω 𝑖 = suc 𝑗 → ( ( rec ( ( 𝑎 ∈ V ↦ ∅ ) , ∅ ) ↾ ω ) ‘ 𝑖 ) = ∅ )
28	18 27	jaoi	⊢ ( ( 𝑖 = ∅ ∨ ∃ 𝑗 ∈ ω 𝑖 = suc 𝑗 ) → ( ( rec ( ( 𝑎 ∈ V ↦ ∅ ) , ∅ ) ↾ ω ) ‘ 𝑖 ) = ∅ )
29	13 28	syl	⊢ ( 𝑖 ∈ ω → ( ( rec ( ( 𝑎 ∈ V ↦ ∅ ) , ∅ ) ↾ ω ) ‘ 𝑖 ) = ∅ )
30	12 29	syl5eq	⊢ ( 𝑖 ∈ ω → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , ∅ , 𝑦 ) ) , Pred ( 𝑅 , ∅ , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) = ∅ )
31	30	iuneq2i	⊢ ∪ 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , ∅ , 𝑦 ) ) , Pred ( 𝑅 , ∅ , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) = ∪ 𝑖 ∈ ω ∅
32		iun0	⊢ ∪ 𝑖 ∈ ω ∅ = ∅
33	1 31 32	3eqtri	⊢ TrPred ( 𝑅 , ∅ , 𝑋 ) = ∅