bnj1286

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	bnj1286.1	\|- B = { d \| ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
	bnj1286.2	\|- Y = <. x , ( f \|` _pred ( x , A , R ) ) >.
	bnj1286.3	\|- C = { f \| E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
	bnj1286.4	\|- D = ( dom g i^i dom h )
	bnj1286.5	\|- E = { x e. D \| ( g ` x ) =/= ( h ` x ) }
	bnj1286.6	\|- ( ph <-> ( R _FrSe A /\ g e. C /\ h e. C /\ ( g \|` D ) =/= ( h \|` D ) ) )
	bnj1286.7	\|- ( ps <-> ( ph /\ x e. E /\ A. y e. E -. y R x ) )
Assertion	bnj1286	\|- ( ps -> _pred ( x , A , R ) C_ D )

Proof

Step	Hyp	Ref	Expression
1		bnj1286.1	\|- B = { d \| ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2		bnj1286.2	\|- Y = <. x , ( f \|` _pred ( x , A , R ) ) >.
3		bnj1286.3	\|- C = { f \| E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4		bnj1286.4	\|- D = ( dom g i^i dom h )
5		bnj1286.5	\|- E = { x e. D \| ( g ` x ) =/= ( h ` x ) }
6		bnj1286.6	\|- ( ph <-> ( R _FrSe A /\ g e. C /\ h e. C /\ ( g \|` D ) =/= ( h \|` D ) ) )
7		bnj1286.7	\|- ( ps <-> ( ph /\ x e. E /\ A. y e. E -. y R x ) )
8	1 2 3 4 5 6 7	bnj1256	\|- ( ph -> E. d e. B g Fn d )
9	8	bnj1196	\|- ( ph -> E. d ( d e. B /\ g Fn d ) )
10	1	bnj1517	\|- ( d e. B -> A. x e. d _pred ( x , A , R ) C_ d )
11	10	adantr	\|- ( ( d e. B /\ g Fn d ) -> A. x e. d _pred ( x , A , R ) C_ d )
12		fndm	\|- ( g Fn d -> dom g = d )
13		sseq2	\|- ( dom g = d -> ( _pred ( x , A , R ) C_ dom g <-> _pred ( x , A , R ) C_ d ) )
14	13	raleqbi1dv	\|- ( dom g = d -> ( A. x e. dom g _pred ( x , A , R ) C_ dom g <-> A. x e. d _pred ( x , A , R ) C_ d ) )
15	12 14	syl	\|- ( g Fn d -> ( A. x e. dom g _pred ( x , A , R ) C_ dom g <-> A. x e. d _pred ( x , A , R ) C_ d ) )
16	15	adantl	\|- ( ( d e. B /\ g Fn d ) -> ( A. x e. dom g _pred ( x , A , R ) C_ dom g <-> A. x e. d _pred ( x , A , R ) C_ d ) )
17	11 16	mpbird	\|- ( ( d e. B /\ g Fn d ) -> A. x e. dom g _pred ( x , A , R ) C_ dom g )
18	9 17	bnj593	\|- ( ph -> E. d A. x e. dom g _pred ( x , A , R ) C_ dom g )
19	18	bnj937	\|- ( ph -> A. x e. dom g _pred ( x , A , R ) C_ dom g )
20	7 19	bnj835	\|- ( ps -> A. x e. dom g _pred ( x , A , R ) C_ dom g )
21	5	ssrab3	\|- E C_ D
22	4	bnj1292	\|- D C_ dom g
23	21 22	sstri	\|- E C_ dom g
24	23	sseli	\|- ( x e. E -> x e. dom g )
25	7 24	bnj836	\|- ( ps -> x e. dom g )
26	20 25	bnj1294	\|- ( ps -> _pred ( x , A , R ) C_ dom g )
27	1 2 3 4 5 6 7	bnj1259	\|- ( ph -> E. d e. B h Fn d )
28	27	bnj1196	\|- ( ph -> E. d ( d e. B /\ h Fn d ) )
29	10	adantr	\|- ( ( d e. B /\ h Fn d ) -> A. x e. d _pred ( x , A , R ) C_ d )
30		fndm	\|- ( h Fn d -> dom h = d )
31		sseq2	\|- ( dom h = d -> ( _pred ( x , A , R ) C_ dom h <-> _pred ( x , A , R ) C_ d ) )
32	31	raleqbi1dv	\|- ( dom h = d -> ( A. x e. dom h _pred ( x , A , R ) C_ dom h <-> A. x e. d _pred ( x , A , R ) C_ d ) )
33	30 32	syl	\|- ( h Fn d -> ( A. x e. dom h _pred ( x , A , R ) C_ dom h <-> A. x e. d _pred ( x , A , R ) C_ d ) )
34	33	adantl	\|- ( ( d e. B /\ h Fn d ) -> ( A. x e. dom h _pred ( x , A , R ) C_ dom h <-> A. x e. d _pred ( x , A , R ) C_ d ) )
35	29 34	mpbird	\|- ( ( d e. B /\ h Fn d ) -> A. x e. dom h _pred ( x , A , R ) C_ dom h )
36	28 35	bnj593	\|- ( ph -> E. d A. x e. dom h _pred ( x , A , R ) C_ dom h )
37	36	bnj937	\|- ( ph -> A. x e. dom h _pred ( x , A , R ) C_ dom h )
38	7 37	bnj835	\|- ( ps -> A. x e. dom h _pred ( x , A , R ) C_ dom h )
39	4	bnj1293	\|- D C_ dom h
40	21 39	sstri	\|- E C_ dom h
41	40	sseli	\|- ( x e. E -> x e. dom h )
42	7 41	bnj836	\|- ( ps -> x e. dom h )
43	38 42	bnj1294	\|- ( ps -> _pred ( x , A , R ) C_ dom h )
44	26 43	ssind	\|- ( ps -> _pred ( x , A , R ) C_ ( dom g i^i dom h ) )
45	44 4	sseqtrrdi	\|- ( ps -> _pred ( x , A , R ) C_ D )

Metamath Proof Explorer

Theorem bnj1286

Proof