Metamath Proof Explorer

Theorem weiunfrlem2

Description: Lemma for weiunfr . (Contributed by Matthew House, 23-Aug-2025)

Ref Expression
Hypotheses weiunfrlem2.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 ) )
weiunfrlem2.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 ) ) ) }
weiunfrlem2.3 
|- C = ( iota_ s e. ( F " r ) A. t e. ( F " r ) -. t R s )
Assertion weiunfrlem2 
|- ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) -> T Fr U_ x e. A B )

Proof

Step Hyp Ref Expression
1 weiunfrlem2.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 weiunfrlem2.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 weiunfrlem2.3 
 |-  C = ( iota_ s e. ( F " r ) A. t e. ( F " r ) -. t R s )
4 vex 
 |-  r e. _V
5 4 inex1 
 |-  ( r i^i [_ C / x ]_ B ) e. _V
6 5 a1i 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( r i^i [_ C / x ]_ B ) e. _V )
7 1 weiunlem1 
 |-  ( ( R We A /\ R Se A ) -> ( F : U_ x e. A B --> A /\ A. w e. U_ x e. A B w e. [_ ( F ` w ) / x ]_ B /\ A. w e. U_ x e. A B A. v e. A ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) ) )
8 7 adantr 
 |-  ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( F : U_ x e. A B --> A /\ A. w e. U_ x e. A B w e. [_ ( F ` w ) / x ]_ B /\ A. w e. U_ x e. A B A. v e. A ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) ) )
9 8 3adantl3 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( F : U_ x e. A B --> A /\ A. w e. U_ x e. A B w e. [_ ( F ` w ) / x ]_ B /\ A. w e. U_ x e. A B A. v e. A ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) ) )
10 9 simp1d 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> F : U_ x e. A B --> A )
11 10 fimassd 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( F " r ) C_ A )
12 1 3 weiunfrlem1 
 |-  ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( C e. ( F " r ) /\ A. w e. r -. ( F ` w ) R C ) )
13 12 3adantl3 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( C e. ( F " r ) /\ A. w e. r -. ( F ` w ) R C ) )
14 13 simpld 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> C e. ( F " r ) )
15 11 14 sseldd 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> C e. A )
16 simpl3 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> A. x e. A S Fr B )
17 nfiu1 
 |-  F/_ x U_ x e. A B
18 nfrab1 
 |-  F/_ x { x e. A | w e. B }
19 nfv 
 |-  F/ x -. v R u
20 18 19 nfralw 
 |-  F/ x A. v e. { x e. A | w e. B } -. v R u
21 20 18 nfriota 
 |-  F/_ x ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u )
22 17 21 nfmpt 
 |-  F/_ x ( 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 ) )
23 1 22 nfcxfr 
 |-  F/_ x F
24 nfcv 
 |-  F/_ x r
