This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )