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

Metamath Proof Explorer

Theorem bnj1447

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

Proof

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