Theorem bnj18eq1

Description: Equality theorem for transitive closure. (Contributed by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

	Ref	Expression
Assertion	bnj18eq1	|- ( X = Y -> _trCl ( X , A , R ) = _trCl ( Y , A , R ) )

Proof

Step	Hyp	Ref	Expression
1		bnj602	|- ( X = Y -> _pred ( X , A , R ) = _pred ( Y , A , R ) )
2	1	eqeq2d	|- ( X = Y -> ( ( f ` (/) ) = _pred ( X , A , R ) <-> ( f ` (/) ) = _pred ( Y , A , R ) ) )
3	2	3anbi2d	|- ( X = Y -> ( ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> ( f Fn n /\ ( f ` (/) ) = _pred ( Y , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) )
4	3	rexbidv	|- ( X = Y -> ( E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( Y , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) )
5	4	abbidv	|- ( X = Y -> { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } = { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( Y , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } )
6	5	eleq2d	|- ( X = Y -> ( f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } <-> f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( Y , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } ) )
7	6	anbi1d	|- ( X = Y -> ( ( f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } /\ x e. U_ i e. dom f ( f ` i ) ) <-> ( f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( Y , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } /\ x e. U_ i e. dom f ( f ` i ) ) ) )
8	7	rexbidv2	|- ( X = Y -> ( E. f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } x e. U_ i e. dom f ( f ` i ) <-> E. f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( Y , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } x e. U_ i e. dom f ( f ` i ) ) )
9	8	abbidv	|- ( X = Y -> { x | E. f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } x e. U_ i e. dom f ( f ` i ) } = { x | E. f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( Y , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } x e. U_ i e. dom f ( f ` i ) } )
10		df-iun	|- U_ f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i ) = { x | E. f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } x e. U_ i e. dom f ( f ` i ) }
11		df-iun	|- U_ f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( Y , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i ) = { x | E. f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( Y , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } x e. U_ i e. dom f ( f ` i ) }
12	9 10 11	3eqtr4g	|- ( X = Y -> U_ f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i ) = U_ f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( Y , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i ) )
13		df-bnj18	|- _trCl ( X , A , R ) = U_ f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i )
14		df-bnj18	|- _trCl ( Y , A , R ) = U_ f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( Y , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i )
15	12 13 14	3eqtr4g	|- ( X = Y -> _trCl ( X , A , R ) = _trCl ( Y , A , R ) )