Metamath Proof Explorer

Theorem weiunpo

Description: A partial ordering on an indexed union can be constructed from a well-ordering on its index class and a collection of partial 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 weiunpo 
|- ( ( R We A /\ R Se A /\ A. x e. A S Po B ) -> T Po 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 simpl1 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> R We A )
4 weso 
 |-  ( R We A -> R Or A )
5 3 4 syl 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> R Or A )
6 simpl2 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> R Se A )
7 1 2 3 6 weiunlem2 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A 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 ) ) )
8 7 simp1d 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> F : U_ x e. A B --> A )
9 simpr1 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> p e. U_ x e. A B )
10 8 9 ffvelcdmd 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> ( F ` p ) e. A )
11 sonr 
 |-  ( ( R Or A /\ ( F ` p ) e. A ) -> -. ( F ` p ) R ( F ` p ) )
12 5 10 11 syl2anc 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> -. ( F ` p ) R ( F ` p ) )
13 csbeq1 
 |-  ( s = ( F ` p ) -> [_ s / x ]_ S = [_ ( F ` p ) / x ]_ S )
14 csbeq1 
 |-  ( s = ( F ` p ) -> [_ s / x ]_ B = [_ ( F ` p ) / x ]_ B )
15 13 14 poeq12d 
 |-  ( s = ( F ` p ) -> ( [_ s / x ]_ S Po [_ s / x ]_ B <-> [_ ( F ` p ) / x ]_ S Po [_ ( F ` p ) / x ]_ B ) )
16 simpl3 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> A. x e. A S Po B )
17 nfv 
 |-  F/ s S Po B
18 nfcsb1v 
 |-  F/_ x [_ s / x ]_ S
19 nfcsb1v 
 |-  F/_ x [_ s / x ]_ B
20 18 19 nfpo 
 |-  F/ x [_ s / x ]_ S Po [_ s / x ]_ B
21 csbeq1a 
 |-  ( x = s -> S = [_ s / x ]_ S )
22 csbeq1a 
 |-  ( x = s -> B = [_ s / x ]_ B )
23 21 22 poeq12d 
 |-  ( x = s -> ( S Po B <-> [_ s / x ]_ S Po [_ s / x ]_ B ) )
24 17 20 23 cbvralw 
 |-  ( A. x e. A S Po B <-> A. s e. A [_ s / x ]_ S Po [_ s / x ]_ B )
25 16 24 sylib 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> A. s e. A [_ s / x ]_ S Po [_ s / x ]_ B )
26 15 25 10 rspcdva 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> [_ ( F ` p ) / x ]_ S Po [_ ( F ` p ) / x ]_ B )
27 id 
 |-  ( t = p -> t = p )
28 fveq2 
 |-  ( t = p -> ( F ` t ) = ( F ` p ) )
29 28 csbeq1d 
 |-  ( t = p -> [_ ( F ` t ) / x ]_ B = [_ ( F ` p ) / x ]_ B )
30 27 29 eleq12d 
 |-  ( t = p -> ( t e. [_ ( F ` t ) / x ]_ B <-> p e. [_ ( F ` p ) / x ]_ B ) )
31 7 simp2d 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A 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 )
32 30 31 9 rspcdva 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> p e. [_ ( F ` p ) / x ]_ B )
33 poirr 
 |-  ( ( [_ ( F ` p ) / x ]_ S Po [_ ( F ` p ) / x ]_ B /\ p e. [_ ( F ` p ) / x ]_ B ) -> -. p [_ ( F ` p ) / x ]_ S p )
34 26 32 33 syl2anc 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> -. p [_ ( F ` p ) / x ]_ S p )
35 34 intnand 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> -. ( ( F ` p ) = ( F ` p ) /\ p [_ ( F ` p ) / x ]_ S p ) )
36 ioran 
 |-  ( -. ( ( F ` p ) R ( F ` p ) \/ ( ( F ` p ) = ( F ` p ) /\ p [_ ( F ` p ) / x ]_ S p ) ) <-> ( -. ( F ` p ) R ( F ` p ) /\ -. ( ( F ` p ) = ( F ` p ) /\ p [_ ( F ` p ) / x ]_ S p ) ) )
37 12 35 36 sylanbrc 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> -. ( ( F ` p ) R ( F ` p ) \/ ( ( F ` p ) = ( F ` p ) /\ p [_ ( F ` p ) / x ]_ S p ) ) )
38 1 2 weiunlem1 
 |-  ( p T p <-> ( ( p e. U_ x e. A B /\ p e. U_ x e. A B ) /\ ( ( F ` p ) R ( F ` p ) \/ ( ( F ` p ) = ( F ` p ) /\ p [_ ( F ` p ) / x ]_ S p ) ) ) )
