Metamath Proof Explorer

Theorem weiunpo

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

Ref Expression
Hypotheses weiunpo.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 ) )
weiunpo.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 weiunpo.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 weiunpo.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 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 ) ) ) )
8 3 6 7 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 : 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 ) ) ) )
9 8 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 )
10 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 )
11 9 10 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 )
12 sonr 
 |-  ( ( R Or A /\ ( F ` p ) e. A ) -> -. ( F ` p ) R ( F ` p ) )
13 5 11 12 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 ) )
14 csbeq1 
 |-  ( s = ( F ` p ) -> [_ s / x ]_ S = [_ ( F ` p ) / x ]_ S )
15 poeq1 
 |-  ( [_ s / x ]_ S = [_ ( F ` p ) / x ]_ S -> ( [_ s / x ]_ S Po [_ s / x ]_ B <-> [_ ( F ` p ) / x ]_ S Po [_ s / x ]_ B ) )
16 14 15 syl 
 |-  ( s = ( F ` p ) -> ( [_ s / x ]_ S Po [_ s / x ]_ B <-> [_ ( F ` p ) / x ]_ S Po [_ s / x ]_ B ) )
17 csbeq1 
 |-  ( s = ( F ` p ) -> [_ s / x ]_ B = [_ ( F ` p ) / x ]_ B )
18 poeq2 
 |-  ( [_ s / x ]_ B = [_ ( F ` p ) / x ]_ B -> ( [_ ( F ` p ) / x ]_ S Po [_ s / x ]_ B <-> [_ ( F ` p ) / x ]_ S Po [_ ( F ` p ) / x ]_ B ) )
19 17 18 syl 
 |-  ( s = ( F ` p ) -> ( [_ ( F ` p ) / x ]_ S Po [_ s / x ]_ B <-> [_ ( F ` p ) / x ]_ S Po [_ ( F ` p ) / x ]_ B ) )
20 16 19 bitrd 
 |-  ( s = ( F ` p ) -> ( [_ s / x ]_ S Po [_ s / x ]_ B <-> [_ ( F ` p ) / x ]_ S Po [_ ( F ` p ) / x ]_ B ) )
21 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 )
22 nfv 
 |-  F/ s S Po B
23 nfcsb1v 
 |-  F/_ x [_ s / x ]_ S
24 nfcsb1v 
 |-  F/_ x [_ s / x ]_ B
25 23 24 nfpo 
 |-  F/ x [_ s / x ]_ S Po [_ s / x ]_ B
26 csbeq1a 
 |-  ( x = s -> S = [_ s / x ]_ S )
27 poeq1 
 |-  ( S = [_ s / x ]_ S -> ( S Po B <-> [_ s / x ]_ S Po B ) )
28 26 27 syl 
 |-  ( x = s -> ( S Po B <-> [_ s / x ]_ S Po B ) )
29 csbeq1a 
 |-  ( x = s -> B = [_ s / x ]_ B )
30 poeq2 
 |-  ( B = [_ s / x ]_ B -> ( [_ s / x ]_ S Po B <-> [_ s / x ]_ S Po [_ s / x ]_ B ) )
31 29 30 syl 
 |-  ( x = s -> ( [_ s / x ]_ S Po B <-> [_ s / x ]_ S Po [_ s / x ]_ B ) )
32 28 31 bitrd 
 |-  ( x = s -> ( S Po B <-> [_ s / x ]_ S Po [_ s / x ]_ B ) )
33 22 25 32 cbvralw 
 |-  ( A. x e. A S Po B <-> A. s e. A [_ s / x ]_ S Po [_ s / x ]_ B )
34 21 33 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 )
35 20 34 11 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 )
36 id 
 |-  ( t = p -> t = p )
37 fveq2 
 |-  ( t = p -> ( F ` t ) = ( F ` p ) )
38 37 csbeq1d 
 |-  ( t = p -> [_ ( F ` t ) / x ]_ B = [_ ( F ` p ) / x ]_ B )
39 36 38 eleq12d 
 |-  ( t = p -> ( t e. [_ ( F ` t ) / x ]_ B <-> p e. [_ ( F ` p ) / x ]_ B ) )
40 8 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 )
41 39 40 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 ) ) -> p e. [_ ( F ` p ) / x ]_ B )
42 poirr 
 |-  ( ( [_ ( F ` p ) / x ]_ S Po [_ ( F ` p ) / x ]_ B /\ p e. [_ ( F ` p ) / x ]_ B ) -> -. p [_ ( F ` p ) / x ]_ S p )
43 35 41 42 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 )
44 43 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 ) )
45 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 ) ) )
46 13 44 45 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 ) ) )
47 simpl 
 |-  ( ( y = p /\ z = p ) -> y = p )
48 47 fveq2d 
 |-  ( ( y = p /\ z = p ) -> ( F ` y ) = ( F ` p ) )
49 simpr 
 |-  ( ( y = p /\ z = p ) -> z = p )
50 49 fveq2d 
 |-  ( ( y = p /\ z = p ) -> ( F ` z ) = ( F ` p ) )
51 48 50 breq12d 
 |-  ( ( y = p /\ z = p ) -> ( ( F ` y ) R ( F ` z ) <-> ( F ` p ) R ( F ` p ) ) )
52 48 50 eqeq12d 
 |-  ( ( y = p /\ z = p ) -> ( ( F ` y ) = ( F ` z ) <-> ( F ` p ) = ( F ` p ) ) )
53 48 csbeq1d 
 |-  ( ( y = p /\ z = p ) -> [_ ( F ` y ) / x ]_ S = [_ ( F ` p ) / x ]_ S )
54 47 53 49 breq123d 
 |-  ( ( y = p /\ z = p ) -> ( y [_ ( F ` y ) / x ]_ S z <-> p [_ ( F ` p ) / x ]_ S p ) )
55 52 54 anbi12d 
 |-  ( ( y = p /\ z = p ) -> ( ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) <-> ( ( F ` p ) = ( F ` p ) /\ p [_ ( F ` p ) / x ]_ S p ) ) )
56 51 55 orbi12d 
 |-  ( ( y = p /\ z = p ) -> ( ( ( F ` y ) R ( F ` z ) \/ ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) <-> ( ( F ` p ) R ( F ` p ) \/ ( ( F ` p ) = ( F ` p ) /\ p [_ ( F ` p ) / x ]_ S p ) ) ) )
57 56 2 brab2a 
 |-  ( 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 ) ) ) )
58 57 simprbi 
 |-  ( p T p -> ( ( F ` p ) R ( F ` p ) \/ ( ( F ` p ) = ( F ` p ) /\ p [_ ( F ` p ) / x ]_ S p ) ) )
59 46 58 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 )
60 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 )
61 10 60 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 ) )
62 simpl 
 |-  ( ( y = p /\ z = q ) -> y = p )
63 62 fveq2d 
 |-  ( ( y = p /\ z = q ) -> ( F ` y ) = ( F ` p ) )
64 simpr 
 |-  ( ( y = p /\ z = q ) -> z = q )
65 64 fveq2d 
 |-  ( ( y = p /\ z = q ) -> ( F ` z ) = ( F ` q ) )
66 63 65 breq12d 
 |-  ( ( y = p /\ z = q ) -> ( ( F ` y ) R ( F ` z ) <-> ( F ` p ) R ( F ` q ) ) )
67 63 65 eqeq12d 
 |-  ( ( y = p /\ z = q ) -> ( ( F ` y ) = ( F ` z ) <-> ( F ` p ) = ( F ` q ) ) )
68 63 csbeq1d 
 |-  ( ( y = p /\ z = q ) -> [_ ( F ` y ) / x ]_ S = [_ ( F ` p ) / x ]_ S )
69 62 68 64 breq123d 
 |-  ( ( y = p /\ z = q ) -> ( y [_ ( F ` y ) / x ]_ S z <-> p [_ ( F ` p ) / x ]_ S q ) )
70 67 69 anbi12d 
 |-  ( ( y = p /\ z = q ) -> ( ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) <-> ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) ) )
71 66 70 orbi12d 
 |-  ( ( y = p /\ z = q ) -> ( ( ( F ` y ) R ( F ` z ) \/ ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) <-> ( ( F ` p ) R ( F ` q ) \/ ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) ) ) )
72 71 2 brab2a 
 |-  ( 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 ) ) ) )
73 72 simprbi 
 |-  ( p T q -> ( ( F ` p ) R ( F ` q ) \/ ( ( F ` p ) = ( F ` q ) /\ p [_ ( F ` p ) / x ]_ S q ) ) )
74 simpl 
 |-  ( ( y = q /\ z = r ) -> y = q )
75 74 fveq2d 
 |-  ( ( y = q /\ z = r ) -> ( F ` y ) = ( F ` q ) )
76 simpr 
 |-  ( ( y = q /\ z = r ) -> z = r )
77 76 fveq2d 
 |-  ( ( y = q /\ z = r ) -> ( F ` z ) = ( F ` r ) )
78 75 77 breq12d 
 |-  ( ( y = q /\ z = r ) -> ( ( F ` y ) R ( F ` z ) <-> ( F ` q ) R ( F ` r ) ) )
79 75 77 eqeq12d 
 |-  ( ( y = q /\ z = r ) -> ( ( F ` y ) = ( F ` z ) <-> ( F ` q ) = ( F ` r ) ) )
80 75 csbeq1d 
 |-  ( ( y = q /\ z = r ) -> [_ ( F ` y ) / x ]_ S = [_ ( F ` q ) / x ]_ S )
81 74 80 76 breq123d 
 |-  ( ( y = q /\ z = r ) -> ( y [_ ( F ` y ) / x ]_ S z <-> q [_ ( F ` q ) / x ]_ S r ) )
82 79 81 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 ) ) )
83 78 82 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 ) ) ) )
84 83 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 ) ) ) )
85 84 simprbi 
 |-  ( q T r -> ( ( F ` q ) R ( F ` r ) \/ ( ( F ` q ) = ( F ` r ) /\ q [_ ( F ` q ) / x ]_ S r ) ) )
