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

Metamath Proof Explorer

Theorem bnj1449

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

Proof

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