25 23 24 nfima 
 |-  F/_ x ( F " r )
26 nfv 
 |-  F/ x -. t R s
27 25 26 nfralw 
 |-  F/ x A. t e. ( F " r ) -. t R s
28 27 25 nfriota 
 |-  F/_ x ( iota_ s e. ( F " r ) A. t e. ( F " r ) -. t R s )
29 3 28 nfcxfr 
 |-  F/_ x C
30 nfra1 
 |-  F/ x A. x e. A S Fr B
31 29 nfcsb1 
 |-  F/_ x [_ C / x ]_ S
32 29 nfcsb1 
 |-  F/_ x [_ C / x ]_ B
33 31 32 nffr 
 |-  F/ x [_ C / x ]_ S Fr [_ C / x ]_ B
34 30 33 nfim 
 |-  F/ x ( A. x e. A S Fr B -> [_ C / x ]_ S Fr [_ C / x ]_ B )
35 csbeq1a 
 |-  ( x = C -> S = [_ C / x ]_ S )
36 freq1 
 |-  ( S = [_ C / x ]_ S -> ( S Fr B <-> [_ C / x ]_ S Fr B ) )
37 35 36 syl 
 |-  ( x = C -> ( S Fr B <-> [_ C / x ]_ S Fr B ) )
38 csbeq1a 
 |-  ( x = C -> B = [_ C / x ]_ B )
39 freq2 
 |-  ( B = [_ C / x ]_ B -> ( [_ C / x ]_ S Fr B <-> [_ C / x ]_ S Fr [_ C / x ]_ B ) )
40 38 39 syl 
 |-  ( x = C -> ( [_ C / x ]_ S Fr B <-> [_ C / x ]_ S Fr [_ C / x ]_ B ) )
41 37 40 bitrd 
 |-  ( x = C -> ( S Fr B <-> [_ C / x ]_ S Fr [_ C / x ]_ B ) )
42 41 imbi2d 
 |-  ( x = C -> ( ( A. x e. A S Fr B -> S Fr B ) <-> ( A. x e. A S Fr B -> [_ C / x ]_ S Fr [_ C / x ]_ B ) ) )
43 rsp 
 |-  ( A. x e. A S Fr B -> ( x e. A -> S Fr B ) )
44 43 com12 
 |-  ( x e. A -> ( A. x e. A S Fr B -> S Fr B ) )
45 29 34 42 44 vtoclgaf 
 |-  ( C e. A -> ( A. x e. A S Fr B -> [_ C / x ]_ S Fr [_ C / x ]_ B ) )
46 15 16 45 sylc 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> [_ C / x ]_ S Fr [_ C / x ]_ B )
47 inss2 
 |-  ( r i^i [_ C / x ]_ B ) C_ [_ C / x ]_ B
48 47 a1i 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( r i^i [_ C / x ]_ B ) C_ [_ C / x ]_ B )
49 10 ffund 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> Fun F )
50 fvelima 
 |-  ( ( Fun F /\ C e. ( F " r ) ) -> E. o e. r ( F ` o ) = C )
51 49 14 50 syl2anc 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> E. o e. r ( F ` o ) = C )
52 simprl 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( o e. r /\ ( F ` o ) = C ) ) -> o e. r )
53 simplrl 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( o e. r /\ ( F ` o ) = C ) ) -> r C_ U_ x e. A B )
54 53 52 sseldd 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( o e. r /\ ( F ` o ) = C ) ) -> o e. U_ x e. A B )
55 9 simp2d 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> A. w e. U_ x e. A B w e. [_ ( F ` w ) / x ]_ B )
56 55 adantr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( o e. r /\ ( F ` o ) = C ) ) -> A. w e. U_ x e. A B w e. [_ ( F ` w ) / x ]_ B )
57 id 
 |-  ( w = o -> w = o )
58 fveq2 
 |-  ( w = o -> ( F ` w ) = ( F ` o ) )
59 58 csbeq1d 
 |-  ( w = o -> [_ ( F ` w ) / x ]_ B = [_ ( F ` o ) / x ]_ B )
60 57 59 eleq12d 
 |-  ( w = o -> ( w e. [_ ( F ` w ) / x ]_ B <-> o e. [_ ( F ` o ) / x ]_ B ) )
61 60 rspcv 
 |-  ( o e. U_ x e. A B -> ( A. w e. U_ x e. A B w e. [_ ( F ` w ) / x ]_ B -> o e. [_ ( F ` o ) / x ]_ B ) )
62 54 56 61 sylc 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( o e. r /\ ( F ` o ) = C ) ) -> o e. [_ ( F ` o ) / x ]_ B )
63 csbeq1 
 |-  ( ( F ` o ) = C -> [_ ( F ` o ) / x ]_ B = [_ C / x ]_ B )
64 63 ad2antll 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( o e. r /\ ( F ` o ) = C ) ) -> [_ ( F ` o ) / x ]_ B = [_ C / x ]_ B )
65 62 64 eleqtrd 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( o e. r /\ ( F ` o ) = C ) ) -> o e. [_ C / x ]_ B )
66 52 65 elind 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( o e. r /\ ( F ` o ) = C ) ) -> o e. ( r i^i [_ C / x ]_ B ) )
67 66 ne0d 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( o e. r /\ ( F ` o ) = C ) ) -> ( r i^i [_ C / x ]_ B ) =/= (/) )
68 51 67 rexlimddv 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( r i^i [_ C / x ]_ B ) =/= (/) )
69 fri 
 |-  ( ( ( ( r i^i [_ C / x ]_ B ) e. _V /\ [_ C / x ]_ S Fr [_ C / x ]_ B ) /\ ( ( r i^i [_ C / x ]_ B ) C_ [_ C / x ]_ B /\ ( r i^i [_ C / x ]_ B ) =/= (/) ) ) -> E. p e. ( r i^i [_ C / x ]_ B ) A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p )
