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

Metamath Proof Explorer

Theorem bnj1520

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

Proof

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