Metamath Proof Explorer

Theorem weiunso

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

Ref Expression
Hypotheses weiun.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 ) )
weiun.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 weiunso 
|- ( ( R We A /\ R Se A /\ A. x e. A S Or B ) -> T Or U_ x e. A B )

Proof

Step Hyp Ref Expression
1 weiun.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 weiun.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 sopo 
 |-  ( S Or B -> S Po B )
4 3 ralimi 
 |-  ( A. x e. A S Or B -> A. x e. A S Po B )
5 1 2 weiunpo 
 |-  ( ( R We A /\ R Se A /\ A. x e. A S Po B ) -> T Po U_ x e. A B )
6 4 5 syl3an3 
 |-  ( ( R We A /\ R Se A /\ A. x e. A S Or B ) -> T Po U_ x e. A B )
7 simplrl 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) R ( F ` r ) ) -> q e. U_ x e. A B )
8 simplrr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) R ( F ` r ) ) -> r e. U_ x e. A B )
9 animorrl 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) R ( F ` r ) ) -> ( ( F ` q ) R ( F ` r ) \/ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) )
10 1 2 weiunlem1 
 |-  ( q T r <-> ( ( q e. U_ x e. A B /\ r e. U_ x e. A B ) /\ ( ( F ` q ) R ( F ` r ) \/ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) )
11 7 8 9 10 syl21anbrc 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) R ( F ` r ) ) -> q T r )
12 11 3mix1d 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) R ( F ` r ) ) -> ( q T r \/ q = r \/ r T q ) )
13 csbeq1 
 |-  ( s = ( F ` q ) -> [_ s / x ]_ S = [_ ( F ` q ) / x ]_ S )
14 csbeq1 
 |-  ( s = ( F ` q ) -> [_ s / x ]_ B = [_ ( F ` q ) / x ]_ B )
15 13 14 soeq12d 
 |-  ( s = ( F ` q ) -> ( [_ s / x ]_ S Or [_ s / x ]_ B <-> [_ ( F ` q ) / x ]_ S Or [_ ( F ` q ) / x ]_ B ) )
16 simpll3 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) -> A. x e. A S Or B )
17 nfv 
 |-  F/ s S Or B
18 nfcsb1v 
 |-  F/_ x [_ s / x ]_ S
19 nfcsb1v 
 |-  F/_ x [_ s / x ]_ B
20 18 19 nfso 
 |-  F/ x [_ s / x ]_ S Or [_ s / x ]_ B
21 csbeq1a 
 |-  ( x = s -> S = [_ s / x ]_ S )
22 csbeq1a 
 |-  ( x = s -> B = [_ s / x ]_ B )
23 21 22 soeq12d 
 |-  ( x = s -> ( S Or B <-> [_ s / x ]_ S Or [_ s / x ]_ B ) )
24 17 20 23 cbvralw 
 |-  ( A. x e. A S Or B <-> A. s e. A [_ s / x ]_ S Or [_ s / x ]_ B )
25 16 24 sylib 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) -> A. s e. A [_ s / x ]_ S Or [_ s / x ]_ B )
26 simpl1 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> R We A )
27 simpl2 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> R Se A )
28 1 2 26 27 weiunlem2 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> ( F : U_ x e. A B --> A /\ A. t e. U_ x e. A B t e. [_ ( F ` t ) / x ]_ B /\ A. s e. A A. t e. [_ s / x ]_ B -. s R ( F ` t ) ) )
29 28 simp1d 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> F : U_ x e. A B --> A )
30 simprl 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> q e. U_ x e. A B )
31 29 30 ffvelcdmd 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> ( F ` q ) e. A )
32 31 adantr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) -> ( F ` q ) e. A )
33 15 25 32 rspcdva 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) -> [_ ( F ` q ) / x ]_ S Or [_ ( F ` q ) / x ]_ B )
34 id 
 |-  ( t = q -> t = q )
35 fveq2 
 |-  ( t = q -> ( F ` t ) = ( F ` q ) )
36 35 csbeq1d 
 |-  ( t = q -> [_ ( F ` t ) / x ]_ B = [_ ( F ` q ) / x ]_ B )
37 34 36 eleq12d 
 |-  ( t = q -> ( t e. [_ ( F ` t ) / x ]_ B <-> q e. [_ ( F ` q ) / x ]_ B ) )
