Theorem bnj938

Description: Technical lemma for bnj69 . 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	bnj938.1	$$⊢D=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
	bnj938.2	No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
	bnj938.3	$$⊢\sigma \leftrightarrow \left(m\in D\wedge n=\mathrm{suc}m\wedge p\in m\right)$$
	bnj938.4	No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( X , A , R ) ) with typecode |-
	bnj938.5	No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |-
Assertion	bnj938	$$⊢\left(RFrSeA\wedge X\in A\wedge \tau \wedge \sigma \right)\to \bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		bnj938.1	$$⊢D=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
2		bnj938.2	Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
3		bnj938.3	$$⊢\sigma \leftrightarrow \left(m\in D\wedge n=\mathrm{suc}m\wedge p\in m\right)$$
4		bnj938.4	Could not format ( ph' <-> ( f ` (/) ) = _pred ( X , A , R ) ) : No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( X , A , R ) ) with typecode |-
5		bnj938.5	Could not format ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |-
6		elisset	$$⊢X\in A\to \exists xx=X$$
7	6	bnj706	$$⊢\left(RFrSeA\wedge X\in A\wedge \tau \wedge \sigma \right)\to \exists xx=X$$
8		bnj291	$$⊢\left(RFrSeA\wedge X\in A\wedge \tau \wedge \sigma \right)\leftrightarrow \left(\left(RFrSeA\wedge \tau \wedge \sigma \right)\wedge X\in A\right)$$
9	8	simplbi	$$⊢\left(RFrSeA\wedge X\in A\wedge \tau \wedge \sigma \right)\to \left(RFrSeA\wedge \tau \wedge \sigma \right)$$
10		bnj602	$$⊢x=X\to pred\left(x,A,R\right)=pred\left(X,A,R\right)$$
11	10	eqeq2d	$$⊢x=X\to \left(f\left(\varnothing \right)=pred\left(x,A,R\right)\leftrightarrow f\left(\varnothing \right)=pred\left(X,A,R\right)\right)$$
12	11 4	bitr4di	Could not format ( x = X -> ( ( f ` (/) ) = _pred ( x , A , R ) <-> ph' ) ) : No typesetting found for |- ( x = X -> ( ( f ` (/) ) = _pred ( x , A , R ) <-> ph' ) ) with typecode |-
13	12	3anbi2d	Could not format ( x = X -> ( ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) <-> ( f Fn m /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( x = X -> ( ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) <-> ( f Fn m /\ ph' /\ ps' ) ) ) with typecode |-
14	13 2	bitr4di	Could not format ( x = X -> ( ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) <-> ta ) ) : No typesetting found for |- ( x = X -> ( ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) <-> ta ) ) with typecode |-
15	14	3anbi2d	Could not format ( x = X -> ( ( R _FrSe A /\ ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) /\ si ) <-> ( R _FrSe A /\ ta /\ si ) ) ) : No typesetting found for |- ( x = X -> ( ( R _FrSe A /\ ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) /\ si ) <-> ( R _FrSe A /\ ta /\ si ) ) ) with typecode |-
16	9 15	syl5ibr	Could not format ( x = X -> ( ( R _FrSe A /\ X e. A /\ ta /\ si ) -> ( R _FrSe A /\ ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) /\ si ) ) ) : No typesetting found for |- ( x = X -> ( ( R _FrSe A /\ X e. A /\ ta /\ si ) -> ( R _FrSe A /\ ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) /\ si ) ) ) with typecode |-
17		biid	Could not format ( ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) <-> ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) ) : No typesetting found for |- ( ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) <-> ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) ) with typecode |-
18		biid	$$⊢f\left(\varnothing \right)=pred\left(x,A,R\right)\leftrightarrow f\left(\varnothing \right)=pred\left(x,A,R\right)$$
19	1 17 3 18 5	bnj546	Could not format ( ( R _FrSe A /\ ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) /\ si ) -> U_ y e. ( f ` p ) _pred ( y , A , R ) e. _V ) : No typesetting found for |- ( ( R _FrSe A /\ ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) /\ si ) -> U_ y e. ( f ` p ) _pred ( y , A , R ) e. _V ) with typecode |-
20	16 19	syl6	$$⊢x=X\to \left(\left(RFrSeA\wedge X\in A\wedge \tau \wedge \sigma \right)\to \bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)\in \mathrm{V}\right)$$
21	20	exlimiv	$$⊢\exists xx=X\to \left(\left(RFrSeA\wedge X\in A\wedge \tau \wedge \sigma \right)\to \bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)\in \mathrm{V}\right)$$
22	7 21	mpcom	$$⊢\left(RFrSeA\wedge X\in A\wedge \tau \wedge \sigma \right)\to \bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)\in \mathrm{V}$$