70 6 46 48 68 69 syl22anc 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> E. p e. ( r i^i [_ C / x ]_ B ) A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p )
71 simprl 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> p e. ( r i^i [_ C / x ]_ B ) )
72 71 elin1d 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> p e. r )
73 13 adantr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> ( C e. ( F " r ) /\ A. w e. r -. ( F ` w ) R C ) )
74 73 simprd 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> A. w e. r -. ( F ` w ) R C )
75 fveq2 
 |-  ( w = t -> ( F ` w ) = ( F ` t ) )
76 75 breq1d 
 |-  ( w = t -> ( ( F ` w ) R C <-> ( F ` t ) R C ) )
77 76 notbid 
 |-  ( w = t -> ( -. ( F ` w ) R C <-> -. ( F ` t ) R C ) )
78 77 rspcv 
 |-  ( t e. r -> ( A. w e. r -. ( F ` w ) R C -> -. ( F ` t ) R C ) )
79 74 78 mpan9 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) -> -. ( F ` t ) R C )
80 fveq2 
 |-  ( w = p -> ( F ` w ) = ( F ` p ) )
81 80 breq1d 
 |-  ( w = p -> ( ( F ` w ) R C <-> ( F ` p ) R C ) )
82 81 notbid 
 |-  ( w = p -> ( -. ( F ` w ) R C <-> -. ( F ` p ) R C ) )
83 82 rspcv 
 |-  ( p e. r -> ( A. w e. r -. ( F ` w ) R C -> -. ( F ` p ) R C ) )
84 72 74 83 sylc 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> -. ( F ` p ) R C )
85 9 adantr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> ( F : U_ x e. A B --> A /\ A. w e. U_ x e. A B w e. [_ ( F ` w ) / x ]_ B /\ A. w e. U_ x e. A B A. v e. A ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) ) )
86 85 simp3d 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> A. w e. U_ x e. A B A. v e. A ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) )
87 71 elin2d 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> p e. [_ C / x ]_ B )
88 simplrl 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> r C_ U_ x e. A B )
89 88 72 sseldd 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> p e. U_ x e. A B )
90 15 adantr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> C e. A )
91 simpl 
 |-  ( ( w = p /\ v = C ) -> w = p )
92 simpr 
 |-  ( ( w = p /\ v = C ) -> v = C )
93 92 csbeq1d 
 |-  ( ( w = p /\ v = C ) -> [_ v / x ]_ B = [_ C / x ]_ B )
94 91 93 eleq12d 
 |-  ( ( w = p /\ v = C ) -> ( w e. [_ v / x ]_ B <-> p e. [_ C / x ]_ B ) )
95 91 fveq2d 
 |-  ( ( w = p /\ v = C ) -> ( F ` w ) = ( F ` p ) )
96 92 95 breq12d 
 |-  ( ( w = p /\ v = C ) -> ( v R ( F ` w ) <-> C R ( F ` p ) ) )
97 96 notbid 
 |-  ( ( w = p /\ v = C ) -> ( -. v R ( F ` w ) <-> -. C R ( F ` p ) ) )
98 94 97 imbi12d 
 |-  ( ( w = p /\ v = C ) -> ( ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) <-> ( p e. [_ C / x ]_ B -> -. C R ( F ` p ) ) ) )
99 98 rspc2gv 
 |-  ( ( p e. U_ x e. A B /\ C e. A ) -> ( A. w e. U_ x e. A B A. v e. A ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) -> ( p e. [_ C / x ]_ B -> -. C R ( F ` p ) ) ) )
100 89 90 99 syl2anc 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> ( A. w e. U_ x e. A B A. v e. A ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) -> ( p e. [_ C / x ]_ B -> -. C R ( F ` p ) ) ) )
101 86 87 100 mp2d 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> -. C R ( F ` p ) )
102 simpll1 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> R We A )
103 weso 
 |-  ( R We A -> R Or A )
104 102 103 syl 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> R Or A )
105 10 adantr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> F : U_ x e. A B --> A )
106 105 89 ffvelcdmd 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> ( F ` p ) e. A )
107 sotrieq2 
 |-  ( ( R Or A /\ ( ( F ` p ) e. A /\ C e. A ) ) -> ( ( F ` p ) = C <-> ( -. ( F ` p ) R C /\ -. C R ( F ` p ) ) ) )
108 104 106 90 107 syl12anc 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> ( ( F ` p ) = C <-> ( -. ( F ` p ) R C /\ -. C R ( F ` p ) ) ) )
109 84 101 108 mpbir2and 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> ( F ` p ) = C )
110 109 adantr 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) -> ( F ` p ) = C )
111 breq2 
 |-  ( ( F ` p ) = C -> ( ( F ` t ) R ( F ` p ) <-> ( F ` t ) R C ) )
