# Metamath Proof Explorer

## Theorem bnj893

Description: Property of _trCl . Under certain conditions, the transitive closure of X in A by R is a set. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion bnj893 ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) ∈ V )

### Proof

Step Hyp Ref Expression
1 biid ( ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2 biid ( ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3 eqid ( ω ∖ { ∅ } ) = ( ω ∖ { ∅ } )
4 eqid { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } = { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) }
5 1 2 3 4 bnj882 trCl ( 𝑋 , 𝐴 , 𝑅 ) = 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑖 ∈ dom 𝑓 ( 𝑓𝑖 )
6 vex 𝑔 ∈ V
7 fveq1 ( 𝑓 = 𝑔 → ( 𝑓 ‘ ∅ ) = ( 𝑔 ‘ ∅ ) )
8 7 eqeq1d ( 𝑓 = 𝑔 → ( ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ↔ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ) )
9 6 8 sbcie ( [ 𝑔 / 𝑓 ] ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ↔ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
10 9 bicomi ( ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ↔ [ 𝑔 / 𝑓 ] ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
11 fveq1 ( 𝑓 = 𝑔 → ( 𝑓 ‘ suc 𝑖 ) = ( 𝑔 ‘ suc 𝑖 ) )
12 fveq1 ( 𝑓 = 𝑔 → ( 𝑓𝑖 ) = ( 𝑔𝑖 ) )
13 12 iuneq1d ( 𝑓 = 𝑔 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
14 11 13 eqeq12d ( 𝑓 = 𝑔 → ( ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
15 14 imbi2d ( 𝑓 = 𝑔 → ( ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
16 15 ralbidv ( 𝑓 = 𝑔 → ( ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
17 6 16 sbcie ( [ 𝑔 / 𝑓 ]𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
18 17 bicomi ( ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ [ 𝑔 / 𝑓 ]𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
19 4 10 18 bnj873 { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } = { 𝑔 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑔 Fn 𝑛 ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) }
20 19 eleq2i ( 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ↔ 𝑓 ∈ { 𝑔 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑔 Fn 𝑛 ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } )
21 20 anbi1i ( ( 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ∧ 𝑤 𝑖 ∈ dom 𝑓 ( 𝑓𝑖 ) ) ↔ ( 𝑓 ∈ { 𝑔 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑔 Fn 𝑛 ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ∧ 𝑤 𝑖 ∈ dom 𝑓 ( 𝑓𝑖 ) ) )
22 21 rexbii2 ( ∃ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑤 𝑖 ∈ dom 𝑓 ( 𝑓𝑖 ) ↔ ∃ 𝑓 ∈ { 𝑔 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑔 Fn 𝑛 ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑤 𝑖 ∈ dom 𝑓 ( 𝑓𝑖 ) )
23 22 abbii { 𝑤 ∣ ∃ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑤 𝑖 ∈ dom 𝑓 ( 𝑓𝑖 ) } = { 𝑤 ∣ ∃ 𝑓 ∈ { 𝑔 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑔 Fn 𝑛 ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑤 𝑖 ∈ dom 𝑓 ( 𝑓𝑖 ) }
24 df-iun 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑖 ∈ dom 𝑓 ( 𝑓𝑖 ) = { 𝑤 ∣ ∃ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑤 𝑖 ∈ dom 𝑓 ( 𝑓𝑖 ) }
25 df-iun 𝑓 ∈ { 𝑔 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑔 Fn 𝑛 ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑖 ∈ dom 𝑓 ( 𝑓𝑖 ) = { 𝑤 ∣ ∃ 𝑓 ∈ { 𝑔 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑔 Fn 𝑛 ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑤 𝑖 ∈ dom 𝑓 ( 𝑓𝑖 ) }
26 23 24 25 3eqtr4i 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑖 ∈ dom 𝑓 ( 𝑓𝑖 ) = 𝑓 ∈ { 𝑔 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑔 Fn 𝑛 ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑖 ∈ dom 𝑓 ( 𝑓𝑖 )
27 biid ( ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ↔ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
28 biid ( ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
29 eqid { 𝑔 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑔 Fn 𝑛 ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } = { 𝑔 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑔 Fn 𝑛 ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) }
30 biid ( ( 𝑅 FrSe 𝐴𝑋𝐴𝑛 ∈ ( ω ∖ { ∅ } ) ) ↔ ( 𝑅 FrSe 𝐴𝑋𝐴𝑛 ∈ ( ω ∖ { ∅ } ) ) )
31 biid ( ( 𝑔 Fn 𝑛 ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑔 Fn 𝑛 ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
32 biid ( [ 𝑧 / 𝑔 ] ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ↔ [ 𝑧 / 𝑔 ] ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
33 biid ( [ 𝑧 / 𝑔 ]𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ [ 𝑧 / 𝑔 ]𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
34 biid ( [ 𝑧 / 𝑔 ] ( 𝑔 Fn 𝑛 ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ [ 𝑧 / 𝑔 ] ( 𝑔 Fn 𝑛 ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
35 biid ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ↔ ( 𝑅 FrSe 𝐴𝑋𝐴 ) )
36 27 28 3 29 30 31 32 33 34 35 bnj849 ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) → { 𝑔 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑔 Fn 𝑛 ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ∈ V )
37 vex 𝑓 ∈ V
38 37 dmex dom 𝑓 ∈ V
39 fvex ( 𝑓𝑖 ) ∈ V
40 38 39 iunex 𝑖 ∈ dom 𝑓 ( 𝑓𝑖 ) ∈ V
41 40 rgenw 𝑓 ∈ { 𝑔 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑔 Fn 𝑛 ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑖 ∈ dom 𝑓 ( 𝑓𝑖 ) ∈ V
42 iunexg ( ( { 𝑔 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑔 Fn 𝑛 ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ∈ V ∧ ∀ 𝑓 ∈ { 𝑔 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑔 Fn 𝑛 ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑖 ∈ dom 𝑓 ( 𝑓𝑖 ) ∈ V ) → 𝑓 ∈ { 𝑔 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑔 Fn 𝑛 ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑖 ∈ dom 𝑓 ( 𝑓𝑖 ) ∈ V )
43 36 41 42 sylancl ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) → 𝑓 ∈ { 𝑔 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑔 Fn 𝑛 ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑔𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑖 ∈ dom 𝑓 ( 𝑓𝑖 ) ∈ V )
44 26 43 eqeltrid ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) → 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑖 ∈ dom 𝑓 ( 𝑓𝑖 ) ∈ V )
45 5 44 eqeltrid ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) ∈ V )