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 = ω ∖ \{\emptyset\}$
	bnj938.2	No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
	bnj938.3	$⊢ σ \leftrightarrow (m \in D \land n = suc m \land p \in m)$
	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	$⊢ (R FrSe A \land X \in A \land τ \land σ) \to ⋃_{y \in f (p)} pred (y, A, R) \in V$

Proof

Step	Hyp	Ref	Expression
1		bnj938.1	$⊢ D = ω ∖ \{\emptyset\}$
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	$⊢ σ \leftrightarrow (m \in D \land n = suc m \land p \in m)$
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 x x = X$
7	6	bnj706	$⊢ (R FrSe A \land X \in A \land τ \land σ) \to \exists x x = X$
8		bnj291	$⊢ (R FrSe A \land X \in A \land τ \land σ) \leftrightarrow ((R FrSe A \land τ \land σ) \land X \in A)$
9	8	simplbi	$⊢ (R FrSe A \land X \in A \land τ \land σ) \to (R FrSe A \land τ \land σ)$
10		bnj602	$⊢ x = X \to pred (x, A, R) = pred (X, A, R)$
11	10	eqeq2d	$⊢ x = X \to (f (\emptyset) = pred (x, A, R) \leftrightarrow f (\emptyset) = pred (X, A, R))$
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	imbitrrid	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 (\emptyset) = pred (x, A, R) \leftrightarrow f (\emptyset) = pred (x, A, R)$
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 ((R FrSe A \land X \in A \land τ \land σ) \to ⋃_{y \in f (p)} pred (y, A, R) \in V)$
21	20	exlimiv	$⊢ \exists x x = X \to ((R FrSe A \land X \in A \land τ \land σ) \to ⋃_{y \in f (p)} pred (y, A, R) \in V)$
22	7 21	mpcom	$⊢ (R FrSe A \land X \in A \land τ \land σ) \to ⋃_{y \in f (p)} pred (y, A, R) \in V$

Metamath Proof Explorer

Theorem bnj938

Proof