This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ φ ↔ f ⁡ ∅ = pred X A R
bnj1097.3 ⊢ χ ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ
bnj1097.5 ⊢ τ ↔ B ∈ V ∧ TrFo B A R ∧ pred X A R ⊆ B
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 ⊢ φ ↔ f ⁡ ∅ = pred X A R
2 bnj1097.3 ⊢ χ ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ
3 bnj1097.5 ⊢ τ ↔ B ∈ V ∧ TrFo B A R ∧ pred X A R ⊆ B
4 1 biimpi ⊢ φ → f ⁡ ∅ = pred X A R
5 2 4 bnj771 ⊢ χ → f ⁡ ∅ = pred X A R
6 5 3ad2ant3 ⊢ θ ∧ τ ∧ χ → f ⁡ ∅ = pred X A R
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 ⊢ τ → pred X A R ⊆ B
9 8 3ad2ant2 ⊢ θ ∧ τ ∧ χ → pred X A R ⊆ 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 ⊢ i = ∅ ∧ f ⁡ ∅ = pred X A R ∧ pred X A R ⊆ B ↔ i = ∅ ∧ f ⁡ ∅ = pred X A R ∧ pred X A R ⊆ B
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 = ∅ → f ⁡ i = pred X A R ↔ f ⁡ ∅ = pred X A R
16 15 biimpar ⊢ i = ∅ ∧ f ⁡ ∅ = pred X A R → f ⁡ i = pred X A R
17 16 adantr ⊢ i = ∅ ∧ f ⁡ ∅ = pred X A R ∧ pred X A R ⊆ B → f ⁡ i = pred X A R
18 simpr ⊢ i = ∅ ∧ f ⁡ ∅ = pred X A R ∧ pred X A R ⊆ B → pred X A R ⊆ B
19 17 18 eqsstrd ⊢ i = ∅ ∧ f ⁡ ∅ = pred X A R ∧ pred X A R ⊆ B → f ⁡ i ⊆ B
20 19 3impa ⊢ i = ∅ ∧ f ⁡ ∅ = pred X A R ∧ pred X A R ⊆ B → f ⁡ i ⊆ 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 |-