Metamath Proof Explorer


Theorem bnj1398

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 bnj1398.1 B=d|dAxdpredxARd
bnj1398.2 Y=xfpredxAR
bnj1398.3 C=f|dBfFndxdfx=GY
bnj1398.4 τfCdomf=xtrClxAR
bnj1398.5 D=xA|¬fτ
bnj1398.6 ψRFrSeAD
bnj1398.7 χψxDyD¬yRx
bnj1398.8 No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
bnj1398.9 No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
bnj1398.10 P=H
bnj1398.11 θχzypredxARytrClyAR
bnj1398.12 ηθypredxARzytrClyAR
Assertion bnj1398 χypredxARytrClyAR=domP

Proof

Step Hyp Ref Expression
1 bnj1398.1 B=d|dAxdpredxARd
2 bnj1398.2 Y=xfpredxAR
3 bnj1398.3 C=f|dBfFndxdfx=GY
4 bnj1398.4 τfCdomf=xtrClxAR
5 bnj1398.5 D=xA|¬fτ
6 bnj1398.6 ψRFrSeAD
7 bnj1398.7 χψxDyD¬yRx
8 bnj1398.8 Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9 bnj1398.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 bnj1398.10 P=H
11 bnj1398.11 θχzypredxARytrClyAR
12 bnj1398.12 ηθypredxARzytrClyAR
13 df-iun ypredxARytrClyAR=z|ypredxARzytrClyAR
14 13 bnj1436 zypredxARytrClyARypredxARzytrClyAR
15 11 14 simplbiim θypredxARzytrClyAR
16 nfv yψ
17 nfv yxD
18 nfra1 yyD¬yRx
19 16 17 18 nf3an yψxDyD¬yRx
20 7 19 nfxfr yχ
21 nfiu1 _yypredxARytrClyAR
22 21 nfcri yzypredxARytrClyAR
23 20 22 nfan yχzypredxARytrClyAR
24 11 23 nfxfr yθ
25 24 nf5ri θyθ
26 15 12 25 bnj1521 θyη
27 nfv fRFrSeA
28 nfe1 ffτ
29 28 nfn f¬fτ
30 nfcv _fA
31 29 30 nfrabw _fxA|¬fτ
32 5 31 nfcxfr _fD
33 nfcv _f
34 32 33 nfne fD
35 27 34 nfan fRFrSeAD
36 6 35 nfxfr fψ
37 32 nfcri fxD
38 nfv f¬yRx
39 32 38 nfralw fyD¬yRx
40 36 37 39 nf3an fψxDyD¬yRx
41 7 40 nfxfr fχ
42 nfv fzypredxARytrClyAR
43 41 42 nfan fχzypredxARytrClyAR
44 11 43 nfxfr fθ
45 nfv fypredxAR
46 nfv fzytrClyAR
47 44 45 46 nf3an fθypredxARzytrClyAR
48 12 47 nfxfr fη
49 48 nf5ri ηfη
50 11 simplbi θχ
51 12 50 bnj835 ηχ
52 12 simp2bi ηypredxAR
53 1 2 3 4 5 6 7 8 bnj1388 Could not format ( ch -> A. y e. _pred ( x , A , R ) E. f ta' ) : No typesetting found for |- ( ch -> A. y e. _pred ( x , A , R ) E. f ta' ) with typecode |-
54 rsp Could not format ( A. y e. _pred ( x , A , R ) E. f ta' -> ( y e. _pred ( x , A , R ) -> E. f ta' ) ) : No typesetting found for |- ( A. y e. _pred ( x , A , R ) E. f ta' -> ( y e. _pred ( x , A , R ) -> E. f ta' ) ) with typecode |-
55 53 54 syl Could not format ( ch -> ( y e. _pred ( x , A , R ) -> E. f ta' ) ) : No typesetting found for |- ( ch -> ( y e. _pred ( x , A , R ) -> E. f ta' ) ) with typecode |-
56 51 52 55 sylc Could not format ( et -> E. f ta' ) : No typesetting found for |- ( et -> E. f ta' ) with typecode |-
57 49 56 bnj596 Could not format ( et -> E. f ( et /\ ta' ) ) : No typesetting found for |- ( et -> E. f ( et /\ ta' ) ) with typecode |-
58 1 2 3 4 8 bnj1373 Could not format ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) : No typesetting found for |- ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) with typecode |-
59 58 simplbi Could not format ( ta' -> f e. C ) : No typesetting found for |- ( ta' -> f e. C ) with typecode |-
60 59 adantl Could not format ( ( et /\ ta' ) -> f e. C ) : No typesetting found for |- ( ( et /\ ta' ) -> f e. C ) with typecode |-
61 58 simprbi Could not format ( ta' -> dom f = ( { y } u. _trCl ( y , A , R ) ) ) : No typesetting found for |- ( ta' -> dom f = ( { y } u. _trCl ( y , A , R ) ) ) with typecode |-
62 rspe ypredxARdomf=ytrClyARypredxARdomf=ytrClyAR
63 52 61 62 syl2an Could not format ( ( et /\ ta' ) -> E. y e. _pred ( x , A , R ) dom f = ( { y } u. _trCl ( y , A , R ) ) ) : No typesetting found for |- ( ( et /\ ta' ) -> E. y e. _pred ( x , A , R ) dom f = ( { y } u. _trCl ( y , A , R ) ) ) with typecode |-
64 9 abeq2i Could not format ( f e. H <-> E. y e. _pred ( x , A , R ) ta' ) : No typesetting found for |- ( f e. H <-> E. y e. _pred ( x , A , R ) ta' ) with typecode |-
65 58 rexbii Could not format ( E. y e. _pred ( x , A , R ) ta' <-> E. y e. _pred ( x , A , R ) ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) : No typesetting found for |- ( E. y e. _pred ( x , A , R ) ta' <-> E. y e. _pred ( x , A , R ) ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) with typecode |-
66 r19.42v ypredxARfCdomf=ytrClyARfCypredxARdomf=ytrClyAR
67 64 65 66 3bitri fHfCypredxARdomf=ytrClyAR
68 60 63 67 sylanbrc Could not format ( ( et /\ ta' ) -> f e. H ) : No typesetting found for |- ( ( et /\ ta' ) -> f e. H ) with typecode |-
69 12 simp3bi ηzytrClyAR
70 69 adantr Could not format ( ( et /\ ta' ) -> z e. ( { y } u. _trCl ( y , A , R ) ) ) : No typesetting found for |- ( ( et /\ ta' ) -> z e. ( { y } u. _trCl ( y , A , R ) ) ) with typecode |-
71 61 adantl Could not format ( ( et /\ ta' ) -> dom f = ( { y } u. _trCl ( y , A , R ) ) ) : No typesetting found for |- ( ( et /\ ta' ) -> dom f = ( { y } u. _trCl ( y , A , R ) ) ) with typecode |-
72 70 71 eleqtrrd Could not format ( ( et /\ ta' ) -> z e. dom f ) : No typesetting found for |- ( ( et /\ ta' ) -> z e. dom f ) with typecode |-
73 68 72 jca Could not format ( ( et /\ ta' ) -> ( f e. H /\ z e. dom f ) ) : No typesetting found for |- ( ( et /\ ta' ) -> ( f e. H /\ z e. dom f ) ) with typecode |-
74 57 73 bnj593 ηffHzdomf
75 df-rex fHzdomfffHzdomf
76 74 75 sylibr ηfHzdomf
77 10 dmeqi domP=domH
78 9 bnj1317 wHfwH
79 78 bnj1400 domH=fHdomf
80 77 79 eqtri domP=fHdomf
81 80 eleq2i zdomPzfHdomf
82 eliun zfHdomffHzdomf
83 81 82 bitri zdomPfHzdomf
84 76 83 sylibr ηzdomP
85 26 84 bnj593 θyzdomP
86 nfre1 Could not format F/ y E. y e. _pred ( x , A , R ) ta' : No typesetting found for |- F/ y E. y e. _pred ( x , A , R ) ta' with typecode |-
87 86 nfab Could not format F/_ y { f | E. y e. _pred ( x , A , R ) ta' } : No typesetting found for |- F/_ y { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
88 9 87 nfcxfr _yH
89 88 nfuni _yH
90 10 89 nfcxfr _yP
91 90 nfdm _ydomP
92 91 nfcrii zdomPyzdomP
93 85 92 bnj1397 θzdomP
94 11 93 sylbir χzypredxARytrClyARzdomP
95 94 ex χzypredxARytrClyARzdomP
96 95 ssrdv χypredxARytrClyARdomP
97 simpr fHzdomfzdomf
98 67 simprbi fHypredxARdomf=ytrClyAR
99 98 adantr fHzdomfypredxARdomf=ytrClyAR
100 r19.42v ypredxARzdomfdomf=ytrClyARzdomfypredxARdomf=ytrClyAR
101 eleq2 domf=ytrClyARzdomfzytrClyAR
102 101 biimpac zdomfdomf=ytrClyARzytrClyAR
103 102 reximi ypredxARzdomfdomf=ytrClyARypredxARzytrClyAR
104 100 103 sylbir zdomfypredxARdomf=ytrClyARypredxARzytrClyAR
105 97 99 104 syl2anc fHzdomfypredxARzytrClyAR
106 105 rexlimiva fHzdomfypredxARzytrClyAR
107 eliun zypredxARytrClyARypredxARzytrClyAR
108 106 83 107 3imtr4i zdomPzypredxARytrClyAR
109 108 ssriv domPypredxARytrClyAR
110 109 a1i χdomPypredxARytrClyAR
111 96 110 eqssd χypredxARytrClyAR=domP