38 28 simp2d 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> A. t e. U_ x e. A B t e. [_ ( F ` t ) / x ]_ B )
39 38 adantr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) -> A. t e. U_ x e. A B t e. [_ ( F ` t ) / x ]_ B )
40 simplrl 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) -> q e. U_ x e. A B )
41 37 39 40 rspcdva 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) -> q e. [_ ( F ` q ) / x ]_ B )
42 id 
 |-  ( t = r -> t = r )
43 fveq2 
 |-  ( t = r -> ( F ` t ) = ( F ` r ) )
44 43 csbeq1d 
 |-  ( t = r -> [_ ( F ` t ) / x ]_ B = [_ ( F ` r ) / x ]_ B )
45 42 44 eleq12d 
 |-  ( t = r -> ( t e. [_ ( F ` t ) / x ]_ B <-> r e. [_ ( F ` r ) / x ]_ B ) )
46 simplrr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) -> r e. U_ x e. A B )
47 45 39 46 rspcdva 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) -> r e. [_ ( F ` r ) / x ]_ B )
48 simpr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) -> ( F ` q ) = ( F ` r ) )
49 48 csbeq1d 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) -> [_ ( F ` q ) / x ]_ B = [_ ( F ` r ) / x ]_ B )
50 47 49 eleqtrrd 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) -> r e. [_ ( F ` q ) / x ]_ B )
51 solin 
 |-  ( ( [_ ( F ` q ) / x ]_ S Or [_ ( F ` q ) / x ]_ B /\ ( q e. [_ ( F ` q ) / x ]_ B /\ r e. [_ ( F ` q ) / x ]_ B ) ) -> ( q [_ ( F ` q ) / x ]_ S r \/ q = r \/ r [_ ( F ` q ) / x ]_ S q ) )
52 33 41 50 51 syl12anc 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) -> ( q [_ ( F ` q ) / x ]_ S r \/ q = r \/ r [_ ( F ` q ) / x ]_ S q ) )
53 simpllr 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) /\ q [_ ( F ` q ) / x ]_ S r ) -> ( q e. U_ x e. A B /\ r e. U_ x e. A B ) )
54 48 anim1i 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) /\ q [_ ( F ` q ) / x ]_ S r ) -> ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) )
55 54 olcd 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) /\ q [_ ( F ` q ) / x ]_ S r ) -> ( ( F ` q ) R ( F ` r ) \/ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) )
56 53 55 10 sylanbrc 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) /\ q [_ ( F ` q ) / x ]_ S r ) -> q T r )
57 56 ex 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) -> ( q [_ ( F ` q ) / x ]_ S r -> q T r ) )
58 idd 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) -> ( q = r -> q = r ) )
59 46 adantr 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) /\ r [_ ( F ` q ) / x ]_ S q ) -> r e. U_ x e. A B )
60 40 adantr 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) /\ r [_ ( F ` q ) / x ]_ S q ) -> q e. U_ x e. A B )
61 simplr 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) /\ r [_ ( F ` q ) / x ]_ S q ) -> ( F ` q ) = ( F ` r ) )
62 61 eqcomd 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) /\ r [_ ( F ` q ) / x ]_ S q ) -> ( F ` r ) = ( F ` q ) )
63 61 csbeq1d 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) /\ r [_ ( F ` q ) / x ]_ S q ) -> [_ ( F ` q ) / x ]_ S = [_ ( F ` r ) / x ]_ S )
64 simpr 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) /\ r [_ ( F ` q ) / x ]_ S q ) -> r [_ ( F ` q ) / x ]_ S q )
65 63 64 breqdi 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) /\ r [_ ( F ` q ) / x ]_ S q ) -> r [_ ( F ` r ) / x ]_ S q )
66 62 65 jca 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) /\ r [_ ( F ` q ) / x ]_ S q ) -> ( ( F ` r ) = ( F ` q ) /\ r [_ ( F ` r ) / x ]_ S q ) )
67 66 olcd 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) /\ r [_ ( F ` q ) / x ]_ S q ) -> ( ( F ` r ) R ( F ` q ) \/ ( ( F ` r ) = ( F ` q ) /\ r [_ ( F ` r ) / x ]_ S q ) ) )
68 1 2 weiunlem1 
 |-  ( r T q <-> ( ( r e. U_ x e. A B /\ q e. U_ x e. A B ) /\ ( ( F ` r ) R ( F ` q ) \/ ( ( F ` r ) = ( F ` q ) /\ r [_ ( F ` r ) / x ]_ S q ) ) ) )
69 59 60 67 68 syl21anbrc 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) /\ r [_ ( F ` q ) / x ]_ S q ) -> r T q )
70 69 ex 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) -> ( r [_ ( F ` q ) / x ]_ S q -> r T q ) )
71 57 58 70 3orim123d 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) -> ( ( q [_ ( F ` q ) / x ]_ S r \/ q = r \/ r [_ ( F ` q ) / x ]_ S q ) -> ( q T r \/ q = r \/ r T q ) ) )
72 52 71 mpd 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` q ) = ( F ` r ) ) -> ( q T r \/ q = r \/ r T q ) )
73 simplrr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` r ) R ( F ` q ) ) -> r e. U_ x e. A B )
74 simplrl 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` r ) R ( F ` q ) ) -> q e. U_ x e. A B )
75 animorrl 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` r ) R ( F ` q ) ) -> ( ( F ` r ) R ( F ` q ) \/ ( ( F ` r ) = ( F ` q ) /\ r [_ ( F ` r ) / x ]_ S q ) ) )
76 73 74 75 68 syl21anbrc 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` r ) R ( F ` q ) ) -> r T q )
77 76 3mix3d 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( F ` r ) R ( F ` q ) ) -> ( q T r \/ q = r \/ r T q ) )
78 weso 
 |-  ( R We A -> R Or A )
79 26 78 syl 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> R Or A )
80 simprr 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> r e. U_ x e. A B )
81 29 80 ffvelcdmd 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> ( F ` r ) e. A )
82 solin 
 |-  ( ( R Or A /\ ( ( F ` q ) e. A /\ ( F ` r ) e. A ) ) -> ( ( F ` q ) R ( F ` r ) \/ ( F ` q ) = ( F ` r ) \/ ( F ` r ) R ( F ` q ) ) )
83 79 31 81 82 syl12anc 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> ( ( F ` q ) R ( F ` r ) \/ ( F ` q ) = ( F ` r ) \/ ( F ` r ) R ( F ` q ) ) )
84 12 72 77 83 mpjao3dan 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Or B ) /\ ( q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> ( q T r \/ q = r \/ r T q ) )
85 6 84 issod 
 |-  ( ( R We A /\ R Se A /\ A. x e. A S Or B ) -> T Or U_ x e. A B )