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

Metamath Proof Explorer

Theorem bnj1491

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

Proof

Step Hyp Ref Expression
1 bnj1491.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj1491.2 ⊢ Y = x f ↾ pred x A R
3 bnj1491.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 bnj1491.4 ⊢ τ ↔ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
5 bnj1491.5 ⊢ D = x ∈ A | ¬ ∃ f τ
6 bnj1491.6 ⊢ ψ ↔ R FrSe A ∧ D ≠ ∅
7 bnj1491.7 ⊢ χ ↔ ψ ∧ x ∈ D ∧ ∀ y ∈ D ¬ y R x
8 bnj1491.8 Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9 bnj1491.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 bnj1491.10 ⊢ P = ⋃ H
11 bnj1491.11 ⊢ Z = x P ↾ pred x A R
12 bnj1491.12 ⊢ Q = P ∪ x G ⁡ Z
13 bnj1491.13 ⊢ χ → Q ∈ C ∧ dom ⁡ Q = x ∪ trCl x A R
14 1 2 3 4 5 6 7 8 9 10 11 12 bnj1466 ⊢ w ∈ Q → ∀ f w ∈ Q
15 14 nfcii ⊢ Ⅎ _ f Q
16 3 bnj1317 ⊢ w ∈ C → ∀ f w ∈ C
17 16 nfcii ⊢ Ⅎ _ f C
18 15 17 nfel ⊢ Ⅎ f Q ∈ C
19 15 nfdm ⊢ Ⅎ _ f dom ⁡ Q
20 19 nfeq1 ⊢ Ⅎ f dom ⁡ Q = x ∪ trCl x A R
21 18 20 nfan ⊢ Ⅎ f Q ∈ C ∧ dom ⁡ Q = x ∪ trCl x A R
22 eleq1 ⊢ f = Q → f ∈ C ↔ Q ∈ C
23 dmeq ⊢ f = Q → dom ⁡ f = dom ⁡ Q
24 23 eqeq1d ⊢ f = Q → dom ⁡ f = x ∪ trCl x A R ↔ dom ⁡ Q = x ∪ trCl x A R
25 22 24 anbi12d ⊢ f = Q → f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ↔ Q ∈ C ∧ dom ⁡ Q = x ∪ trCl x A R
26 15 21 25 spcegf ⊢ Q ∈ V → Q ∈ C ∧ dom ⁡ Q = x ∪ trCl x A R → ∃ f f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
27 13 26 mpan9 ⊢ χ ∧ Q ∈ V → ∃ f f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R