bnj1442

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	bnj1442.1	\|- B = { d \| ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
	bnj1442.2	\|- Y = <. x , ( f \|` _pred ( x , A , R ) ) >.
	bnj1442.3	\|- C = { f \| E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
	bnj1442.4	\|- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) )
	bnj1442.5	\|- D = { x e. A \| -. E. f ta }
	bnj1442.6	\|- ( ps <-> ( R _FrSe A /\ D =/= (/) ) )
	bnj1442.7	\|- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) )
	bnj1442.8	\|- ( ta' <-> [. y / x ]. ta )
	bnj1442.9	\|- H = { f \| E. y e. _pred ( x , A , R ) ta' }
	bnj1442.10	\|- P = U. H
	bnj1442.11	\|- Z = <. x , ( P \|` _pred ( x , A , R ) ) >.
	bnj1442.12	\|- Q = ( P u. { <. x , ( G ` Z ) >. } )
	bnj1442.13	\|- W = <. z , ( Q \|` _pred ( z , A , R ) ) >.
	bnj1442.14	\|- E = ( { x } u. _trCl ( x , A , R ) )
	bnj1442.15	\|- ( ch -> P Fn _trCl ( x , A , R ) )
	bnj1442.16	\|- ( ch -> Q Fn ( { x } u. _trCl ( x , A , R ) ) )
	bnj1442.17	\|- ( th <-> ( ch /\ z e. E ) )
	bnj1442.18	\|- ( et <-> ( th /\ z e. { x } ) )
Assertion	bnj1442	\|- ( et -> ( Q ` z ) = ( G ` W ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1442.1	\|- B = { d \| ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2		bnj1442.2	\|- Y = <. x , ( f \|` _pred ( x , A , R ) ) >.
3		bnj1442.3	\|- C = { f \| E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4		bnj1442.4	\|- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) )
5		bnj1442.5	\|- D = { x e. A \| -. E. f ta }
6		bnj1442.6	\|- ( ps <-> ( R _FrSe A /\ D =/= (/) ) )
7		bnj1442.7	\|- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) )
8		bnj1442.8	\|- ( ta' <-> [. y / x ]. ta )
9		bnj1442.9	\|- H = { f \| E. y e. _pred ( x , A , R ) ta' }
10		bnj1442.10	\|- P = U. H
11		bnj1442.11	\|- Z = <. x , ( P \|` _pred ( x , A , R ) ) >.
12		bnj1442.12	\|- Q = ( P u. { <. x , ( G ` Z ) >. } )
13		bnj1442.13	\|- W = <. z , ( Q \|` _pred ( z , A , R ) ) >.
14		bnj1442.14	\|- E = ( { x } u. _trCl ( x , A , R ) )
15		bnj1442.15	\|- ( ch -> P Fn _trCl ( x , A , R ) )
16		bnj1442.16	\|- ( ch -> Q Fn ( { x } u. _trCl ( x , A , R ) ) )
17		bnj1442.17	\|- ( th <-> ( ch /\ z e. E ) )
18		bnj1442.18	\|- ( et <-> ( th /\ z e. { x } ) )
19	16	fnfund	\|- ( ch -> Fun Q )
20		opex	\|- <. x , ( G ` Z ) >. e. _V
21	20	snid	\|- <. x , ( G ` Z ) >. e. { <. x , ( G ` Z ) >. }
22		elun2	\|- ( <. x , ( G ` Z ) >. e. { <. x , ( G ` Z ) >. } -> <. x , ( G ` Z ) >. e. ( P u. { <. x , ( G ` Z ) >. } ) )
23	21 22	ax-mp	\|- <. x , ( G ` Z ) >. e. ( P u. { <. x , ( G ` Z ) >. } )
24	23 12	eleqtrri	\|- <. x , ( G ` Z ) >. e. Q
25		funopfv	\|- ( Fun Q -> ( <. x , ( G ` Z ) >. e. Q -> ( Q ` x ) = ( G ` Z ) ) )
26	19 24 25	mpisyl	\|- ( ch -> ( Q ` x ) = ( G ` Z ) )
27	17 26	bnj832	\|- ( th -> ( Q ` x ) = ( G ` Z ) )
28	18 27	bnj832	\|- ( et -> ( Q ` x ) = ( G ` Z ) )
29		elsni	\|- ( z e. { x } -> z = x )
30	18 29	simplbiim	\|- ( et -> z = x )
31	30	fveq2d	\|- ( et -> ( Q ` z ) = ( Q ` x ) )
32		bnj602	\|- ( z = x -> _pred ( z , A , R ) = _pred ( x , A , R ) )
33	32	reseq2d	\|- ( z = x -> ( Q \|` _pred ( z , A , R ) ) = ( Q \|` _pred ( x , A , R ) ) )
34	30 33	syl	\|- ( et -> ( Q \|` _pred ( z , A , R ) ) = ( Q \|` _pred ( x , A , R ) ) )
35	12	bnj931	\|- P C_ Q
36	35	a1i	\|- ( ch -> P C_ Q )
37	6	simplbi	\|- ( ps -> R _FrSe A )
38	7 37	bnj835	\|- ( ch -> R _FrSe A )
39	5 7	bnj1212	\|- ( ch -> x e. A )
40		bnj906	\|- ( ( R _FrSe A /\ x e. A ) -> _pred ( x , A , R ) C_ _trCl ( x , A , R ) )
41	38 39 40	syl2anc	\|- ( ch -> _pred ( x , A , R ) C_ _trCl ( x , A , R ) )
42	15	fndmd	\|- ( ch -> dom P = _trCl ( x , A , R ) )
43	41 42	sseqtrrd	\|- ( ch -> _pred ( x , A , R ) C_ dom P )
44	19 36 43	bnj1503	\|- ( ch -> ( Q \|` _pred ( x , A , R ) ) = ( P \|` _pred ( x , A , R ) ) )
45	17 44	bnj832	\|- ( th -> ( Q \|` _pred ( x , A , R ) ) = ( P \|` _pred ( x , A , R ) ) )
46	18 45	bnj832	\|- ( et -> ( Q \|` _pred ( x , A , R ) ) = ( P \|` _pred ( x , A , R ) ) )
47	34 46	eqtrd	\|- ( et -> ( Q \|` _pred ( z , A , R ) ) = ( P \|` _pred ( x , A , R ) ) )
48	30 47	opeq12d	\|- ( et -> <. z , ( Q \|` _pred ( z , A , R ) ) >. = <. x , ( P \|` _pred ( x , A , R ) ) >. )
49	48 13 11	3eqtr4g	\|- ( et -> W = Z )
50	49	fveq2d	\|- ( et -> ( G ` W ) = ( G ` Z ) )
51	28 31 50	3eqtr4d	\|- ( et -> ( Q ` z ) = ( G ` W ) )

Metamath Proof Explorer

Theorem bnj1442

Proof