bnj554

Description: Technical lemma for bnj852 . 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	bnj554.19	\|- ( et <-> ( m e. D /\ n = suc m /\ p e. _om /\ m = suc p ) )
	bnj554.20	\|- ( ze <-> ( i e. _om /\ suc i e. n /\ m = suc i ) )
	bnj554.21	\|- K = U_ y e. ( G ` i ) _pred ( y , A , R )
	bnj554.22	\|- L = U_ y e. ( G ` p ) _pred ( y , A , R )
	bnj554.23	\|- K = U_ y e. ( G ` i ) _pred ( y , A , R )
	bnj554.24	\|- L = U_ y e. ( G ` p ) _pred ( y , A , R )
Assertion	bnj554	\|- ( ( et /\ ze ) -> ( ( G ` m ) = L <-> ( G ` suc i ) = K ) )

Proof

Step	Hyp	Ref	Expression
1		bnj554.19	\|- ( et <-> ( m e. D /\ n = suc m /\ p e. _om /\ m = suc p ) )
2		bnj554.20	\|- ( ze <-> ( i e. _om /\ suc i e. n /\ m = suc i ) )
3		bnj554.21	\|- K = U_ y e. ( G ` i ) _pred ( y , A , R )
4		bnj554.22	\|- L = U_ y e. ( G ` p ) _pred ( y , A , R )
5		bnj554.23	\|- K = U_ y e. ( G ` i ) _pred ( y , A , R )
6		bnj554.24	\|- L = U_ y e. ( G ` p ) _pred ( y , A , R )
7	1	bnj1254	\|- ( et -> m = suc p )
8	2	simp3bi	\|- ( ze -> m = suc i )
9		simpr	\|- ( ( m = suc p /\ m = suc i ) -> m = suc i )
10		bnj551	\|- ( ( m = suc p /\ m = suc i ) -> p = i )
11		fveq2	\|- ( m = suc i -> ( G ` m ) = ( G ` suc i ) )
12		fveq2	\|- ( p = i -> ( G ` p ) = ( G ` i ) )
13		iuneq1	\|- ( ( G ` p ) = ( G ` i ) -> U_ y e. ( G ` p ) _pred ( y , A , R ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )
14	13 6 5	3eqtr4g	\|- ( ( G ` p ) = ( G ` i ) -> L = K )
15	12 14	syl	\|- ( p = i -> L = K )
16	11 15	eqeqan12d	\|- ( ( m = suc i /\ p = i ) -> ( ( G ` m ) = L <-> ( G ` suc i ) = K ) )
17	9 10 16	syl2anc	\|- ( ( m = suc p /\ m = suc i ) -> ( ( G ` m ) = L <-> ( G ` suc i ) = K ) )
18	7 8 17	syl2an	\|- ( ( et /\ ze ) -> ( ( G ` m ) = L <-> ( G ` suc i ) = K ) )

Metamath Proof Explorer

Theorem bnj554

Proof