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

Metamath Proof Explorer

Theorem bnj1444

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 bnj1444.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
bnj1444.2 ⊢ Y = x f ↾ pred x A R
bnj1444.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
bnj1444.4 ⊢ τ ↔ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
bnj1444.5 ⊢ D = x ∈ A | ¬ ∃ f τ
bnj1444.6 ⊢ ψ ↔ R FrSe A ∧ D ≠ ∅
bnj1444.7 ⊢ χ ↔ ψ ∧ x ∈ D ∧ ∀ y ∈ D ¬ y R x
bnj1444.8 No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
bnj1444.9 No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
bnj1444.10 ⊢ P = ⋃ H
bnj1444.11 ⊢ Z = x P ↾ pred x A R
bnj1444.12 ⊢ Q = P ∪ x G ⁡ Z
bnj1444.13 ⊢ W = z Q ↾ pred z A R
bnj1444.14 ⊢ E = x ∪ trCl x A R
bnj1444.15 ⊢ χ → P Fn trCl x A R
bnj1444.16 ⊢ χ → Q Fn x ∪ trCl x A R
bnj1444.17 ⊢ θ ↔ χ ∧ z ∈ E
bnj1444.18 ⊢ η ↔ θ ∧ z ∈ x
bnj1444.19 ⊢ ζ ↔ θ ∧ z ∈ trCl x A R
bnj1444.20 ⊢ ρ ↔ ζ ∧ f ∈ H ∧ z ∈ dom ⁡ f
Assertion bnj1444 ⊢ ρ → ∀ y ρ

Proof

Step Hyp Ref Expression
1 bnj1444.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj1444.2 ⊢ Y = x f ↾ pred x A R
3 bnj1444.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 bnj1444.4 ⊢ τ ↔ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
5 bnj1444.5 ⊢ D = x ∈ A | ¬ ∃ f τ
6 bnj1444.6 ⊢ ψ ↔ R FrSe A ∧ D ≠ ∅
7 bnj1444.7 ⊢ χ ↔ ψ ∧ x ∈ D ∧ ∀ y ∈ D ¬ y R x
8 bnj1444.8 Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9 bnj1444.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 bnj1444.10 ⊢ P = ⋃ H
11 bnj1444.11 ⊢ Z = x P ↾ pred x A R
12 bnj1444.12 ⊢ Q = P ∪ x G ⁡ Z
13 bnj1444.13 ⊢ W = z Q ↾ pred z A R
14 bnj1444.14 ⊢ E = x ∪ trCl x A R
15 bnj1444.15 ⊢ χ → P Fn trCl x A R
16 bnj1444.16 ⊢ χ → Q Fn x ∪ trCl x A R
17 bnj1444.17 ⊢ θ ↔ χ ∧ z ∈ E
18 bnj1444.18 ⊢ η ↔ θ ∧ z ∈ x
19 bnj1444.19 ⊢ ζ ↔ θ ∧ z ∈ trCl x A R
20 bnj1444.20 ⊢ ρ ↔ ζ ∧ f ∈ H ∧ z ∈ dom ⁡ f
21 nfv ⊢ Ⅎ y ψ
22 nfv ⊢ Ⅎ y x ∈ D
23 nfra1 ⊢ Ⅎ y ∀ y ∈ D ¬ y R x
24 21 22 23 nf3an ⊢ Ⅎ y ψ ∧ x ∈ D ∧ ∀ y ∈ D ¬ y R x
25 7 24 nfxfr ⊢ Ⅎ y χ
26 nfv ⊢ Ⅎ y z ∈ E
27 25 26 nfan ⊢ Ⅎ y χ ∧ z ∈ E
28 17 27 nfxfr ⊢ Ⅎ y θ
29 nfv ⊢ Ⅎ y z ∈ trCl x A R
30 28 29 nfan ⊢ Ⅎ y θ ∧ z ∈ trCl x A R
31 19 30 nfxfr ⊢ Ⅎ y ζ
32 nfre1 Could not format F/ y E. y e. _pred ( x , A , R ) ta' : No typesetting found for |- F/ y E. y e. _pred ( x , A , R ) ta' with typecode |-
33 32 nfab Could not format F/_ y { f | E. y e. _pred ( x , A , R ) ta' } : No typesetting found for |- F/_ y { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
34 9 33 nfcxfr ⊢ Ⅎ _ y H
35 34 nfcri ⊢ Ⅎ y f ∈ H
36 nfv ⊢ Ⅎ y z ∈ dom ⁡ f
37 31 35 36 nf3an ⊢ Ⅎ y ζ ∧ f ∈ H ∧ z ∈ dom ⁡ f
38 20 37 nfxfr ⊢ Ⅎ y ρ
39 38 nf5ri ⊢ ρ → ∀ y ρ