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

Metamath Proof Explorer

Theorem bnj1371

Description: Technical lemma for bnj60 . 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 bnj1371.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
bnj1371.2 ⊢ Y = x f ↾ pred x A R
bnj1371.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
bnj1371.4 ⊢ τ ↔ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
bnj1371.5 ⊢ D = x ∈ A | ¬ ∃ f τ
bnj1371.6 ⊢ ψ ↔ R FrSe A ∧ D ≠ ∅
bnj1371.7 ⊢ χ ↔ ψ ∧ x ∈ D ∧ ∀ y ∈ D ¬ y R x
bnj1371.8 No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
bnj1371.9 No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
bnj1371.10 ⊢ P = ⋃ H
bnj1371.11 No typesetting found for |- ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) with typecode |-
Assertion bnj1371 ⊢ f ∈ H → Fun ⁡ f

Proof

Step Hyp Ref Expression
1 bnj1371.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj1371.2 ⊢ Y = x f ↾ pred x A R
3 bnj1371.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 bnj1371.4 ⊢ τ ↔ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
5 bnj1371.5 ⊢ D = x ∈ A | ¬ ∃ f τ
6 bnj1371.6 ⊢ ψ ↔ R FrSe A ∧ D ≠ ∅
7 bnj1371.7 ⊢ χ ↔ ψ ∧ x ∈ D ∧ ∀ y ∈ D ¬ y R x
8 bnj1371.8 Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9 bnj1371.9 Could not format H = { f | E. y e. _pred ( x , A , R ) ta' } : No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
10 bnj1371.10 ⊢ P = ⋃ H
11 bnj1371.11 Could not format ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) : No typesetting found for |- ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) with typecode |-
12 9 bnj1436 Could not format ( f e. H -> E. y e. _pred ( x , A , R ) ta' ) : No typesetting found for |- ( f e. H -> E. y e. _pred ( x , A , R ) ta' ) with typecode |-
13 rexex Could not format ( E. y e. _pred ( x , A , R ) ta' -> E. y ta' ) : No typesetting found for |- ( E. y e. _pred ( x , A , R ) ta' -> E. y ta' ) with typecode |-
14 12 13 syl Could not format ( f e. H -> E. y ta' ) : No typesetting found for |- ( f e. H -> E. y ta' ) with typecode |-
15 11 exbii Could not format ( E. y ta' <-> E. y ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) : No typesetting found for |- ( E. y ta' <-> E. y ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) with typecode |-
16 14 15 sylib ⊢ f ∈ H → ∃ y f ∈ C ∧ dom ⁡ f = y ∪ trCl y A R
17 exsimpl ⊢ ∃ y f ∈ C ∧ dom ⁡ f = y ∪ trCl y A R → ∃ y f ∈ C
18 16 17 syl ⊢ f ∈ H → ∃ y f ∈ C
19 3 eqabri ⊢ f ∈ C ↔ ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
20 19 bnj1238 ⊢ f ∈ C → ∃ d ∈ B f Fn d
21 fnfun ⊢ f Fn d → Fun ⁡ f
22 20 21 bnj31 ⊢ f ∈ C → ∃ d ∈ B Fun ⁡ f
23 22 bnj1265 ⊢ f ∈ C → Fun ⁡ f
24 18 23 bnj593 ⊢ f ∈ H → ∃ y Fun ⁡ f
25 24 bnj937 ⊢ f ∈ H → Fun ⁡ f