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

Metamath Proof Explorer

Theorem fnwe2

Description: A well-ordering can be constructed on a partitioned set by patching together well-orderings on each partition using a well-ordering on the partitions themselves. Similar to fnwe but does not require the within-partition ordering to be globally well. (Contributed by Stefan O'Rear, 19-Jan-2015)

Ref Expression
Hypotheses fnwe2.su 
|- ( z = ( F ` x ) -> S = U )
fnwe2.t 
|- T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }
fnwe2.s 
|- ( ( ph /\ x e. A ) -> U We { y e. A | ( F ` y ) = ( F ` x ) } )
fnwe2.f 
|- ( ph -> ( F |` A ) : A --> B )
fnwe2.r 
|- ( ph -> R We B )
Assertion fnwe2 
|- ( ph -> T We A )

Proof

Step Hyp Ref Expression
1 fnwe2.su 
 |-  ( z = ( F ` x ) -> S = U )
2 fnwe2.t 
 |-  T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }
3 fnwe2.s 
 |-  ( ( ph /\ x e. A ) -> U We { y e. A | ( F ` y ) = ( F ` x ) } )
4 fnwe2.f 
 |-  ( ph -> ( F |` A ) : A --> B )
5 fnwe2.r 
 |-  ( ph -> R We B )
6 3 adantlr 
 |-  ( ( ( ph /\ ( a C_ A /\ a =/= (/) ) ) /\ x e. A ) -> U We { y e. A | ( F ` y ) = ( F ` x ) } )
7 4 adantr 
 |-  ( ( ph /\ ( a C_ A /\ a =/= (/) ) ) -> ( F |` A ) : A --> B )
8 5 adantr 
 |-  ( ( ph /\ ( a C_ A /\ a =/= (/) ) ) -> R We B )
9 simprl 
 |-  ( ( ph /\ ( a C_ A /\ a =/= (/) ) ) -> a C_ A )
10 simprr 
 |-  ( ( ph /\ ( a C_ A /\ a =/= (/) ) ) -> a =/= (/) )
11 1 2 6 7 8 9 10 fnwe2lem2 
 |-  ( ( ph /\ ( a C_ A /\ a =/= (/) ) ) -> E. c e. a A. d e. a -. d T c )
12 11 ex 
 |-  ( ph -> ( ( a C_ A /\ a =/= (/) ) -> E. c e. a A. d e. a -. d T c ) )
13 12 alrimiv 
 |-  ( ph -> A. a ( ( a C_ A /\ a =/= (/) ) -> E. c e. a A. d e. a -. d T c ) )
14 df-fr 
 |-  ( T Fr A <-> A. a ( ( a C_ A /\ a =/= (/) ) -> E. c e. a A. d e. a -. d T c ) )
15 13 14 sylibr 
 |-  ( ph -> T Fr A )
16 3 adantlr 
 |-  ( ( ( ph /\ ( a e. A /\ b e. A ) ) /\ x e. A ) -> U We { y e. A | ( F ` y ) = ( F ` x ) } )
17 4 adantr 
 |-  ( ( ph /\ ( a e. A /\ b e. A ) ) -> ( F |` A ) : A --> B )
18 5 adantr 
 |-  ( ( ph /\ ( a e. A /\ b e. A ) ) -> R We B )
19 simprl 
 |-  ( ( ph /\ ( a e. A /\ b e. A ) ) -> a e. A )
20 simprr 
 |-  ( ( ph /\ ( a e. A /\ b e. A ) ) -> b e. A )
21 1 2 16 17 18 19 20 fnwe2lem3 
 |-  ( ( ph /\ ( a e. A /\ b e. A ) ) -> ( a T b \/ a = b \/ b T a ) )
22 21 ralrimivva 
 |-  ( ph -> A. a e. A A. b e. A ( a T b \/ a = b \/ b T a ) )
23 dfwe2 
 |-  ( T We A <-> ( T Fr A /\ A. a e. A A. b e. A ( a T b \/ a = b \/ b T a ) ) )
24 15 22 23 sylanbrc 
 |-  ( ph -> T We A )