Metamath Proof Explorer


Theorem bnj1312

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 bnj1312.1 B = d | d A x d pred x A R d
bnj1312.2 Y = x f pred x A R
bnj1312.3 C = f | d B f Fn d x d f x = G Y
bnj1312.4 τ f C dom f = x trCl x A R
bnj1312.5 D = x A | ¬ f τ
bnj1312.6 ψ R FrSe A D
bnj1312.7 χ ψ x D y D ¬ y R x
bnj1312.8 No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
bnj1312.9 No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
bnj1312.10 P = H
bnj1312.11 Z = x P pred x A R
bnj1312.12 Q = P x G Z
bnj1312.13 W = z Q pred z A R
bnj1312.14 E = x trCl x A R
Assertion bnj1312 R FrSe A x A f C dom f = x trCl x A R

Proof

Step Hyp Ref Expression
1 bnj1312.1 B = d | d A x d pred x A R d
2 bnj1312.2 Y = x f pred x A R
3 bnj1312.3 C = f | d B f Fn d x d f x = G Y
4 bnj1312.4 τ f C dom f = x trCl x A R
5 bnj1312.5 D = x A | ¬ f τ
6 bnj1312.6 ψ R FrSe A D
7 bnj1312.7 χ ψ x D y D ¬ y R x
8 bnj1312.8 Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9 bnj1312.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 bnj1312.10 P = H
11 bnj1312.11 Z = x P pred x A R
12 bnj1312.12 Q = P x G Z
13 bnj1312.13 W = z Q pred z A R
14 bnj1312.14 E = x trCl x A R
15 6 simplbi ψ R FrSe A
16 5 ssrab3 D A
17 16 a1i ψ D A
18 6 simprbi ψ D
19 5 bnj1230 w D x w D
20 19 bnj1228 R FrSe A D A D x D y D ¬ y R x
21 15 17 18 20 syl3anc ψ x D y D ¬ y R x
22 nfv x R FrSe A
23 19 nfcii _ x D
24 nfcv _ x
25 23 24 nfne x D
26 22 25 nfan x R FrSe A D
27 6 26 nfxfr x ψ
28 27 nf5ri ψ x ψ
29 21 7 28 bnj1521 ψ x χ
30 7 simp2bi χ x D
31 5 bnj1538 x D ¬ f τ
32 1 2 3 4 5 6 7 8 9 10 11 12 bnj1489 χ Q V
33 7 15 bnj835 χ R FrSe A
34 1 2 3 4 5 6 7 8 9 10 bnj1384 R FrSe A Fun P
35 33 34 syl χ Fun P
36 1 2 3 4 5 6 7 8 9 10 bnj1415 χ dom P = trCl x A R
37 35 36 bnj1422 χ P Fn trCl x A R
38 1 2 3 4 5 6 7 8 9 10 11 12 36 bnj1416 χ dom Q = x trCl x A R
39 1 2 3 4 5 6 7 8 9 10 11 12 35 38 36 bnj1421 χ Fun Q
40 39 38 bnj1422 χ Q Fn x trCl x A R
41 1 2 3 4 5 6 7 8 9 10 11 12 13 14 37 40 bnj1423 χ z E Q z = G W
42 14 fneq2i Q Fn E Q Fn x trCl x A R
43 40 42 sylibr χ Q Fn E
44 1 2 3 4 5 6 7 8 9 10 11 12 13 14 bnj1452 χ E B
45 1 2 3 4 5 6 7 8 9 10 11 12 13 14 32 41 43 44 bnj1463 χ Q C
46 45 38 jca χ Q C dom Q = x trCl x A R
47 1 2 3 4 5 6 7 8 9 10 11 12 46 bnj1491 χ Q V f f C dom f = x trCl x A R
48 32 47 mpdan χ f f C dom f = x trCl x A R
49 48 4 bnj1198 χ f τ
50 31 49 nsyl3 χ ¬ x D
51 29 30 50 bnj1304 ¬ ψ
52 6 51 bnj1541 R FrSe A D =
53 5 52 bnj1476 R FrSe A x A f τ
54 4 exbii f τ f f C dom f = x trCl x A R
55 df-rex f C dom f = x trCl x A R f f C dom f = x trCl x A R
56 54 55 bitr4i f τ f C dom f = x trCl x A R
57 56 ralbii x A f τ x A f C dom f = x trCl x A R
58 53 57 sylib R FrSe A x A f C dom f = x trCl x A R