Metamath Proof Explorer

Theorem fnse

Description: Condition for the well-order in fnwe to be set-like. (Contributed by Mario Carneiro, 25-Jun-2015)

Ref Expression
Hypotheses fnse.1 
|- T = { <. x , y >. | ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x S y ) ) ) }
fnse.2 
|- ( ph -> F : A --> B )
fnse.3 
|- ( ph -> R Se B )
fnse.4 
|- ( ph -> ( `' F " w ) e. _V )
Assertion fnse 
|- ( ph -> T Se A )

Proof

Step Hyp Ref Expression
1 fnse.1 
 |-  T = { <. x , y >. | ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x S y ) ) ) }
2 fnse.2 
 |-  ( ph -> F : A --> B )
3 fnse.3 
 |-  ( ph -> R Se B )
4 fnse.4 
 |-  ( ph -> ( `' F " w ) e. _V )
5 2 ffvelrnda 
 |-  ( ( ph /\ z e. A ) -> ( F ` z ) e. B )
6 seex 
 |-  ( ( R Se B /\ ( F ` z ) e. B ) -> { u e. B | u R ( F ` z ) } e. _V )
7 3 5 6 syl2an2r 
 |-  ( ( ph /\ z e. A ) -> { u e. B | u R ( F ` z ) } e. _V )
8 snex 
 |-  { ( F ` z ) } e. _V
9 unexg 
 |-  ( ( { u e. B | u R ( F ` z ) } e. _V /\ { ( F ` z ) } e. _V ) -> ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) e. _V )
10 7 8 9 sylancl 
 |-  ( ( ph /\ z e. A ) -> ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) e. _V )
11 imaeq2 
 |-  ( w = ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) -> ( `' F " w ) = ( `' F " ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) ) )
12 11 eleq1d 
 |-  ( w = ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) -> ( ( `' F " w ) e. _V <-> ( `' F " ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) ) e. _V ) )
13 12 imbi2d 
 |-  ( w = ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) -> ( ( ph -> ( `' F " w ) e. _V ) <-> ( ph -> ( `' F " ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) ) e. _V ) ) )
14 13 4 vtoclg 
 |-  ( ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) e. _V -> ( ph -> ( `' F " ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) ) e. _V ) )
15 14 impcom 
 |-  ( ( ph /\ ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) e. _V ) -> ( `' F " ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) ) e. _V )
16 10 15 syldan 
 |-  ( ( ph /\ z e. A ) -> ( `' F " ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) ) e. _V )
17 inss2 
 |-  ( A i^i ( `' T " { z } ) ) C_ ( `' T " { z } )
18 vex 
 |-  w e. _V
19 18 eliniseg 
 |-  ( z e. _V -> ( w e. ( `' T " { z } ) <-> w T z ) )
20 19 elv 
 |-  ( w e. ( `' T " { z } ) <-> w T z )
21 fveq2 
 |-  ( x = w -> ( F ` x ) = ( F ` w ) )
22 fveq2 
 |-  ( y = z -> ( F ` y ) = ( F ` z ) )
23 21 22 breqan12d 
 |-  ( ( x = w /\ y = z ) -> ( ( F ` x ) R ( F ` y ) <-> ( F ` w ) R ( F ` z ) ) )
24 21 22 eqeqan12d 
 |-  ( ( x = w /\ y = z ) -> ( ( F ` x ) = ( F ` y ) <-> ( F ` w ) = ( F ` z ) ) )
25 breq12 
 |-  ( ( x = w /\ y = z ) -> ( x S y <-> w S z ) )
26 24 25 anbi12d 
 |-  ( ( x = w /\ y = z ) -> ( ( ( F ` x ) = ( F ` y ) /\ x S y ) <-> ( ( F ` w ) = ( F ` z ) /\ w S z ) ) )
27 23 26 orbi12d 
 |-  ( ( x = w /\ y = z ) -> ( ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x S y ) ) <-> ( ( F ` w ) R ( F ` z ) \/ ( ( F ` w ) = ( F ` z ) /\ w S z ) ) ) )
28 27 1 brab2a 
 |-  ( w T z <-> ( ( w e. A /\ z e. A ) /\ ( ( F ` w ) R ( F ` z ) \/ ( ( F ` w ) = ( F ` z ) /\ w S z ) ) ) )
29 2 ffvelrnda 
 |-  ( ( ph /\ w e. A ) -> ( F ` w ) e. B )
30 29 adantrr 
 |-  ( ( ph /\ ( w e. A /\ z e. A ) ) -> ( F ` w ) e. B )
31 breq1 
 |-  ( u = ( F ` w ) -> ( u R ( F ` z ) <-> ( F ` w ) R ( F ` z ) ) )
32 31 elrab3 
 |-  ( ( F ` w ) e. B -> ( ( F ` w ) e. { u e. B | u R ( F ` z ) } <-> ( F ` w ) R ( F ` z ) ) )
33 30 32 syl 
 |-  ( ( ph /\ ( w e. A /\ z e. A ) ) -> ( ( F ` w ) e. { u e. B | u R ( F ` z ) } <-> ( F ` w ) R ( F ` z ) ) )
34 33 biimprd 
 |-  ( ( ph /\ ( w e. A /\ z e. A ) ) -> ( ( F ` w ) R ( F ` z ) -> ( F ` w ) e. { u e. B | u R ( F ` z ) } ) )
35 simpl 
 |-  ( ( ( F ` w ) = ( F ` z ) /\ w S z ) -> ( F ` w ) = ( F ` z ) )
36 fvex 
 |-  ( F ` w ) e. _V
37 36 elsn 
 |-  ( ( F ` w ) e. { ( F ` z ) } <-> ( F ` w ) = ( F ` z ) )
38 35 37 sylibr 
 |-  ( ( ( F ` w ) = ( F ` z ) /\ w S z ) -> ( F ` w ) e. { ( F ` z ) } )
39 38 a1i 
 |-  ( ( ph /\ ( w e. A /\ z e. A ) ) -> ( ( ( F ` w ) = ( F ` z ) /\ w S z ) -> ( F ` w ) e. { ( F ` z ) } ) )
40 34 39 orim12d 
 |-  ( ( ph /\ ( w e. A /\ z e. A ) ) -> ( ( ( F ` w ) R ( F ` z ) \/ ( ( F ` w ) = ( F ` z ) /\ w S z ) ) -> ( ( F ` w ) e. { u e. B | u R ( F ` z ) } \/ ( F ` w ) e. { ( F ` z ) } ) ) )
41 elun 
 |-  ( ( F ` w ) e. ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) <-> ( ( F ` w ) e. { u e. B | u R ( F ` z ) } \/ ( F ` w ) e. { ( F ` z ) } ) )
42 40 41 syl6ibr 
 |-  ( ( ph /\ ( w e. A /\ z e. A ) ) -> ( ( ( F ` w ) R ( F ` z ) \/ ( ( F ` w ) = ( F ` z ) /\ w S z ) ) -> ( F ` w ) e. ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) ) )
43 simprl 
 |-  ( ( ph /\ ( w e. A /\ z e. A ) ) -> w e. A )
44 42 43 jctild 
 |-  ( ( ph /\ ( w e. A /\ z e. A ) ) -> ( ( ( F ` w ) R ( F ` z ) \/ ( ( F ` w ) = ( F ` z ) /\ w S z ) ) -> ( w e. A /\ ( F ` w ) e. ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) ) ) )
45 2 ffnd 
 |-  ( ph -> F Fn A )
46 45 adantr 
 |-  ( ( ph /\ ( w e. A /\ z e. A ) ) -> F Fn A )
47 elpreima 
 |-  ( F Fn A -> ( w e. ( `' F " ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) ) <-> ( w e. A /\ ( F ` w ) e. ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) ) ) )
48 46 47 syl 
 |-  ( ( ph /\ ( w e. A /\ z e. A ) ) -> ( w e. ( `' F " ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) ) <-> ( w e. A /\ ( F ` w ) e. ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) ) ) )
49 44 48 sylibrd 
 |-  ( ( ph /\ ( w e. A /\ z e. A ) ) -> ( ( ( F ` w ) R ( F ` z ) \/ ( ( F ` w ) = ( F ` z ) /\ w S z ) ) -> w e. ( `' F " ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) ) ) )
50 49 expimpd 
 |-  ( ph -> ( ( ( w e. A /\ z e. A ) /\ ( ( F ` w ) R ( F ` z ) \/ ( ( F ` w ) = ( F ` z ) /\ w S z ) ) ) -> w e. ( `' F " ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) ) ) )
51 28 50 syl5bi 
 |-  ( ph -> ( w T z -> w e. ( `' F " ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) ) ) )
52 20 51 syl5bi 
 |-  ( ph -> ( w e. ( `' T " { z } ) -> w e. ( `' F " ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) ) ) )
53 52 ssrdv 
 |-  ( ph -> ( `' T " { z } ) C_ ( `' F " ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) ) )
54 17 53 sstrid 
 |-  ( ph -> ( A i^i ( `' T " { z } ) ) C_ ( `' F " ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) ) )
55 54 adantr 
 |-  ( ( ph /\ z e. A ) -> ( A i^i ( `' T " { z } ) ) C_ ( `' F " ( { u e. B | u R ( F ` z ) } u. { ( F ` z ) } ) ) )
56 16 55 ssexd 
 |-  ( ( ph /\ z e. A ) -> ( A i^i ( `' T " { z } ) ) e. _V )
57 56 ralrimiva 
 |-  ( ph -> A. z e. A ( A i^i ( `' T " { z } ) ) e. _V )
58 dfse2 
 |-  ( T Se A <-> A. z e. A ( A i^i ( `' T " { z } ) ) e. _V )
59 57 58 sylibr 
 |-  ( ph -> T Se A )