112 111 notbid 
 |-  ( ( F ` p ) = C -> ( -. ( F ` t ) R ( F ` p ) <-> -. ( F ` t ) R C ) )
113 110 112 syl 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) -> ( -. ( F ` t ) R ( F ` p ) <-> -. ( F ` t ) R C ) )
114 79 113 mpbird 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) -> -. ( F ` t ) R ( F ` p ) )
115 simplr 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) /\ ( F ` t ) = ( F ` p ) ) -> t e. r )
116 88 sselda 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) -> t e. U_ x e. A B )
117 55 ad2antrr 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) -> A. w e. U_ x e. A B w e. [_ ( F ` w ) / x ]_ B )
118 id 
 |-  ( w = t -> w = t )
119 75 csbeq1d 
 |-  ( w = t -> [_ ( F ` w ) / x ]_ B = [_ ( F ` t ) / x ]_ B )
120 118 119 eleq12d 
 |-  ( w = t -> ( w e. [_ ( F ` w ) / x ]_ B <-> t e. [_ ( F ` t ) / x ]_ B ) )
121 120 rspcv 
 |-  ( t e. U_ x e. A B -> ( A. w e. U_ x e. A B w e. [_ ( F ` w ) / x ]_ B -> t e. [_ ( F ` t ) / x ]_ B ) )
122 116 117 121 sylc 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) -> t e. [_ ( F ` t ) / x ]_ B )
123 122 adantr 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) /\ ( F ` t ) = ( F ` p ) ) -> t e. [_ ( F ` t ) / x ]_ B )
124 simpr 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) /\ ( F ` t ) = ( F ` p ) ) -> ( F ` t ) = ( F ` p ) )
125 110 adantr 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) /\ ( F ` t ) = ( F ` p ) ) -> ( F ` p ) = C )
126 124 125 eqtrd 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) /\ ( F ` t ) = ( F ` p ) ) -> ( F ` t ) = C )
127 126 csbeq1d 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) /\ ( F ` t ) = ( F ` p ) ) -> [_ ( F ` t ) / x ]_ B = [_ C / x ]_ B )
128 123 127 eleqtrd 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) /\ ( F ` t ) = ( F ` p ) ) -> t e. [_ C / x ]_ B )
129 115 128 elind 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) /\ ( F ` t ) = ( F ` p ) ) -> t e. ( r i^i [_ C / x ]_ B ) )
130 simprr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p )
131 130 ad2antrr 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) /\ ( F ` t ) = ( F ` p ) ) -> A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p )
132 breq1 
 |-  ( q = t -> ( q [_ C / x ]_ S p <-> t [_ C / x ]_ S p ) )
133 132 notbid 
 |-  ( q = t -> ( -. q [_ C / x ]_ S p <-> -. t [_ C / x ]_ S p ) )
134 133 rspcv 
 |-  ( t e. ( r i^i [_ C / x ]_ B ) -> ( A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p -> -. t [_ C / x ]_ S p ) )
135 129 131 134 sylc 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) /\ ( F ` t ) = ( F ` p ) ) -> -. t [_ C / x ]_ S p )
136 126 csbeq1d 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) /\ ( F ` t ) = ( F ` p ) ) -> [_ ( F ` t ) / x ]_ S = [_ C / x ]_ S )
137 136 breqd 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) /\ ( F ` t ) = ( F ` p ) ) -> ( t [_ ( F ` t ) / x ]_ S p <-> t [_ C / x ]_ S p ) )
138 135 137 mtbird 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) /\ ( F ` t ) = ( F ` p ) ) -> -. t [_ ( F ` t ) / x ]_ S p )
139 138 ex 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) -> ( ( F ` t ) = ( F ` p ) -> -. t [_ ( F ` t ) / x ]_ S p ) )
140 imnan 
 |-  ( ( ( F ` t ) = ( F ` p ) -> -. t [_ ( F ` t ) / x ]_ S p ) <-> -. ( ( F ` t ) = ( F ` p ) /\ t [_ ( F ` t ) / x ]_ S p ) )
141 139 140 sylib 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) -> -. ( ( F ` t ) = ( F ` p ) /\ t [_ ( F ` t ) / x ]_ S p ) )
142 pm4.56 
 |-  ( ( -. ( F ` t ) R ( F ` p ) /\ -. ( ( F ` t ) = ( F ` p ) /\ t [_ ( F ` t ) / x ]_ S p ) ) <-> -. ( ( F ` t ) R ( F ` p ) \/ ( ( F ` t ) = ( F ` p ) /\ t [_ ( F ` t ) / x ]_ S p ) ) )
