Metamath Proof Explorer


Theorem bnj1498

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

Proof

Step Hyp Ref Expression
1 bnj1498.1 B = d | d A x d pred x A R d
2 bnj1498.2 Y = x f pred x A R
3 bnj1498.3 C = f | d B f Fn d x d f x = G Y
4 bnj1498.4 F = C
5 eliun z f C dom f f C z dom f
6 3 bnj1436 f C d B f Fn d x d f x = G Y
7 6 bnj1299 f C d B f Fn d
8 fndm f Fn d dom f = d
9 7 8 bnj31 f C d B dom f = d
10 9 bnj1196 f C d d B dom f = d
11 1 bnj1436 d B d A x d pred x A R d
12 11 simpld d B d A
13 12 anim1i d B dom f = d d A dom f = d
14 10 13 bnj593 f C d d A dom f = d
15 sseq1 dom f = d dom f A d A
16 15 biimparc d A dom f = d dom f A
17 14 16 bnj593 f C d dom f A
18 17 bnj937 f C dom f A
19 18 sselda f C z dom f z A
20 19 rexlimiva f C z dom f z A
21 5 20 sylbi z f C dom f z A
22 3 bnj1317 w C f w C
23 22 bnj1400 dom C = f C dom f
24 21 23 eleq2s z dom C z A
25 4 dmeqi dom F = dom C
26 24 25 eleq2s z dom F z A
27 26 ssriv dom F A
28 27 a1i R FrSe A dom F A
29 1 2 3 bnj1493 R FrSe A x A f C dom f = x trCl x A R
30 vsnid x x
31 elun1 x x x x trCl x A R
32 30 31 ax-mp x x trCl x A R
33 eleq2 dom f = x trCl x A R x dom f x x trCl x A R
34 32 33 mpbiri dom f = x trCl x A R x dom f
35 34 reximi f C dom f = x trCl x A R f C x dom f
36 35 ralimi x A f C dom f = x trCl x A R x A f C x dom f
37 29 36 syl R FrSe A x A f C x dom f
38 eliun x f C dom f f C x dom f
39 38 ralbii x A x f C dom f x A f C x dom f
40 37 39 sylibr R FrSe A x A x f C dom f
41 nfcv _ x A
42 1 bnj1309 t B x t B
43 3 42 bnj1307 t C x t C
44 43 nfcii _ x C
45 nfcv _ x dom f
46 44 45 nfiun _ x f C dom f
47 41 46 dfss3f A f C dom f x A x f C dom f
48 40 47 sylibr R FrSe A A f C dom f
49 48 23 sseqtrrdi R FrSe A A dom C
50 49 25 sseqtrrdi R FrSe A A dom F
51 28 50 eqssd R FrSe A dom F = A