86 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 )
87 9 86 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 )
88 9 60 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 )
89 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 ) ) )
90 5 11 87 88 89 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 ) ) )
91 90 imp 
 |-  ( ( ( ( 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 ) )
92 91 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 ) R ( F ` r ) ) ) -> ( ( F ` p ) R ( F ` r ) \/ ( ( F ` p ) = ( F ` r ) /\ p [_ ( F ` p ) / x ]_ S r ) ) )
93 92 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 ) R ( F ` r ) ) -> ( ( F ` p ) R ( F ` r ) \/ ( ( F ` p ) = ( F ` r ) /\ p [_ ( F ` p ) / x ]_ S r ) ) ) )
94 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 ) )
95 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 ) )
96 94 95 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 ) )
97 96 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 ) ) )
98 97 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 ) ) ) )
99 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 ) )
100 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 ) )
101 99 100 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 ) )
102 101 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 ) ) )
103 102 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 ) ) ) )
104 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 ) )
105 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 ) )
106 104 105 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 ) )
107 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 )
108 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 )
109 104 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 )
110 109 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 ) )
111 108 110 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 )
112 35 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 )
113 41 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 )
114 id 
 |-  ( t = q -> t = q )
115 fveq2 
 |-  ( t = q -> ( F ` t ) = ( F ` q ) )
116 115 csbeq1d 
 |-  ( t = q -> [_ ( F ` t ) / x ]_ B = [_ ( F ` q ) / x ]_ B )
117 114 116 eleq12d 
 |-  ( t = q -> ( t e. [_ ( F ` t ) / x ]_ B <-> q e. [_ ( F ` q ) / x ]_ B ) )
118 117 40 86 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 )
119 118 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 )
120 104 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 )
121 119 120 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 )
122 id 
 |-  ( t = r -> t = r )
123 fveq2 
 |-  ( t = r -> ( F ` t ) = ( F ` r ) )
124 123 csbeq1d 
 |-  ( t = r -> [_ ( F ` t ) / x ]_ B = [_ ( F ` r ) / x ]_ B )
125 122 124 eleq12d 
 |-  ( t = r -> ( t e. [_ ( F ` t ) / x ]_ B <-> r e. [_ ( F ` r ) / x ]_ B ) )
126 125 40 60 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 )
127 126 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 )
128 106 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 )
129 127 128 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 )
130 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 ) )
131 112 113 121 129 130 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 ) )
132 107 111 131 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 )
133 106 132 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 ) )
134 133 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 ) ) )
135 134 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 ) ) ) )
136 93 98 103 135 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 ) ) ) )
137 73 85 136 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 ) ) ) )
138 simpl 
 |-  ( ( y = p /\ z = r ) -> y = p )
139 138 fveq2d 
 |-  ( ( y = p /\ z = r ) -> ( F ` y ) = ( F ` p ) )
140 simpr 
 |-  ( ( y = p /\ z = r ) -> z = r )
141 140 fveq2d 
 |-  ( ( y = p /\ z = r ) -> ( F ` z ) = ( F ` r ) )
142 139 141 breq12d 
 |-  ( ( y = p /\ z = r ) -> ( ( F ` y ) R ( F ` z ) <-> ( F ` p ) R ( F ` r ) ) )
143 139 141 eqeq12d 
 |-  ( ( y = p /\ z = r ) -> ( ( F ` y ) = ( F ` z ) <-> ( F ` p ) = ( F ` r ) ) )
144 139 csbeq1d 
 |-  ( ( y = p /\ z = r ) -> [_ ( F ` y ) / x ]_ S = [_ ( F ` p ) / x ]_ S )
145 138 144 140 breq123d 
 |-  ( ( y = p /\ z = r ) -> ( y [_ ( F ` y ) / x ]_ S z <-> p [_ ( F ` p ) / x ]_ S r ) )
146 143 145 anbi12d 
 |-  ( ( y = p /\ z = r ) -> ( ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) <-> ( ( F ` p ) = ( F ` r ) /\ p [_ ( F ` p ) / x ]_ S r ) ) )
147 142 146 orbi12d 
 |-  ( ( y = p /\ z = r ) -> ( ( ( F ` y ) R ( F ` z ) \/ ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) <-> ( ( F ` p ) R ( F ` r ) \/ ( ( F ` p ) = ( F ` r ) /\ p [_ ( F ` p ) / x ]_ S r ) ) ) )
148 147 2 brab2a 
 |-  ( 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 ) ) ) )
149 148 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 )
150 61 137 149 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 ) )
151 59 150 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 ) ) )
152 151 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 ) ) )
153 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 ) ) )
154 152 153 sylibr 
 |-  ( ( R We A /\ R Se A /\ A. x e. A S Po B ) -> T Po U_ x e. A B )