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

Metamath Proof Explorer

Theorem bnj1446

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

Proof

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