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

Metamath Proof Explorer

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 ) )