39 38 simprbi 
 |-  ( p T p -> ( ( F ` p ) R ( F ` p ) \/ ( ( F ` p ) = ( F ` p ) /\ p [_ ( F ` p ) / x ]_ S p ) ) )
40 37 39 nsyl 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> -. p T p )
41 simpr3 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> r e. U_ x e. A B )
42 9 41 jca 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> ( p e. U_ x e. A B /\ r e. U_ x e. A B ) )
43 1 2 weiunlem1 
 |-  ( p T q <-> ( ( p e. U_ x e. A B /\ q e. U_ x e. A B ) /\ ( ( F ` p ) R ( F ` q ) \/ ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) ) ) )
44 43 simprbi 
 |-  ( p T q -> ( ( F ` p ) R ( F ` q ) \/ ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) ) )
45 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 ) ) ) )
46 45 simprbi 
 |-  ( q T r -> ( ( F ` q ) R ( F ` r ) \/ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) )
47 simpr2 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> q e. U_ x e. A B )
48 8 47 ffvelcdmd 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> ( F ` q ) e. A )
49 8 41 ffvelcdmd 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> ( F ` r ) e. A )
50 sotr 
 |-  ( ( R Or A /\ ( ( F ` p ) e. A /\ ( F ` q ) e. A /\ ( F ` r ) e. A ) ) -> ( ( ( F ` p ) R ( F ` q ) /\ ( F ` q ) R ( F ` r ) ) -> ( F ` p ) R ( F ` r ) ) )
51 5 10 48 49 50 syl13anc 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> ( ( ( F ` p ) R ( F ` q ) /\ ( F ` q ) R ( F ` r ) ) -> ( F ` p ) R ( F ` r ) ) )
52 orc 
 |-  ( ( F ` p ) R ( F ` r ) -> ( ( F ` p ) R ( F ` r ) \/ ( ( F ` p ) = ( F ` r ) /\ p [_ ( F ` p ) / x ]_ S r ) ) )
53 51 52 syl6 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> ( ( ( F ` p ) R ( F ` q ) /\ ( F ` q ) R ( F ` r ) ) -> ( ( F ` p ) R ( F ` r ) \/ ( ( F ` p ) = ( F ` r ) /\ p [_ ( F ` p ) / x ]_ S r ) ) ) )
54 simprll 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( F ` q ) R ( F ` r ) ) ) -> ( F ` p ) = ( F ` q ) )
55 simprr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( F ` q ) R ( F ` r ) ) ) -> ( F ` q ) R ( F ` r ) )
56 54 55 eqbrtrd 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( F ` q ) R ( F ` r ) ) ) -> ( F ` p ) R ( F ` r ) )
57 56 orcd 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( F ` q ) R ( F ` r ) ) ) -> ( ( F ` p ) R ( F ` r ) \/ ( ( F ` p ) = ( F ` r ) /\ p [_ ( F ` p ) / x ]_ S r ) ) )
58 57 ex 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> ( ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( F ` q ) R ( F ` r ) ) -> ( ( F ` p ) R ( F ` r ) \/ ( ( F ` p ) = ( F ` r ) /\ p [_ ( F ` p ) / x ]_ S r ) ) ) )
59 simprl 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( F ` p ) R ( F ` q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> ( F ` p ) R ( F ` q ) )
60 simprrl 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( F ` p ) R ( F ` q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> ( F ` q ) = ( F ` r ) )
61 59 60 breqtrd 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( F ` p ) R ( F ` q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> ( F ` p ) R ( F ` r ) )
62 61 orcd 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( F ` p ) R ( F ` q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> ( ( F ` p ) R ( F ` r ) \/ ( ( F ` p ) = ( F ` r ) /\ p [_ ( F ` p ) / x ]_ S r ) ) )
63 62 ex 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> ( ( ( F ` p ) R ( F ` q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) -> ( ( F ` p ) R ( F ` r ) \/ ( ( F ` p ) = ( F ` r ) /\ p [_ ( F ` p ) / x ]_ S r ) ) ) )
64 simprll 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> ( F ` p ) = ( F ` q ) )
65 simprrl 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> ( F ` q ) = ( F ` r ) )
66 64 65 eqtrd 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> ( F ` p ) = ( F ` r ) )
67 simprlr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> p [_ ( F ` p ) / x ]_ S q )
68 simprrr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> q [_ ( F ` q ) / x ]_ S r )
69 64 csbeq1d 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> [_ ( F ` p ) / x ]_ S = [_ ( F ` q ) / x ]_ S )
70 69 breqd 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> ( q [_ ( F ` p ) / x ]_ S r <-> q [_ ( F ` q ) / x ]_ S r ) )
71 68 70 mpbird 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> q [_ ( F ` p ) / x ]_ S r )
72 26 adantr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> [_ ( F ` p ) / x ]_ S Po [_ ( F ` p ) / x ]_ B )
73 32 adantr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> p e. [_ ( F ` p ) / x ]_ B )
74 id 
 |-  ( t = q -> t = q )
75 fveq2 
 |-  ( t = q -> ( F ` t ) = ( F ` q ) )
76 75 csbeq1d 
 |-  ( t = q -> [_ ( F ` t ) / x ]_ B = [_ ( F ` q ) / x ]_ B )
77 74 76 eleq12d 
 |-  ( t = q -> ( t e. [_ ( F ` t ) / x ]_ B <-> q e. [_ ( F ` q ) / x ]_ B ) )
