Theorem bnj1097

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	bnj1097.1	$$⊢\phi \leftrightarrow f\left(\varnothing \right)=pred\left(X,A,R\right)$$
	bnj1097.3	$$⊢\chi \leftrightarrow \left(n\in D\wedge fFnn\wedge \phi \wedge \psi \right)$$
	bnj1097.5	$$⊢\tau \leftrightarrow \left(B\in \mathrm{V}\wedge TrFo\left(B,A,R\right)\wedge pred\left(X,A,R\right)\subseteq B\right)$$
Assertion	bnj1097	Could not format assertion : No typesetting found for |- ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bnj1097.1	$$⊢\phi \leftrightarrow f\left(\varnothing \right)=pred\left(X,A,R\right)$$
2		bnj1097.3	$$⊢\chi \leftrightarrow \left(n\in D\wedge fFnn\wedge \phi \wedge \psi \right)$$
3		bnj1097.5	$$⊢\tau \leftrightarrow \left(B\in \mathrm{V}\wedge TrFo\left(B,A,R\right)\wedge pred\left(X,A,R\right)\subseteq B\right)$$
4	1	biimpi	$$⊢\phi \to f\left(\varnothing \right)=pred\left(X,A,R\right)$$
5	2 4	bnj771	$$⊢\chi \to f\left(\varnothing \right)=pred\left(X,A,R\right)$$
6	5	3ad2ant3	$$⊢\left(\theta \wedge \tau \wedge \chi \right)\to f\left(\varnothing \right)=pred\left(X,A,R\right)$$
7	6	adantr	Could not format ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` (/) ) = _pred ( X , A , R ) ) : No typesetting found for |- ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` (/) ) = _pred ( X , A , R ) ) with typecode |-
8	3	simp3bi	$$⊢\tau \to pred\left(X,A,R\right)\subseteq B$$
9	8	3ad2ant2	$$⊢\left(\theta \wedge \tau \wedge \chi \right)\to pred\left(X,A,R\right)\subseteq B$$
10	9	adantr	Could not format ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> _pred ( X , A , R ) C_ B ) : No typesetting found for |- ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> _pred ( X , A , R ) C_ B ) with typecode |-
11	7 10	jca	Could not format ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) ) : No typesetting found for |- ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) ) with typecode |-
12	11	anim2i	Could not format ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( i = (/) /\ ( ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) ) ) : No typesetting found for |- ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( i = (/) /\ ( ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) ) ) with typecode |-
13		3anass	$$⊢\left(i=\varnothing \wedge f\left(\varnothing \right)=pred\left(X,A,R\right)\wedge pred\left(X,A,R\right)\subseteq B\right)\leftrightarrow \left(i=\varnothing \wedge \left(f\left(\varnothing \right)=pred\left(X,A,R\right)\wedge pred\left(X,A,R\right)\subseteq B\right)\right)$$
14	12 13	sylibr	Could not format ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( i = (/) /\ ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) ) : No typesetting found for |- ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( i = (/) /\ ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) ) with typecode |-
15		fveqeq2	$$⊢i=\varnothing \to \left(f\left(i\right)=pred\left(X,A,R\right)\leftrightarrow f\left(\varnothing \right)=pred\left(X,A,R\right)\right)$$
16	15	biimpar	$$⊢\left(i=\varnothing \wedge f\left(\varnothing \right)=pred\left(X,A,R\right)\right)\to f\left(i\right)=pred\left(X,A,R\right)$$
17	16	adantr	$$⊢\left(\left(i=\varnothing \wedge f\left(\varnothing \right)=pred\left(X,A,R\right)\right)\wedge pred\left(X,A,R\right)\subseteq B\right)\to f\left(i\right)=pred\left(X,A,R\right)$$
18		simpr	$$⊢\left(\left(i=\varnothing \wedge f\left(\varnothing \right)=pred\left(X,A,R\right)\right)\wedge pred\left(X,A,R\right)\subseteq B\right)\to pred\left(X,A,R\right)\subseteq B$$
19	17 18	eqsstrd	$$⊢\left(\left(i=\varnothing \wedge f\left(\varnothing \right)=pred\left(X,A,R\right)\right)\wedge pred\left(X,A,R\right)\subseteq B\right)\to f\left(i\right)\subseteq B$$
20	19	3impa	$$⊢\left(i=\varnothing \wedge f\left(\varnothing \right)=pred\left(X,A,R\right)\wedge pred\left(X,A,R\right)\subseteq B\right)\to f\left(i\right)\subseteq B$$
21	14 20	syl	Could not format ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) : No typesetting found for |- ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) with typecode |-