bnj1253

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

Proof

Step	Hyp	Ref	Expression
1		bnj1253.1	\|- B = { d \| ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2		bnj1253.2	\|- Y = <. x , ( f \|` _pred ( x , A , R ) ) >.
3		bnj1253.3	\|- C = { f \| E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4		bnj1253.4	\|- D = ( dom g i^i dom h )
5		bnj1253.5	\|- E = { x e. D \| ( g ` x ) =/= ( h ` x ) }
6		bnj1253.6	\|- ( ph <-> ( R _FrSe A /\ g e. C /\ h e. C /\ ( g \|` D ) =/= ( h \|` D ) ) )
7		bnj1253.7	\|- ( ps <-> ( ph /\ x e. E /\ A. y e. E -. y R x ) )
8	6	bnj1254	\|- ( ph -> ( g \|` D ) =/= ( h \|` D ) )
9	1 2 3 4 5 6 7	bnj1256	\|- ( ph -> E. d e. B g Fn d )
10	4	bnj1292	\|- D C_ dom g
11		fndm	\|- ( g Fn d -> dom g = d )
12	10 11	sseqtrid	\|- ( g Fn d -> D C_ d )
13		fnssres	\|- ( ( g Fn d /\ D C_ d ) -> ( g \|` D ) Fn D )
14	12 13	mpdan	\|- ( g Fn d -> ( g \|` D ) Fn D )
15	9 14	bnj31	\|- ( ph -> E. d e. B ( g \|` D ) Fn D )
16	15	bnj1265	\|- ( ph -> ( g \|` D ) Fn D )
17	1 2 3 4 5 6 7	bnj1259	\|- ( ph -> E. d e. B h Fn d )
18	4	bnj1293	\|- D C_ dom h
19		fndm	\|- ( h Fn d -> dom h = d )
20	18 19	sseqtrid	\|- ( h Fn d -> D C_ d )
21		fnssres	\|- ( ( h Fn d /\ D C_ d ) -> ( h \|` D ) Fn D )
22	20 21	mpdan	\|- ( h Fn d -> ( h \|` D ) Fn D )
23	17 22	bnj31	\|- ( ph -> E. d e. B ( h \|` D ) Fn D )
24	23	bnj1265	\|- ( ph -> ( h \|` D ) Fn D )
25		ssid	\|- D C_ D
26		fvreseq	\|- ( ( ( ( g \|` D ) Fn D /\ ( h \|` D ) Fn D ) /\ D C_ D ) -> ( ( ( g \|` D ) \|` D ) = ( ( h \|` D ) \|` D ) <-> A. x e. D ( ( g \|` D ) ` x ) = ( ( h \|` D ) ` x ) ) )
27	25 26	mpan2	\|- ( ( ( g \|` D ) Fn D /\ ( h \|` D ) Fn D ) -> ( ( ( g \|` D ) \|` D ) = ( ( h \|` D ) \|` D ) <-> A. x e. D ( ( g \|` D ) ` x ) = ( ( h \|` D ) ` x ) ) )
28	16 24 27	syl2anc	\|- ( ph -> ( ( ( g \|` D ) \|` D ) = ( ( h \|` D ) \|` D ) <-> A. x e. D ( ( g \|` D ) ` x ) = ( ( h \|` D ) ` x ) ) )
29		residm	\|- ( ( g \|` D ) \|` D ) = ( g \|` D )
30		residm	\|- ( ( h \|` D ) \|` D ) = ( h \|` D )
31	29 30	eqeq12i	\|- ( ( ( g \|` D ) \|` D ) = ( ( h \|` D ) \|` D ) <-> ( g \|` D ) = ( h \|` D ) )
32		df-ral	\|- ( A. x e. D ( ( g \|` D ) ` x ) = ( ( h \|` D ) ` x ) <-> A. x ( x e. D -> ( ( g \|` D ) ` x ) = ( ( h \|` D ) ` x ) ) )
33	28 31 32	3bitr3g	\|- ( ph -> ( ( g \|` D ) = ( h \|` D ) <-> A. x ( x e. D -> ( ( g \|` D ) ` x ) = ( ( h \|` D ) ` x ) ) ) )
34		fvres	\|- ( x e. D -> ( ( g \|` D ) ` x ) = ( g ` x ) )
35		fvres	\|- ( x e. D -> ( ( h \|` D ) ` x ) = ( h ` x ) )
36	34 35	eqeq12d	\|- ( x e. D -> ( ( ( g \|` D ) ` x ) = ( ( h \|` D ) ` x ) <-> ( g ` x ) = ( h ` x ) ) )
37	36	pm5.74i	\|- ( ( x e. D -> ( ( g \|` D ) ` x ) = ( ( h \|` D ) ` x ) ) <-> ( x e. D -> ( g ` x ) = ( h ` x ) ) )
38	37	albii	\|- ( A. x ( x e. D -> ( ( g \|` D ) ` x ) = ( ( h \|` D ) ` x ) ) <-> A. x ( x e. D -> ( g ` x ) = ( h ` x ) ) )
39	33 38	bitrdi	\|- ( ph -> ( ( g \|` D ) = ( h \|` D ) <-> A. x ( x e. D -> ( g ` x ) = ( h ` x ) ) ) )
40	39	necon3abid	\|- ( ph -> ( ( g \|` D ) =/= ( h \|` D ) <-> -. A. x ( x e. D -> ( g ` x ) = ( h ` x ) ) ) )
41		df-rex	\|- ( E. x e. D ( g ` x ) =/= ( h ` x ) <-> E. x ( x e. D /\ ( g ` x ) =/= ( h ` x ) ) )
42		pm4.61	\|- ( -. ( x e. D -> ( g ` x ) = ( h ` x ) ) <-> ( x e. D /\ -. ( g ` x ) = ( h ` x ) ) )
43		df-ne	\|- ( ( g ` x ) =/= ( h ` x ) <-> -. ( g ` x ) = ( h ` x ) )
44	43	anbi2i	\|- ( ( x e. D /\ ( g ` x ) =/= ( h ` x ) ) <-> ( x e. D /\ -. ( g ` x ) = ( h ` x ) ) )
45	42 44	bitr4i	\|- ( -. ( x e. D -> ( g ` x ) = ( h ` x ) ) <-> ( x e. D /\ ( g ` x ) =/= ( h ` x ) ) )
46	45	exbii	\|- ( E. x -. ( x e. D -> ( g ` x ) = ( h ` x ) ) <-> E. x ( x e. D /\ ( g ` x ) =/= ( h ` x ) ) )
47		exnal	\|- ( E. x -. ( x e. D -> ( g ` x ) = ( h ` x ) ) <-> -. A. x ( x e. D -> ( g ` x ) = ( h ` x ) ) )
48	41 46 47	3bitr2ri	\|- ( -. A. x ( x e. D -> ( g ` x ) = ( h ` x ) ) <-> E. x e. D ( g ` x ) =/= ( h ` x ) )
49	40 48	bitrdi	\|- ( ph -> ( ( g \|` D ) =/= ( h \|` D ) <-> E. x e. D ( g ` x ) =/= ( h ` x ) ) )
50	8 49	mpbid	\|- ( ph -> E. x e. D ( g ` x ) =/= ( h ` x ) )
51	5	neeq1i	\|- ( E =/= (/) <-> { x e. D \| ( g ` x ) =/= ( h ` x ) } =/= (/) )
52		rabn0	\|- ( { x e. D \| ( g ` x ) =/= ( h ` x ) } =/= (/) <-> E. x e. D ( g ` x ) =/= ( h ` x ) )
53	51 52	bitri	\|- ( E =/= (/) <-> E. x e. D ( g ` x ) =/= ( h ` x ) )
54	50 53	sylibr	\|- ( ph -> E =/= (/) )

Metamath Proof Explorer

Theorem bnj1253

Proof