Definition df-bnj18

Description: Define the function giving: the transitive closure of X in A by R . This definition has been designed for facilitating verification that it is eliminable and that the $d restrictions are sound and complete. For a more readable definition see bnj882 . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Assertion	df-bnj18	⊢ trCl ( 𝑋 , 𝐴 , 𝑅 ) = ∪ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cX	⊢ 𝑋
1		cA	⊢ 𝐴
2		cR	⊢ 𝑅
3	1 2 0	c-bnj18	⊢ trCl ( 𝑋 , 𝐴 , 𝑅 )
4		vf	⊢ 𝑓
5		vn	⊢ 𝑛
6		com	⊢ ω
7		c0	⊢ ∅
8	7	csn	⊢ { ∅ }
9	6 8	cdif	⊢ ( ω ∖ { ∅ } )
10	4	cv	⊢ 𝑓
11	5	cv	⊢ 𝑛
12	10 11	wfn	⊢ 𝑓 Fn 𝑛
13	7 10	cfv	⊢ ( 𝑓 ‘ ∅ )
14	1 2 0	c-bnj14	⊢ pred ( 𝑋 , 𝐴 , 𝑅 )
15	13 14	wceq	⊢ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 )
16		vi	⊢ 𝑖
17	16	cv	⊢ 𝑖
18	17	csuc	⊢ suc 𝑖
19	18 11	wcel	⊢ suc 𝑖 ∈ 𝑛
20	18 10	cfv	⊢ ( 𝑓 ‘ suc 𝑖 )
21		vy	⊢ 𝑦
22	17 10	cfv	⊢ ( 𝑓 ‘ 𝑖 )
23	21	cv	⊢ 𝑦
24	1 2 23	c-bnj14	⊢ pred ( 𝑦 , 𝐴 , 𝑅 )
25	21 22 24	ciun	⊢ ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
26	20 25	wceq	⊢ ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
27	19 26	wi	⊢ ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
28	27 16 6	wral	⊢ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
29	12 15 28	w3a	⊢ ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
30	29 5 9	wrex	⊢ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
31	30 4	cab	⊢ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) }
32	10	cdm	⊢ dom 𝑓
33	16 32 22	ciun	⊢ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 )
34	4 31 33	ciun	⊢ ∪ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 )
35	3 34	wceq	⊢ trCl ( 𝑋 , 𝐴 , 𝑅 ) = ∪ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 )