Metamath Proof Explorer

Theorem bnj1463

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

Proof

Step Hyp Ref Expression
1 bnj1463.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj1463.2 ⊢ Y = x f ↾ pred x A R
3 bnj1463.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 bnj1463.4 ⊢ τ ↔ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
5 bnj1463.5 ⊢ D = x ∈ A | ¬ ∃ f τ
6 bnj1463.6 ⊢ ψ ↔ R FrSe A ∧ D ≠ ∅
7 bnj1463.7 ⊢ χ ↔ ψ ∧ x ∈ D ∧ ∀ y ∈ D ¬ y R x
8 bnj1463.8 Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9 bnj1463.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 bnj1463.10 ⊢ P = ⋃ H
11 bnj1463.11 ⊢ Z = x P ↾ pred x A R
12 bnj1463.12 ⊢ Q = P ∪ x G ⁡ Z
13 bnj1463.13 ⊢ W = z Q ↾ pred z A R
14 bnj1463.14 ⊢ E = x ∪ trCl x A R
15 bnj1463.15 ⊢ χ → Q ∈ V
16 bnj1463.16 ⊢ χ → ∀ z ∈ E Q ⁡ z = G ⁡ W
17 bnj1463.17 ⊢ χ → Q Fn E
18 bnj1463.18 ⊢ χ → E ∈ B
19 18 elexd ⊢ χ → E ∈ V
20 eleq1 ⊢ d = E → d ∈ B ↔ E ∈ B
21 fneq2 ⊢ d = E → Q Fn d ↔ Q Fn E
22 raleq ⊢ d = E → ∀ z ∈ d Q ⁡ z = G ⁡ W ↔ ∀ z ∈ E Q ⁡ z = G ⁡ W
23 21 22 anbi12d ⊢ d = E → Q Fn d ∧ ∀ z ∈ d Q ⁡ z = G ⁡ W ↔ Q Fn E ∧ ∀ z ∈ E Q ⁡ z = G ⁡ W
24 20 23 anbi12d ⊢ d = E → d ∈ B ∧ Q Fn d ∧ ∀ z ∈ d Q ⁡ z = G ⁡ W ↔ E ∈ B ∧ Q Fn E ∧ ∀ z ∈ E Q ⁡ z = G ⁡ W
25 1 bnj1317 ⊢ w ∈ B → ∀ d w ∈ B
26 25 nfcii ⊢ Ⅎ _ d B
27 26 nfel2 ⊢ Ⅎ d E ∈ B
28 1 2 3 4 5 6 7 8 9 10 11 12 bnj1467 ⊢ w ∈ Q → ∀ d w ∈ Q
29 28 nfcii ⊢ Ⅎ _ d Q
30 nfcv ⊢ Ⅎ _ d E
31 29 30 nffn ⊢ Ⅎ d Q Fn E
32 1 2 3 4 5 6 7 8 9 10 11 12 13 bnj1446 ⊢ Q ⁡ z = G ⁡ W → ∀ d Q ⁡ z = G ⁡ W
33 32 nf5i ⊢ Ⅎ d Q ⁡ z = G ⁡ W
34 30 33 nfralw ⊢ Ⅎ d ∀ z ∈ E Q ⁡ z = G ⁡ W
35 31 34 nfan ⊢ Ⅎ d Q Fn E ∧ ∀ z ∈ E Q ⁡ z = G ⁡ W
36 27 35 nfan ⊢ Ⅎ d E ∈ B ∧ Q Fn E ∧ ∀ z ∈ E Q ⁡ z = G ⁡ W
37 36 nf5ri ⊢ E ∈ B ∧ Q Fn E ∧ ∀ z ∈ E Q ⁡ z = G ⁡ W → ∀ d E ∈ B ∧ Q Fn E ∧ ∀ z ∈ E Q ⁡ z = G ⁡ W
38 18 17 16 jca32 ⊢ χ → E ∈ B ∧ Q Fn E ∧ ∀ z ∈ E Q ⁡ z = G ⁡ W
39 24 37 38 bnj1465 ⊢ χ ∧ E ∈ V → ∃ d d ∈ B ∧ Q Fn d ∧ ∀ z ∈ d Q ⁡ z = G ⁡ W
40 19 39 mpdan ⊢ χ → ∃ d d ∈ B ∧ Q Fn d ∧ ∀ z ∈ d Q ⁡ z = G ⁡ W
41 df-rex ⊢ ∃ d ∈ B Q Fn d ∧ ∀ z ∈ d Q ⁡ z = G ⁡ W ↔ ∃ d d ∈ B ∧ Q Fn d ∧ ∀ z ∈ d Q ⁡ z = G ⁡ W
42 40 41 sylibr ⊢ χ → ∃ d ∈ B Q Fn d ∧ ∀ z ∈ d Q ⁡ z = G ⁡ W
43 nfcv ⊢ Ⅎ _ f B
44 1 2 3 4 5 6 7 8 9 10 11 12 bnj1466 ⊢ w ∈ Q → ∀ f w ∈ Q
45 44 nfcii ⊢ Ⅎ _ f Q
46 nfcv ⊢ Ⅎ _ f d
47 45 46 nffn ⊢ Ⅎ f Q Fn d
48 1 2 3 4 5 6 7 8 9 10 11 12 13 bnj1448 ⊢ Q ⁡ z = G ⁡ W → ∀ f Q ⁡ z = G ⁡ W
49 48 nf5i ⊢ Ⅎ f Q ⁡ z = G ⁡ W
50 46 49 nfralw ⊢ Ⅎ f ∀ z ∈ d Q ⁡ z = G ⁡ W
51 47 50 nfan ⊢ Ⅎ f Q Fn d ∧ ∀ z ∈ d Q ⁡ z = G ⁡ W
52 43 51 nfrex ⊢ Ⅎ f ∃ d ∈ B Q Fn d ∧ ∀ z ∈ d Q ⁡ z = G ⁡ W
53 52 nf5ri ⊢ ∃ d ∈ B Q Fn d ∧ ∀ z ∈ d Q ⁡ z = G ⁡ W → ∀ f ∃ d ∈ B Q Fn d ∧ ∀ z ∈ d Q ⁡ z = G ⁡ W
54 29 nfeq2 ⊢ Ⅎ d f = Q
55 fneq1 ⊢ f = Q → f Fn d ↔ Q Fn d
56 fveq1 ⊢ f = Q → f ⁡ z = Q ⁡ z
57 reseq1 ⊢ f = Q → f ↾ pred z A R = Q ↾ pred z A R
58 57 opeq2d ⊢ f = Q → z f ↾ pred z A R = z Q ↾ pred z A R
59 58 13 eqtr4di ⊢ f = Q → z f ↾ pred z A R = W
60 59 fveq2d ⊢ f = Q → G ⁡ z f ↾ pred z A R = G ⁡ W
61 56 60 eqeq12d ⊢ f = Q → f ⁡ z = G ⁡ z f ↾ pred z A R ↔ Q ⁡ z = G ⁡ W
62 61 ralbidv ⊢ f = Q → ∀ z ∈ d f ⁡ z = G ⁡ z f ↾ pred z A R ↔ ∀ z ∈ d Q ⁡ z = G ⁡ W
63 55 62 anbi12d ⊢ f = Q → f Fn d ∧ ∀ z ∈ d f ⁡ z = G ⁡ z f ↾ pred z A R ↔ Q Fn d ∧ ∀ z ∈ d Q ⁡ z = G ⁡ W
64 54 63 rexbid ⊢ f = Q → ∃ d ∈ B f Fn d ∧ ∀ z ∈ d f ⁡ z = G ⁡ z f ↾ pred z A R ↔ ∃ d ∈ B Q Fn d ∧ ∀ z ∈ d Q ⁡ z = G ⁡ W
65 53 64 44 bnj1468 ⊢ Q ∈ V → [˙Q / f]˙ ∃ d ∈ B f Fn d ∧ ∀ z ∈ d f ⁡ z = G ⁡ z f ↾ pred z A R ↔ ∃ d ∈ B Q Fn d ∧ ∀ z ∈ d Q ⁡ z = G ⁡ W
66 15 65 syl ⊢ χ → [˙Q / f]˙ ∃ d ∈ B f Fn d ∧ ∀ z ∈ d f ⁡ z = G ⁡ z f ↾ pred z A R ↔ ∃ d ∈ B Q Fn d ∧ ∀ z ∈ d Q ⁡ z = G ⁡ W
67 42 66 mpbird ⊢ χ → [˙Q / f]˙ ∃ d ∈ B f Fn d ∧ ∀ z ∈ d f ⁡ z = G ⁡ z f ↾ pred z A R
68 fveq2 ⊢ x = z → f ⁡ x = f ⁡ z
69 id ⊢ x = z → x = z
70 bnj602 ⊢ x = z → pred x A R = pred z A R
71 70 reseq2d ⊢ x = z → f ↾ pred x A R = f ↾ pred z A R
72 69 71 opeq12d ⊢ x = z → x f ↾ pred x A R = z f ↾ pred z A R
73 2 72 syl5eq ⊢ x = z → Y = z f ↾ pred z A R
74 73 fveq2d ⊢ x = z → G ⁡ Y = G ⁡ z f ↾ pred z A R
75 68 74 eqeq12d ⊢ x = z → f ⁡ x = G ⁡ Y ↔ f ⁡ z = G ⁡ z f ↾ pred z A R
76 75 cbvralvw ⊢ ∀ x ∈ d f ⁡ x = G ⁡ Y ↔ ∀ z ∈ d f ⁡ z = G ⁡ z f ↾ pred z A R
77 76 anbi2i ⊢ f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y ↔ f Fn d ∧ ∀ z ∈ d f ⁡ z = G ⁡ z f ↾ pred z A R
78 77 rexbii ⊢ ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y ↔ ∃ d ∈ B f Fn d ∧ ∀ z ∈ d f ⁡ z = G ⁡ z f ↾ pred z A R
79 78 sbcbii ⊢ [˙Q / f]˙ ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y ↔ [˙Q / f]˙ ∃ d ∈ B f Fn d ∧ ∀ z ∈ d f ⁡ z = G ⁡ z f ↾ pred z A R
80 67 79 sylibr ⊢ χ → [˙Q / f]˙ ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
81 3 bnj1454 ⊢ Q ∈ V → Q ∈ C ↔ [˙Q / f]˙ ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
82 15 81 syl ⊢ χ → Q ∈ C ↔ [˙Q / f]˙ ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
83 80 82 mpbird ⊢ χ → Q ∈ C