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

Metamath Proof Explorer

Theorem bnj1519

Description: Technical lemma for bnj1500 . 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 bnj1519.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
bnj1519.2 ⊢ Y = x f ↾ pred x A R
bnj1519.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
bnj1519.4 ⊢ F = ⋃ C
Assertion bnj1519 ⊢ F ⁡ x = G ⁡ x F ↾ pred x A R → ∀ d F ⁡ x = G ⁡ x F ↾ pred x A R

Proof

Step Hyp Ref Expression
1 bnj1519.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj1519.2 ⊢ Y = x f ↾ pred x A R
3 bnj1519.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 bnj1519.4 ⊢ F = ⋃ C
5 nfre1 ⊢ Ⅎ d ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
6 5 nfab ⊢ Ⅎ _ d f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
7 3 6 nfcxfr ⊢ Ⅎ _ d C
8 7 nfuni ⊢ Ⅎ _ d ⋃ C
9 4 8 nfcxfr ⊢ Ⅎ _ d F
10 nfcv ⊢ Ⅎ _ d x
11 9 10 nffv ⊢ Ⅎ _ d F ⁡ x
12 nfcv ⊢ Ⅎ _ d G
13 nfcv ⊢ Ⅎ _ d pred x A R
14 9 13 nfres ⊢ Ⅎ _ d F ↾ pred x A R
15 10 14 nfop ⊢ Ⅎ _ d x F ↾ pred x A R
16 12 15 nffv ⊢ Ⅎ _ d G ⁡ x F ↾ pred x A R
17 11 16 nfeq ⊢ Ⅎ d F ⁡ x = G ⁡ x F ↾ pred x A R
18 17 nf5ri ⊢ F ⁡ x = G ⁡ x F ↾ pred x A R → ∀ d F ⁡ x = G ⁡ x F ↾ pred x A R