143 142 biimpi 
 |-  ( ( -. ( F ` t ) R ( F ` p ) /\ -. ( ( F ` t ) = ( F ` p ) /\ t [_ ( F ` t ) / x ]_ S p ) ) -> -. ( ( F ` t ) R ( F ` p ) \/ ( ( F ` t ) = ( F ` p ) /\ t [_ ( F ` t ) / x ]_ S p ) ) )
144 114 141 143 syl2anc 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) -> -. ( ( F ` t ) R ( F ` p ) \/ ( ( F ` t ) = ( F ` p ) /\ t [_ ( F ` t ) / x ]_ S p ) ) )
145 144 intnand 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) -> -. ( ( t e. U_ x e. A B /\ p e. U_ x e. A B ) /\ ( ( F ` t ) R ( F ` p ) \/ ( ( F ` t ) = ( F ` p ) /\ t [_ ( F ` t ) / x ]_ S p ) ) ) )
146 simpl 
 |-  ( ( y = t /\ z = p ) -> y = t )
147 146 fveq2d 
 |-  ( ( y = t /\ z = p ) -> ( F ` y ) = ( F ` t ) )
148 simpr 
 |-  ( ( y = t /\ z = p ) -> z = p )
149 148 fveq2d 
 |-  ( ( y = t /\ z = p ) -> ( F ` z ) = ( F ` p ) )
150 147 149 breq12d 
 |-  ( ( y = t /\ z = p ) -> ( ( F ` y ) R ( F ` z ) <-> ( F ` t ) R ( F ` p ) ) )
151 147 149 eqeq12d 
 |-  ( ( y = t /\ z = p ) -> ( ( F ` y ) = ( F ` z ) <-> ( F ` t ) = ( F ` p ) ) )
152 147 csbeq1d 
 |-  ( ( y = t /\ z = p ) -> [_ ( F ` y ) / x ]_ S = [_ ( F ` t ) / x ]_ S )
153 146 152 148 breq123d 
 |-  ( ( y = t /\ z = p ) -> ( y [_ ( F ` y ) / x ]_ S z <-> t [_ ( F ` t ) / x ]_ S p ) )
154 151 153 anbi12d 
 |-  ( ( y = t /\ z = p ) -> ( ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) <-> ( ( F ` t ) = ( F ` p ) /\ t [_ ( F ` t ) / x ]_ S p ) ) )
155 150 154 orbi12d 
 |-  ( ( y = t /\ z = p ) -> ( ( ( F ` y ) R ( F ` z ) \/ ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) <-> ( ( F ` t ) R ( F ` p ) \/ ( ( F ` t ) = ( F ` p ) /\ t [_ ( F ` t ) / x ]_ S p ) ) ) )
156 155 2 brab2a 
 |-  ( t T p <-> ( ( t e. U_ x e. A B /\ p e. U_ x e. A B ) /\ ( ( F ` t ) R ( F ` p ) \/ ( ( F ` t ) = ( F ` p ) /\ t [_ ( F ` t ) / x ]_ S p ) ) ) )
157 145 156 sylnibr 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) /\ t e. r ) -> -. t T p )
158 157 ralrimiva 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( p e. ( r i^i [_ C / x ]_ B ) /\ A. q e. ( r i^i [_ C / x ]_ B ) -. q [_ C / x ]_ S p ) ) -> A. t e. r -. t T p )
159 70 72 158 reximssdv 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> E. p e. r A. t e. r -. t T p )
160 159 ex 
 |-  ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) -> ( ( r C_ U_ x e. A B /\ r =/= (/) ) -> E. p e. r A. t e. r -. t T p ) )
161 160 alrimiv 
 |-  ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) -> A. r ( ( r C_ U_ x e. A B /\ r =/= (/) ) -> E. p e. r A. t e. r -. t T p ) )
162 df-fr 
 |-  ( T Fr U_ x e. A B <-> A. r ( ( r C_ U_ x e. A B /\ r =/= (/) ) -> E. p e. r A. t e. r -. t T p ) )
163 161 162 sylibr 
 |-  ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) -> T Fr U_ x e. A B )