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

Metamath Proof Explorer

Theorem bnj1445

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

Proof

Step Hyp Ref Expression
1 bnj1445.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj1445.2 ⊢ Y = x f ↾ pred x A R
3 bnj1445.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 bnj1445.4 ⊢ τ ↔ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
5 bnj1445.5 ⊢ D = x ∈ A | ¬ ∃ f τ
6 bnj1445.6 ⊢ ψ ↔ R FrSe A ∧ D ≠ ∅
7 bnj1445.7 ⊢ χ ↔ ψ ∧ x ∈ D ∧ ∀ y ∈ D ¬ y R x
8 bnj1445.8 Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9 bnj1445.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 bnj1445.10 ⊢ P = ⋃ H
11 bnj1445.11 ⊢ Z = x P ↾ pred x A R
12 bnj1445.12 ⊢ Q = P ∪ x G ⁡ Z
13 bnj1445.13 ⊢ W = z Q ↾ pred z A R
14 bnj1445.14 ⊢ E = x ∪ trCl x A R
15 bnj1445.15 ⊢ χ → P Fn trCl x A R
16 bnj1445.16 ⊢ χ → Q Fn x ∪ trCl x A R
17 bnj1445.17 ⊢ θ ↔ χ ∧ z ∈ E
18 bnj1445.18 ⊢ η ↔ θ ∧ z ∈ x
19 bnj1445.19 ⊢ ζ ↔ θ ∧ z ∈ trCl x A R
20 bnj1445.20 ⊢ ρ ↔ ζ ∧ f ∈ H ∧ z ∈ dom ⁡ f
21 bnj1445.21 ⊢ σ ↔ ρ ∧ y ∈ pred x A R ∧ f ∈ C ∧ dom ⁡ f = y ∪ trCl y A R
22 bnj1445.22 ⊢ φ ↔ σ ∧ d ∈ B ∧ f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
23 bnj1445.23 ⊢ X = z f ↾ pred z A R
24 nfv ⊢ Ⅎ d R FrSe A
25 nfre1 ⊢ Ⅎ d ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
26 25 nfab ⊢ Ⅎ _ d f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
27 3 26 nfcxfr ⊢ Ⅎ _ d C
28 27 nfcri ⊢ Ⅎ d f ∈ C
29 nfv ⊢ Ⅎ d dom ⁡ f = x ∪ trCl x A R
30 28 29 nfan ⊢ Ⅎ d f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
31 4 30 nfxfr ⊢ Ⅎ d τ
32 31 nfex ⊢ Ⅎ d ∃ f τ
33 32 nfn ⊢ Ⅎ d ¬ ∃ f τ
34 nfcv ⊢ Ⅎ _ d A
35 33 34 nfrabw ⊢ Ⅎ _ d x ∈ A | ¬ ∃ f τ
36 5 35 nfcxfr ⊢ Ⅎ _ d D
37 nfcv ⊢ Ⅎ _ d ∅
38 36 37 nfne ⊢ Ⅎ d D ≠ ∅
39 24 38 nfan ⊢ Ⅎ d R FrSe A ∧ D ≠ ∅
40 6 39 nfxfr ⊢ Ⅎ d ψ
41 36 nfcri ⊢ Ⅎ d x ∈ D
42 nfv ⊢ Ⅎ d ¬ y R x
43 36 42 nfralw ⊢ Ⅎ d ∀ y ∈ D ¬ y R x
44 40 41 43 nf3an ⊢ Ⅎ d ψ ∧ x ∈ D ∧ ∀ y ∈ D ¬ y R x
45 7 44 nfxfr ⊢ Ⅎ d χ
46 45 nf5ri ⊢ χ → ∀ d χ
47 46 bnj1351 ⊢ χ ∧ z ∈ E → ∀ d χ ∧ z ∈ E
48 47 nf5i ⊢ Ⅎ d χ ∧ z ∈ E
49 17 48 nfxfr ⊢ Ⅎ d θ
50 nfv ⊢ Ⅎ d z ∈ trCl x A R
51 49 50 nfan ⊢ Ⅎ d θ ∧ z ∈ trCl x A R
52 19 51 nfxfr ⊢ Ⅎ d ζ
53 nfcv ⊢ Ⅎ _ d pred x A R
54 nfcv ⊢ Ⅎ _ d y
55 54 31 nfsbcw ⊢ Ⅎ d [˙y / x]˙ τ
56 8 55 nfxfr Could not format F/ d ta' : No typesetting found for |- F/ d ta' with typecode |-
57 53 56 nfrexw Could not format F/ d E. y e. _pred ( x , A , R ) ta' : No typesetting found for |- F/ d E. y e. _pred ( x , A , R ) ta' with typecode |-
58 57 nfab Could not format F/_ d { f | E. y e. _pred ( x , A , R ) ta' } : No typesetting found for |- F/_ d { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
59 9 58 nfcxfr ⊢ Ⅎ _ d H
60 59 nfcri ⊢ Ⅎ d f ∈ H
61 nfv ⊢ Ⅎ d z ∈ dom ⁡ f
62 52 60 61 nf3an ⊢ Ⅎ d ζ ∧ f ∈ H ∧ z ∈ dom ⁡ f
63 20 62 nfxfr ⊢ Ⅎ d ρ
64 63 nf5ri ⊢ ρ → ∀ d ρ
65 ax-5 ⊢ y ∈ pred x A R → ∀ d y ∈ pred x A R
66 28 nf5ri ⊢ f ∈ C → ∀ d f ∈ C
67 ax-5 ⊢ dom ⁡ f = y ∪ trCl y A R → ∀ d dom ⁡ f = y ∪ trCl y A R
68 64 65 66 67 bnj982 ⊢ ρ ∧ y ∈ pred x A R ∧ f ∈ C ∧ dom ⁡ f = y ∪ trCl y A R → ∀ d ρ ∧ y ∈ pred x A R ∧ f ∈ C ∧ dom ⁡ f = y ∪ trCl y A R
69 21 68 hbxfrbi ⊢ σ → ∀ d σ