Metamath Proof Explorer

Theorem bnj1518

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

Proof

Step Hyp Ref Expression
1 bnj1518.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj1518.2 ⊢ Y = x f ↾ pred x A R
3 bnj1518.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 bnj1518.4 ⊢ F = ⋃ C
5 bnj1518.5 ⊢ φ ↔ R FrSe A ∧ x ∈ A
6 bnj1518.6 ⊢ ψ ↔ φ ∧ f ∈ C ∧ x ∈ dom ⁡ f
7 nfv ⊢ Ⅎ d φ
8 nfre1 ⊢ Ⅎ d ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
9 8 nfab ⊢ Ⅎ _ d f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
10 3 9 nfcxfr ⊢ Ⅎ _ d C
11 10 nfcri ⊢ Ⅎ d f ∈ C
12 nfv ⊢ Ⅎ d x ∈ dom ⁡ f
13 7 11 12 nf3an ⊢ Ⅎ d φ ∧ f ∈ C ∧ x ∈ dom ⁡ f
14 6 13 nfxfr ⊢ Ⅎ d ψ
15 14 nf5ri ⊢ ψ → ∀ d ψ