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

Metamath Proof Explorer

Theorem bnj1442

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

Proof

Step Hyp Ref Expression
1 bnj1442.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj1442.2 ⊢ Y = x f ↾ pred x A R
3 bnj1442.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 bnj1442.4 ⊢ τ ↔ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
5 bnj1442.5 ⊢ D = x ∈ A | ¬ ∃ f τ
6 bnj1442.6 ⊢ ψ ↔ R FrSe A ∧ D ≠ ∅
7 bnj1442.7 ⊢ χ ↔ ψ ∧ x ∈ D ∧ ∀ y ∈ D ¬ y R x
8 bnj1442.8 Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9 bnj1442.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 bnj1442.10 ⊢ P = ⋃ H
11 bnj1442.11 ⊢ Z = x P ↾ pred x A R
12 bnj1442.12 ⊢ Q = P ∪ x G ⁡ Z
13 bnj1442.13 ⊢ W = z Q ↾ pred z A R
14 bnj1442.14 ⊢ E = x ∪ trCl x A R
15 bnj1442.15 ⊢ χ → P Fn trCl x A R
16 bnj1442.16 ⊢ χ → Q Fn x ∪ trCl x A R
17 bnj1442.17 ⊢ θ ↔ χ ∧ z ∈ E
18 bnj1442.18 ⊢ η ↔ θ ∧ z ∈ x
19 16 fnfund ⊢ χ → Fun ⁡ Q
20 opex ⊢ x G ⁡ Z ∈ V
21 20 snid ⊢ x G ⁡ Z ∈ x G ⁡ Z
22 elun2 ⊢ x G ⁡ Z ∈ x G ⁡ Z → x G ⁡ Z ∈ P ∪ x G ⁡ Z
23 21 22 ax-mp ⊢ x G ⁡ Z ∈ P ∪ x G ⁡ Z
24 23 12 eleqtrri ⊢ x G ⁡ Z ∈ Q
25 funopfv ⊢ Fun ⁡ Q → x G ⁡ Z ∈ Q → Q ⁡ x = G ⁡ Z
26 19 24 25 mpisyl ⊢ χ → Q ⁡ x = G ⁡ Z
27 17 26 bnj832 ⊢ θ → Q ⁡ x = G ⁡ Z
28 18 27 bnj832 ⊢ η → Q ⁡ x = G ⁡ Z
29 elsni ⊢ z ∈ x → z = x
30 18 29 simplbiim ⊢ η → z = x
31 30 fveq2d ⊢ η → Q ⁡ z = Q ⁡ x
32 bnj602 ⊢ z = x → pred z A R = pred x A R
33 32 reseq2d ⊢ z = x → Q ↾ pred z A R = Q ↾ pred x A R
34 30 33 syl ⊢ η → Q ↾ pred z A R = Q ↾ pred x A R
35 12 bnj931 ⊢ P ⊆ Q
36 35 a1i ⊢ χ → P ⊆ Q
37 6 simplbi ⊢ ψ → R FrSe A
38 7 37 bnj835 ⊢ χ → R FrSe A
39 5 7 bnj1212 ⊢ χ → x ∈ A
40 bnj906 ⊢ R FrSe A ∧ x ∈ A → pred x A R ⊆ trCl x A R
41 38 39 40 syl2anc ⊢ χ → pred x A R ⊆ trCl x A R
42 15 fndmd ⊢ χ → dom ⁡ P = trCl x A R
43 41 42 sseqtrrd ⊢ χ → pred x A R ⊆ dom ⁡ P
44 19 36 43 bnj1503 ⊢ χ → Q ↾ pred x A R = P ↾ pred x A R
45 17 44 bnj832 ⊢ θ → Q ↾ pred x A R = P ↾ pred x A R
46 18 45 bnj832 ⊢ η → Q ↾ pred x A R = P ↾ pred x A R
47 34 46 eqtrd ⊢ η → Q ↾ pred z A R = P ↾ pred x A R
48 30 47 opeq12d ⊢ η → z Q ↾ pred z A R = x P ↾ pred x A R
49 48 13 11 3eqtr4g ⊢ η → W = Z
50 49 fveq2d ⊢ η → G ⁡ W = G ⁡ Z
51 28 31 50 3eqtr4d ⊢ η → Q ⁡ z = G ⁡ W