bnj1467

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

Proof

Step	Hyp	Ref	Expression
1		bnj1467.1	\|- B = { d \| ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2		bnj1467.2	\|- Y = <. x , ( f \|` _pred ( x , A , R ) ) >.
3		bnj1467.3	\|- C = { f \| E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4		bnj1467.4	\|- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) )
5		bnj1467.5	\|- D = { x e. A \| -. E. f ta }
6		bnj1467.6	\|- ( ps <-> ( R _FrSe A /\ D =/= (/) ) )
7		bnj1467.7	\|- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) )
8		bnj1467.8	\|- ( ta' <-> [. y / x ]. ta )
9		bnj1467.9	\|- H = { f \| E. y e. _pred ( x , A , R ) ta' }
10		bnj1467.10	\|- P = U. H
11		bnj1467.11	\|- Z = <. x , ( P \|` _pred ( x , A , R ) ) >.
12		bnj1467.12	\|- Q = ( P u. { <. x , ( G ` Z ) >. } )
13		nfcv	\|- F/_ d _pred ( x , A , R )
14		nfcv	\|- F/_ d y
15		nfre1	\|- F/ d E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) )
16	15	nfab	\|- F/_ d { f \| E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
17	3 16	nfcxfr	\|- F/_ d C
18	17	nfcri	\|- F/ d f e. C
19		nfv	\|- F/ d dom f = ( { x } u. _trCl ( x , A , R ) )
20	18 19	nfan	\|- F/ d ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) )
21	4 20	nfxfr	\|- F/ d ta
22	14 21	nfsbcw	\|- F/ d [. y / x ]. ta
23	8 22	nfxfr	\|- F/ d ta'
24	13 23	nfrex	\|- F/ d E. y e. _pred ( x , A , R ) ta'
25	24	nfab	\|- F/_ d { f \| E. y e. _pred ( x , A , R ) ta' }
26	9 25	nfcxfr	\|- F/_ d H
27	26	nfuni	\|- F/_ d U. H
28	10 27	nfcxfr	\|- F/_ d P
29		nfcv	\|- F/_ d x
30		nfcv	\|- F/_ d G
31	28 13	nfres	\|- F/_ d ( P \|` _pred ( x , A , R ) )
32	29 31	nfop	\|- F/_ d <. x , ( P \|` _pred ( x , A , R ) ) >.
33	11 32	nfcxfr	\|- F/_ d Z
34	30 33	nffv	\|- F/_ d ( G ` Z )
35	29 34	nfop	\|- F/_ d <. x , ( G ` Z ) >.
36	35	nfsn	\|- F/_ d { <. x , ( G ` Z ) >. }
37	28 36	nfun	\|- F/_ d ( P u. { <. x , ( G ` Z ) >. } )
38	12 37	nfcxfr	\|- F/_ d Q
39	38	nfcrii	\|- ( w e. Q -> A. d w e. Q )

Metamath Proof Explorer

Theorem bnj1467

Proof