Metamath Proof Explorer


Theorem bnj1321

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 bnj1321.1 B = d | d A x d pred x A R d
bnj1321.2 Y = x f pred x A R
bnj1321.3 C = f | d B f Fn d x d f x = G Y
bnj1321.4 τ f C dom f = x trCl x A R
Assertion bnj1321 R FrSe A f τ ∃! f τ

Proof

Step Hyp Ref Expression
1 bnj1321.1 B = d | d A x d pred x A R d
2 bnj1321.2 Y = x f pred x A R
3 bnj1321.3 C = f | d B f Fn d x d f x = G Y
4 bnj1321.4 τ f C dom f = x trCl x A R
5 simpr R FrSe A f τ f τ
6 simp1 R FrSe A τ g f τ R FrSe A
7 4 simplbi τ f C
8 7 3ad2ant2 R FrSe A τ g f τ f C
9 nfab1 _ f f | d B f Fn d x d f x = G Y
10 3 9 nfcxfr _ f C
11 10 nfcri f g C
12 nfv f dom g = x trCl x A R
13 11 12 nfan f g C dom g = x trCl x A R
14 eleq1w f = g f C g C
15 dmeq f = g dom f = dom g
16 15 eqeq1d f = g dom f = x trCl x A R dom g = x trCl x A R
17 14 16 anbi12d f = g f C dom f = x trCl x A R g C dom g = x trCl x A R
18 4 17 syl5bb f = g τ g C dom g = x trCl x A R
19 13 18 sbiev g f τ g C dom g = x trCl x A R
20 19 simplbi g f τ g C
21 20 3ad2ant3 R FrSe A τ g f τ g C
22 eqid dom f dom g = dom f dom g
23 1 2 3 22 bnj1326 R FrSe A f C g C f dom f dom g = g dom f dom g
24 6 8 21 23 syl3anc R FrSe A τ g f τ f dom f dom g = g dom f dom g
25 4 simprbi τ dom f = x trCl x A R
26 25 3ad2ant2 R FrSe A τ g f τ dom f = x trCl x A R
27 19 simprbi g f τ dom g = x trCl x A R
28 27 3ad2ant3 R FrSe A τ g f τ dom g = x trCl x A R
29 26 28 eqtr4d R FrSe A τ g f τ dom f = dom g
30 bnj1322 dom f = dom g dom f dom g = dom f
31 30 reseq2d dom f = dom g f dom f dom g = f dom f
32 29 31 syl R FrSe A τ g f τ f dom f dom g = f dom f
33 releq z = f Rel z Rel f
34 1 2 3 bnj66 z C Rel z
35 33 34 vtoclga f C Rel f
36 resdm Rel f f dom f = f
37 8 35 36 3syl R FrSe A τ g f τ f dom f = f
38 32 37 eqtrd R FrSe A τ g f τ f dom f dom g = f
39 eqeq2 dom f = dom g dom f dom g = dom f dom f dom g = dom g
40 30 39 mpbid dom f = dom g dom f dom g = dom g
41 40 reseq2d dom f = dom g g dom f dom g = g dom g
42 29 41 syl R FrSe A τ g f τ g dom f dom g = g dom g
43 1 2 3 bnj66 g C Rel g
44 resdm Rel g g dom g = g
45 21 43 44 3syl R FrSe A τ g f τ g dom g = g
46 42 45 eqtrd R FrSe A τ g f τ g dom f dom g = g
47 24 38 46 3eqtr3d R FrSe A τ g f τ f = g
48 47 3expib R FrSe A τ g f τ f = g
49 48 alrimivv R FrSe A f g τ g f τ f = g
50 49 adantr R FrSe A f τ f g τ g f τ f = g
51 nfv g τ
52 51 eu2 ∃! f τ f τ f g τ g f τ f = g
53 5 50 52 sylanbrc R FrSe A f τ ∃! f τ