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

Metamath Proof Explorer

Theorem bnj1448

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

Proof

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