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