Theorem weiunwe

Description: A well-ordering on an indexed union can be constructed from a well-ordering on its index set and a collection of well-orderings on its members. (Contributed by Matthew House, 23-Aug-2025)

	Ref	Expression
Hypotheses	weiunwe.1	|- F = ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) )
	weiunwe.2	|- T = { <. y , z >. | ( ( y e. U_ x e. A B /\ z e. U_ x e. A B ) /\ ( ( F ` y ) R ( F ` z ) \/ ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) ) }
Assertion	weiunwe	|- ( ( R We A /\ R Se A /\ A. x e. A S We B ) -> T We U_ x e. A B )

Proof

Step	Hyp	Ref	Expression
1		weiunwe.1	|- F = ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) )
2		weiunwe.2	|- T = { <. y , z >. | ( ( y e. U_ x e. A B /\ z e. U_ x e. A B ) /\ ( ( F ` y ) R ( F ` z ) \/ ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) ) }
3		wefr	|- ( S We B -> S Fr B )
4	3	ralimi	|- ( A. x e. A S We B -> A. x e. A S Fr B )
5	1 2	weiunfr	|- ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) -> T Fr U_ x e. A B )
6	4 5	syl3an3	|- ( ( R We A /\ R Se A /\ A. x e. A S We B ) -> T Fr U_ x e. A B )
7		weso	|- ( S We B -> S Or B )
8	7	ralimi	|- ( A. x e. A S We B -> A. x e. A S Or B )
9	1 2	weiunso	|- ( ( R We A /\ R Se A /\ A. x e. A S Or B ) -> T Or U_ x e. A B )
10	8 9	syl3an3	|- ( ( R We A /\ R Se A /\ A. x e. A S We B ) -> T Or U_ x e. A B )
11		df-we	|- ( T We U_ x e. A B <-> ( T Fr U_ x e. A B /\ T Or U_ x e. A B ) )
12	6 10 11	sylanbrc	|- ( ( R We A /\ R Se A /\ A. x e. A S We B ) -> T We U_ x e. A B )