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

Metamath Proof Explorer

Theorem bnj545

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 bnj545.1 No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-
bnj545.2 ⊢ D = ω ∖ ∅
bnj545.3 ⊢ G = f ∪ m ⋃ y ∈ f ⁡ p pred y A R
bnj545.4 No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
bnj545.5 ⊢ σ ↔ m ∈ D ∧ n = suc ⁡ m ∧ p ∈ m
bnj545.6 ⊢ R FrSe A ∧ τ ∧ σ → G Fn n
bnj545.7 No typesetting found for |- ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) ) with typecode |-
Assertion bnj545 Could not format assertion : No typesetting found for |- ( ( R _FrSe A /\ ta /\ si ) -> ph" ) with typecode |-

Proof

Step Hyp Ref Expression
1 bnj545.1 Could not format ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-
2 bnj545.2 ⊢ D = ω ∖ ∅
3 bnj545.3 ⊢ G = f ∪ m ⋃ y ∈ f ⁡ p pred y A R
4 bnj545.4 Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
5 bnj545.5 ⊢ σ ↔ m ∈ D ∧ n = suc ⁡ m ∧ p ∈ m
6 bnj545.6 ⊢ R FrSe A ∧ τ ∧ σ → G Fn n
7 bnj545.7 Could not format ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) ) with typecode |-
8 4 simp1bi ⊢ τ → f Fn m
9 5 simp1bi ⊢ σ → m ∈ D
10 8 9 anim12i ⊢ τ ∧ σ → f Fn m ∧ m ∈ D
11 10 3adant1 ⊢ R FrSe A ∧ τ ∧ σ → f Fn m ∧ m ∈ D
12 2 bnj529 ⊢ m ∈ D → ∅ ∈ m
13 fndm ⊢ f Fn m → dom ⁡ f = m
14 eleq2 ⊢ dom ⁡ f = m → ∅ ∈ dom ⁡ f ↔ ∅ ∈ m
15 14 biimparc ⊢ ∅ ∈ m ∧ dom ⁡ f = m → ∅ ∈ dom ⁡ f
16 12 13 15 syl2anr ⊢ f Fn m ∧ m ∈ D → ∅ ∈ dom ⁡ f
17 11 16 syl ⊢ R FrSe A ∧ τ ∧ σ → ∅ ∈ dom ⁡ f
18 6 fnfund ⊢ R FrSe A ∧ τ ∧ σ → Fun ⁡ G
19 17 18 jca ⊢ R FrSe A ∧ τ ∧ σ → ∅ ∈ dom ⁡ f ∧ Fun ⁡ G
20 3 bnj931 ⊢ f ⊆ G
21 19 20 jctil ⊢ R FrSe A ∧ τ ∧ σ → f ⊆ G ∧ ∅ ∈ dom ⁡ f ∧ Fun ⁡ G
22 df-3an ⊢ ∅ ∈ dom ⁡ f ∧ Fun ⁡ G ∧ f ⊆ G ↔ ∅ ∈ dom ⁡ f ∧ Fun ⁡ G ∧ f ⊆ G
23 3anrot ⊢ ∅ ∈ dom ⁡ f ∧ Fun ⁡ G ∧ f ⊆ G ↔ Fun ⁡ G ∧ f ⊆ G ∧ ∅ ∈ dom ⁡ f
24 ancom ⊢ ∅ ∈ dom ⁡ f ∧ Fun ⁡ G ∧ f ⊆ G ↔ f ⊆ G ∧ ∅ ∈ dom ⁡ f ∧ Fun ⁡ G
25 22 23 24 3bitr3i ⊢ Fun ⁡ G ∧ f ⊆ G ∧ ∅ ∈ dom ⁡ f ↔ f ⊆ G ∧ ∅ ∈ dom ⁡ f ∧ Fun ⁡ G
26 21 25 sylibr ⊢ R FrSe A ∧ τ ∧ σ → Fun ⁡ G ∧ f ⊆ G ∧ ∅ ∈ dom ⁡ f
27 funssfv ⊢ Fun ⁡ G ∧ f ⊆ G ∧ ∅ ∈ dom ⁡ f → G ⁡ ∅ = f ⁡ ∅
28 26 27 syl ⊢ R FrSe A ∧ τ ∧ σ → G ⁡ ∅ = f ⁡ ∅
29 4 simp2bi Could not format ( ta -> ph' ) : No typesetting found for |- ( ta -> ph' ) with typecode |-
30 29 3ad2ant2 Could not format ( ( R _FrSe A /\ ta /\ si ) -> ph' ) : No typesetting found for |- ( ( R _FrSe A /\ ta /\ si ) -> ph' ) with typecode |-
31 eqtr ⊢ G ⁡ ∅ = f ⁡ ∅ ∧ f ⁡ ∅ = pred x A R → G ⁡ ∅ = pred x A R
32 1 31 sylan2b Could not format ( ( ( G ` (/) ) = ( f ` (/) ) /\ ph' ) -> ( G ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ( ( G ` (/) ) = ( f ` (/) ) /\ ph' ) -> ( G ` (/) ) = _pred ( x , A , R ) ) with typecode |-
33 32 7 sylibr Could not format ( ( ( G ` (/) ) = ( f ` (/) ) /\ ph' ) -> ph" ) : No typesetting found for |- ( ( ( G ` (/) ) = ( f ` (/) ) /\ ph' ) -> ph" ) with typecode |-
34 28 30 33 syl2anc Could not format ( ( R _FrSe A /\ ta /\ si ) -> ph" ) : No typesetting found for |- ( ( R _FrSe A /\ ta /\ si ) -> ph" ) with typecode |-