Theorem bnj882

Description: Definition (using hypotheses for readability) of the function giving the transitive closure of X in A by R . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj882.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
	bnj882.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj882.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
	bnj882.4	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
Assertion	bnj882	⊢ trCl ( 𝑋 , 𝐴 , 𝑅 ) = ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 )

Proof

Step	Hyp	Ref	Expression
1		bnj882.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2		bnj882.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3		bnj882.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
4		bnj882.4	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
5		df-bnj18	⊢ trCl ( 𝑋 , 𝐴 , 𝑅 ) = ∪ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 )
6		df-iun	⊢ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) = { 𝑤 ∣ ∃ 𝑓 ∈ 𝐵 𝑤 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) }
7		df-iun	⊢ ∪ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) = { 𝑤 ∣ ∃ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑤 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) }
8	1 2	anbi12i	⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ( ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
9	8	anbi2i	⊢ ( ( 𝑓 Fn 𝑛 ∧ ( 𝜑 ∧ 𝜓 ) ) ↔ ( 𝑓 Fn 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) )
10		3anass	⊢ ( ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ( 𝑓 Fn 𝑛 ∧ ( 𝜑 ∧ 𝜓 ) ) )
11		3anass	⊢ ( ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑓 Fn 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) )
12	9 10 11	3bitr4i	⊢ ( ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
13	3 12	rexeqbii	⊢ ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
14	13	abbii	⊢ { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) } = { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) }
15	4 14	eqtri	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) }
16	15	eleq2i	⊢ ( 𝑓 ∈ 𝐵 ↔ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } )
17	16	anbi1i	⊢ ( ( 𝑓 ∈ 𝐵 ∧ 𝑤 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ) ↔ ( 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ∧ 𝑤 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ) )
18	17	rexbii2	⊢ ( ∃ 𝑓 ∈ 𝐵 𝑤 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ↔ ∃ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑤 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) )
19	18	abbii	⊢ { 𝑤 ∣ ∃ 𝑓 ∈ 𝐵 𝑤 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) } = { 𝑤 ∣ ∃ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑤 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) }
20	7 19	eqtr4i	⊢ ∪ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) = { 𝑤 ∣ ∃ 𝑓 ∈ 𝐵 𝑤 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) }
21	6 20	eqtr4i	⊢ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) = ∪ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 )
22	5 21	eqtr4i	⊢ trCl ( 𝑋 , 𝐴 , 𝑅 ) = ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 )