78 77 31 47 rspcdva 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> q e. [_ ( F ` q ) / x ]_ B )
79 78 adantr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> q e. [_ ( F ` q ) / x ]_ B )
80 64 csbeq1d 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> [_ ( F ` p ) / x ]_ B = [_ ( F ` q ) / x ]_ B )
81 79 80 eleqtrrd 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> q e. [_ ( F ` p ) / x ]_ B )
82 id 
 |-  ( t = r -> t = r )
83 fveq2 
 |-  ( t = r -> ( F ` t ) = ( F ` r ) )
84 83 csbeq1d 
 |-  ( t = r -> [_ ( F ` t ) / x ]_ B = [_ ( F ` r ) / x ]_ B )
85 82 84 eleq12d 
 |-  ( t = r -> ( t e. [_ ( F ` t ) / x ]_ B <-> r e. [_ ( F ` r ) / x ]_ B ) )
86 85 31 41 rspcdva 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> r e. [_ ( F ` r ) / x ]_ B )
87 86 adantr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> r e. [_ ( F ` r ) / x ]_ B )
88 66 csbeq1d 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> [_ ( F ` p ) / x ]_ B = [_ ( F ` r ) / x ]_ B )
89 87 88 eleqtrrd 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> r e. [_ ( F ` p ) / x ]_ B )
90 potr 
 |-  ( ( [_ ( F ` p ) / x ]_ S Po [_ ( F ` p ) / x ]_ B /\ ( p e. [_ ( F ` p ) / x ]_ B /\ q e. [_ ( F ` p ) / x ]_ B /\ r e. [_ ( F ` p ) / x ]_ B ) ) -> ( ( p [_ ( F ` p ) / x ]_ S q /\ q [_ ( F ` p ) / x ]_ S r ) -> p [_ ( F ` p ) / x ]_ S r ) )
91 72 73 81 89 90 syl13anc 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> ( ( p [_ ( F ` p ) / x ]_ S q /\ q [_ ( F ` p ) / x ]_ S r ) -> p [_ ( F ` p ) / x ]_ S r ) )
92 67 71 91 mp2and 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> p [_ ( F ` p ) / x ]_ S r )
93 66 92 jca 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> ( ( F ` p ) = ( F ` r ) /\ p [_ ( F ` p ) / x ]_ S r ) )
94 93 olcd 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) /\ ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> ( ( F ` p ) R ( F ` r ) \/ ( ( F ` p ) = ( F ` r ) /\ p [_ ( F ` p ) / x ]_ S r ) ) )
95 94 ex 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> ( ( ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) /\ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) -> ( ( F ` p ) R ( F ` r ) \/ ( ( F ` p ) = ( F ` r ) /\ p [_ ( F ` p ) / x ]_ S r ) ) ) )
96 53 58 63 95 ccased 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> ( ( ( ( F ` p ) R ( F ` q ) \/ ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) ) /\ ( ( F ` q ) R ( F ` r ) \/ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) ) -> ( ( F ` p ) R ( F ` r ) \/ ( ( F ` p ) = ( F ` r ) /\ p [_ ( F ` p ) / x ]_ S r ) ) ) )
97 44 46 96 syl2ani 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> ( ( p T q /\ q T r ) -> ( ( F ` p ) R ( F ` r ) \/ ( ( F ` p ) = ( F ` r ) /\ p [_ ( F ` p ) / x ]_ S r ) ) ) )
98 1 2 weiunlem1 
 |-  ( p T r <-> ( ( p e. U_ x e. A B /\ r e. U_ x e. A B ) /\ ( ( F ` p ) R ( F ` r ) \/ ( ( F ` p ) = ( F ` r ) /\ p [_ ( F ` p ) / x ]_ S r ) ) ) )
99 98 biimpri 
 |-  ( ( ( p e. U_ x e. A B /\ r e. U_ x e. A B ) /\ ( ( F ` p ) R ( F ` r ) \/ ( ( F ` p ) = ( F ` r ) /\ p [_ ( F ` p ) / x ]_ S r ) ) ) -> p T r )
100 42 97 99 syl6an 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> ( ( p T q /\ q T r ) -> p T r ) )
101 40 100 jca 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Po B ) /\ ( p e. U_ x e. A B /\ q e. U_ x e. A B /\ r e. U_ x e. A B ) ) -> ( -. p T p /\ ( ( p T q /\ q T r ) -> p T r ) ) )
102 101 ralrimivvva 
 |-  ( ( R We A /\ R Se A /\ A. x e. A S Po B ) -> A. p e. U_ x e. A B A. q e. U_ x e. A B A. r e. U_ x e. A B ( -. p T p /\ ( ( p T q /\ q T r ) -> p T r ) ) )
103 df-po 
 |-  ( T Po U_ x e. A B <-> A. p e. U_ x e. A B A. q e. U_ x e. A B A. r e. U_ x e. A B ( -. p T p /\ ( ( p T q /\ q T r ) -> p T r ) ) )
104 102 103 sylibr 
 |-  ( ( R We A /\ R Se A /\ A. x e. A S Po B ) -> T Po U_ x e. A B )