Metamath Proof Explorer

Theorem weiunso

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

Ref Expression
Hypotheses weiunso.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 ) )
weiunso.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 weiunso.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 weiunso.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 simpl 
 |-  ( ( y = q /\ z = r ) -> y = q )
11 10 fveq2d 
 |-  ( ( y = q /\ z = r ) -> ( F ` y ) = ( F ` q ) )
12 simpr 
 |-  ( ( y = q /\ z = r ) -> z = r )
13 12 fveq2d 
 |-  ( ( y = q /\ z = r ) -> ( F ` z ) = ( F ` r ) )
14 11 13 breq12d 
 |-  ( ( y = q /\ z = r ) -> ( ( F ` y ) R ( F ` z ) <-> ( F ` q ) R ( F ` r ) ) )
15 11 13 eqeq12d 
 |-  ( ( y = q /\ z = r ) -> ( ( F ` y ) = ( F ` z ) <-> ( F ` q ) = ( F ` r ) ) )
16 11 csbeq1d 
 |-  ( ( y = q /\ z = r ) -> [_ ( F ` y ) / x ]_ S = [_ ( F ` q ) / x ]_ S )
17 10 16 12 breq123d 
 |-  ( ( y = q /\ z = r ) -> ( y [_ ( F ` y ) / x ]_ S z <-> q [_ ( F ` q ) / x ]_ S r ) )
18 15 17 anbi12d 
 |-  ( ( y = q /\ z = r ) -> ( ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) <-> ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) )
19 14 18 orbi12d 
 |-  ( ( y = q /\ z = r ) -> ( ( ( F ` y ) R ( F ` z ) \/ ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) <-> ( ( F ` q ) R ( F ` r ) \/ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) )
20 19 2 brab2a 
 |-  ( 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 ) ) ) )
21 7 8 9 20 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 )
22 21 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 ) )
23 csbeq1 
 |-  ( s = ( F ` q ) -> [_ s / x ]_ S = [_ ( F ` q ) / x ]_ S )
24 soeq1 
 |-  ( [_ s / x ]_ S = [_ ( F ` q ) / x ]_ S -> ( [_ s / x ]_ S Or [_ s / x ]_ B <-> [_ ( F ` q ) / x ]_ S Or [_ s / x ]_ B ) )
25 23 24 syl 
 |-  ( s = ( F ` q ) -> ( [_ s / x ]_ S Or [_ s / x ]_ B <-> [_ ( F ` q ) / x ]_ S Or [_ s / x ]_ B ) )
26 csbeq1 
 |-  ( s = ( F ` q ) -> [_ s / x ]_ B = [_ ( F ` q ) / x ]_ B )
27 soeq2 
 |-  ( [_ s / x ]_ B = [_ ( F ` q ) / x ]_ B -> ( [_ ( F ` q ) / x ]_ S Or [_ s / x ]_ B <-> [_ ( F ` q ) / x ]_ S Or [_ ( F ` q ) / x ]_ B ) )
28 26 27 syl 
 |-  ( s = ( F ` q ) -> ( [_ ( F ` q ) / x ]_ S Or [_ s / x ]_ B <-> [_ ( F ` q ) / x ]_ S Or [_ ( F ` q ) / x ]_ B ) )
29 25 28 bitrd 
 |-  ( s = ( F ` q ) -> ( [_ s / x ]_ S Or [_ s / x ]_ B <-> [_ ( F ` q ) / x ]_ S Or [_ ( F ` q ) / x ]_ B ) )
30 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 )
31 nfv 
 |-  F/ s S Or B
32 nfcsb1v 
 |-  F/_ x [_ s / x ]_ S
33 nfcsb1v 
 |-  F/_ x [_ s / x ]_ B
34 32 33 nfso 
 |-  F/ x [_ s / x ]_ S Or [_ s / x ]_ B
35 csbeq1a 
 |-  ( x = s -> S = [_ s / x ]_ S )
36 soeq1 
 |-  ( S = [_ s / x ]_ S -> ( S Or B <-> [_ s / x ]_ S Or B ) )
37 35 36 syl 
 |-  ( x = s -> ( S Or B <-> [_ s / x ]_ S Or B ) )
38 csbeq1a 
 |-  ( x = s -> B = [_ s / x ]_ B )
39 soeq2 
 |-  ( B = [_ s / x ]_ B -> ( [_ s / x ]_ S Or B <-> [_ s / x ]_ S Or [_ s / x ]_ B ) )
40 38 39 syl 
 |-  ( x = s -> ( [_ s / x ]_ S Or B <-> [_ s / x ]_ S Or [_ s / x ]_ B ) )
41 37 40 bitrd 
 |-  ( x = s -> ( S Or B <-> [_ s / x ]_ S Or [_ s / x ]_ B ) )
42 31 34 41 cbvralw 
 |-  ( A. x e. A S Or B <-> A. s e. A [_ s / x ]_ S Or [_ s / x ]_ B )
43 30 42 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 )
44 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 )
45 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 )
46 1 weiunlem2 
 |-  ( ( R We A /\ R Se A ) -> ( F : U_ x e. A B --> A /\ A. t e. U_ x e. A B t e. [_ ( F ` t ) / x ]_ B /\ A. t e. U_ x e. A B A. s e. A ( t e. [_ s / x ]_ B -> -. s R ( F ` t ) ) ) )
47 44 45 46 syl2anc 
 |-  ( ( ( 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. t e. U_ x e. A B A. s e. A ( t e. [_ s / x ]_ B -> -. s R ( F ` t ) ) ) )
