This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )