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 )

Metamath Proof Explorer

Theorem bnj893

Proof