48 47 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 )
49 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 )
50 48 49 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 )
51 50 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 )
52 29 43 51 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 )
53 id 
 |-  ( t = q -> t = q )
54 fveq2 
 |-  ( t = q -> ( F ` t ) = ( F ` q ) )
55 54 csbeq1d 
 |-  ( t = q -> [_ ( F ` t ) / x ]_ B = [_ ( F ` q ) / x ]_ B )
56 53 55 eleq12d 
 |-  ( t = q -> ( t e. [_ ( F ` t ) / x ]_ B <-> q e. [_ ( F ` q ) / x ]_ B ) )
57 47 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 )
58 57 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 )
59 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 )
60 56 58 59 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 )
61 id 
 |-  ( t = r -> t = r )
62 fveq2 
 |-  ( t = r -> ( F ` t ) = ( F ` r ) )
63 62 csbeq1d 
 |-  ( t = r -> [_ ( F ` t ) / x ]_ B = [_ ( F ` r ) / x ]_ B )
64 61 63 eleq12d 
 |-  ( t = r -> ( t e. [_ ( F ` t ) / x ]_ B <-> r e. [_ ( F ` r ) / x ]_ B ) )
65 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 )
66 64 58 65 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 )
67 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 ) )
68 67 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 )
69 66 68 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 )
70 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 ) )
71 52 60 69 70 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 ) )
72 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 ) )
73 67 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 ) )
74 73 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 ) ) )
75 72 74 20 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 )
76 75 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 ) )
77 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 ) )
78 65 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 )
79 59 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 )
80 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 ) )
81 80 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 ) )
82 80 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 )
83 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 )
84 82 83 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 )
85 81 84 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 ) )
86 85 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 ) ) )
87 simpl 
 |-  ( ( y = r /\ z = q ) -> y = r )
88 87 fveq2d 
 |-  ( ( y = r /\ z = q ) -> ( F ` y ) = ( F ` r ) )
89 simpr 
 |-  ( ( y = r /\ z = q ) -> z = q )
90 89 fveq2d 
 |-  ( ( y = r /\ z = q ) -> ( F ` z ) = ( F ` q ) )
91 88 90 breq12d 
 |-  ( ( y = r /\ z = q ) -> ( ( F ` y ) R ( F ` z ) <-> ( F ` r ) R ( F ` q ) ) )
92 88 90 eqeq12d 
 |-  ( ( y = r /\ z = q ) -> ( ( F ` y ) = ( F ` z ) <-> ( F ` r ) = ( F ` q ) ) )
93 88 csbeq1d 
 |-  ( ( y = r /\ z = q ) -> [_ ( F ` y ) / x ]_ S = [_ ( F ` r ) / x ]_ S )
94 87 93 89 breq123d 
 |-  ( ( y = r /\ z = q ) -> ( y [_ ( F ` y ) / x ]_ S z <-> r [_ ( F ` r ) / x ]_ S q ) )
95 92 94 anbi12d 
 |-  ( ( y = r /\ z = q ) -> ( ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) <-> ( ( F ` r ) = ( F ` q ) /\ r [_ ( F ` r ) / x ]_ S q ) ) )
96 91 95 orbi12d 
 |-  ( ( y = r /\ z = q ) -> ( ( ( F ` y ) R ( F ` z ) \/ ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) <-> ( ( F ` r ) R ( F ` q ) \/ ( ( F ` r ) = ( F ` q ) /\ r [_ ( F ` r ) / x ]_ S q ) ) ) )
97 96 2 brab2a 
 |-  ( 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 ) ) ) )
98 78 79 86 97 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 )
99 98 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 ) )
100 76 77 99 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 ) ) )
101 71 100 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 ) )
102 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 )
103 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 )
104 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 ) ) )
105 102 103 104 97 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 )
106 105 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 ) )
107 weso 
 |-  ( R We A -> R Or A )
108 44 107 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 )
109 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 )
110 48 109 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 )
111 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 ) ) )
112 108 50 110 111 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 ) ) )
113 22 101 106 112 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 ) )
114 6 113 issod 
 |-  ( ( R We A /\ R Se A /\ A. x e. A S Or B ) -> T Or U_ x e. A B )