bnj518

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	bnj518.1	\|- ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
	bnj518.2	\|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
	bnj518.3	\|- ( ta <-> ( ph /\ ps /\ n e. _om /\ p e. n ) )
Assertion	bnj518	\|- ( ( R _FrSe A /\ ta ) -> A. y e. ( f ` p ) _pred ( y , A , R ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		bnj518.1	\|- ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
2		bnj518.2	\|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3		bnj518.3	\|- ( ta <-> ( ph /\ ps /\ n e. _om /\ p e. n ) )
4		bnj334	\|- ( ( ph /\ ps /\ n e. _om /\ p e. n ) <-> ( n e. _om /\ ph /\ ps /\ p e. n ) )
5	3 4	bitri	\|- ( ta <-> ( n e. _om /\ ph /\ ps /\ p e. n ) )
6		df-bnj17	\|- ( ( n e. _om /\ ph /\ ps /\ p e. n ) <-> ( ( n e. _om /\ ph /\ ps ) /\ p e. n ) )
7	1 2	bnj517	\|- ( ( n e. _om /\ ph /\ ps ) -> A. p e. n ( f ` p ) C_ A )
8	7	r19.21bi	\|- ( ( ( n e. _om /\ ph /\ ps ) /\ p e. n ) -> ( f ` p ) C_ A )
9	6 8	sylbi	\|- ( ( n e. _om /\ ph /\ ps /\ p e. n ) -> ( f ` p ) C_ A )
10	5 9	sylbi	\|- ( ta -> ( f ` p ) C_ A )
11		ssel	\|- ( ( f ` p ) C_ A -> ( y e. ( f ` p ) -> y e. A ) )
12		bnj93	\|- ( ( R _FrSe A /\ y e. A ) -> _pred ( y , A , R ) e. _V )
13	12	ex	\|- ( R _FrSe A -> ( y e. A -> _pred ( y , A , R ) e. _V ) )
14	11 13	sylan9r	\|- ( ( R _FrSe A /\ ( f ` p ) C_ A ) -> ( y e. ( f ` p ) -> _pred ( y , A , R ) e. _V ) )
15	14	ralrimiv	\|- ( ( R _FrSe A /\ ( f ` p ) C_ A ) -> A. y e. ( f ` p ) _pred ( y , A , R ) e. _V )
16	10 15	sylan2	\|- ( ( R _FrSe A /\ ta ) -> A. y e. ( f ` p ) _pred ( y , A , R ) e. _V )

Metamath Proof Explorer

Theorem bnj518

Proof