Theorem bnj1416

Description: Technical lemma for bnj60 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1416.1	|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
	bnj1416.2	|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
	bnj1416.3	|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
	bnj1416.4	|- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) )
	bnj1416.5	|- D = { x e. A | -. E. f ta }
	bnj1416.6	|- ( ps <-> ( R _FrSe A /\ D =/= (/) ) )
	bnj1416.7	|- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) )
	bnj1416.8	|- ( ta' <-> [. y / x ]. ta )
	bnj1416.9	|- H = { f | E. y e. _pred ( x , A , R ) ta' }
	bnj1416.10	|- P = U. H
	bnj1416.11	|- Z = <. x , ( P |` _pred ( x , A , R ) ) >.
	bnj1416.12	|- Q = ( P u. { <. x , ( G ` Z ) >. } )
	bnj1416.28	|- ( ch -> dom P = _trCl ( x , A , R ) )
Assertion	bnj1416	|- ( ch -> dom Q = ( { x } u. _trCl ( x , A , R ) ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1416.1	|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2		bnj1416.2	|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3		bnj1416.3	|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4		bnj1416.4	|- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) )
5		bnj1416.5	|- D = { x e. A | -. E. f ta }
6		bnj1416.6	|- ( ps <-> ( R _FrSe A /\ D =/= (/) ) )
7		bnj1416.7	|- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) )
8		bnj1416.8	|- ( ta' <-> [. y / x ]. ta )
9		bnj1416.9	|- H = { f | E. y e. _pred ( x , A , R ) ta' }
10		bnj1416.10	|- P = U. H
11		bnj1416.11	|- Z = <. x , ( P |` _pred ( x , A , R ) ) >.
12		bnj1416.12	|- Q = ( P u. { <. x , ( G ` Z ) >. } )
13		bnj1416.28	|- ( ch -> dom P = _trCl ( x , A , R ) )
14	12	dmeqi	|- dom Q = dom ( P u. { <. x , ( G ` Z ) >. } )
15		dmun	|- dom ( P u. { <. x , ( G ` Z ) >. } ) = ( dom P u. dom { <. x , ( G ` Z ) >. } )
16		fvex	|- ( G ` Z ) e. _V
17	16	dmsnop	|- dom { <. x , ( G ` Z ) >. } = { x }
18	17	uneq2i	|- ( dom P u. dom { <. x , ( G ` Z ) >. } ) = ( dom P u. { x } )
19	14 15 18	3eqtri	|- dom Q = ( dom P u. { x } )
20	13	uneq1d	|- ( ch -> ( dom P u. { x } ) = ( _trCl ( x , A , R ) u. { x } ) )
21		uncom	|- ( _trCl ( x , A , R ) u. { x } ) = ( { x } u. _trCl ( x , A , R ) )
22	20 21	eqtrdi	|- ( ch -> ( dom P u. { x } ) = ( { x } u. _trCl ( x , A , R ) ) )
23	19 22	syl5eq	|- ( ch -> dom Q = ( { x } u. _trCl ( x , A , R ) ) )