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 C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
bnj1498.2
|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
bnj1498.3
|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
bnj1498.4
|- F = U. C
Assertion bnj1498
|- ( R _FrSe A -> dom F = A )

Proof

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