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 )