Metamath Proof Explorer

Theorem weiunfr

Description: A well-founded relation on an indexed union can be constructed from a well-ordering on its index class and a collection of well-founded relations 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 weiunfr 
|- ( ( 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 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 csbeq1 
 |-  ( s = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) -> [_ s / x ]_ S = [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S )
4 csbeq1 
 |-  ( s = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) -> [_ s / x ]_ B = [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B )
5 3 4 freq12d 
 |-  ( s = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) -> ( [_ s / x ]_ S Fr [_ s / x ]_ B <-> [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S Fr [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) )
6 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 )
7 nfv 
 |-  F/ s S Fr B
8 nfcsb1v 
 |-  F/_ x [_ s / x ]_ S
9 nfcsb1v 
 |-  F/_ x [_ s / x ]_ B
10 8 9 nffr 
 |-  F/ x [_ s / x ]_ S Fr [_ s / x ]_ B
11 csbeq1a 
 |-  ( x = s -> S = [_ s / x ]_ S )
12 csbeq1a 
 |-  ( x = s -> B = [_ s / x ]_ B )
13 11 12 freq12d 
 |-  ( x = s -> ( S Fr B <-> [_ s / x ]_ S Fr [_ s / x ]_ B ) )
14 7 10 13 cbvralw 
 |-  ( A. x e. A S Fr B <-> A. s e. A [_ s / x ]_ S Fr [_ s / x ]_ B )
15 6 14 sylib 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> A. s e. A [_ s / x ]_ S Fr [_ s / x ]_ B )
16 simpl1 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> R We A )
17 simpl2 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> R Se A )
18 1 2 16 17 weiunlem2 
 |-  ( ( ( 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. 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 ) ) )
19 18 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 )
20 19 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 )
21 eqid 
 |-  ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p )
22 simprl 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> r C_ U_ x e. A B )
23 simprr 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> r =/= (/) )
24 1 2 16 17 21 22 23 weiunfrlem 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) e. ( F " r ) /\ A. t e. r -. ( F ` t ) R ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) /\ A. t e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) )
25 24 simp1d 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) e. ( F " r ) )
26 20 25 sseldd 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) e. A )
27 5 15 26 rspcdva 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S Fr [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B )
28 inss2 
 |-  ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) C_ [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B
29 28 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 [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) C_ [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B )
30 vex 
 |-  r e. _V
31 30 inex1 
 |-  ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) e. _V
32 31 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 [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) e. _V )
33 19 ffund 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> Fun F )
34 fvelima 
 |-  ( ( Fun F /\ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) e. ( F " r ) ) -> E. t e. r ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) )
35 33 25 34 syl2anc 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> E. t e. r ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) )
36 simprl 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( t e. r /\ ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) -> t e. r )
37 simplrl 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( t e. r /\ ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) -> r C_ U_ x e. A B )
38 37 36 sseldd 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( t e. r /\ ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) -> t e. U_ x e. A B )
39 18 simp2d 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> A. t e. U_ x e. A B t e. [_ ( F ` t ) / x ]_ B )
40 39 r19.21bi 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ t e. U_ x e. A B ) -> t e. [_ ( F ` t ) / x ]_ B )
41 38 40 syldan 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( t e. r /\ ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) -> t e. [_ ( F ` t ) / x ]_ B )
42 simprr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( t e. r /\ ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) -> ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) )
43 42 csbeq1d 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( t e. r /\ ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) -> [_ ( F ` t ) / x ]_ B = [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B )
44 41 43 eleqtrd 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( t e. r /\ ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) -> t e. [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B )
45 36 44 elind 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( t e. r /\ ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) -> t e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) )
46 45 ne0d 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( t e. r /\ ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) ) -> ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) =/= (/) )
47 35 46 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 [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) =/= (/) )
48 27 29 32 47 frd 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> E. n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n )
49 simprl 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) -> n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) )
50 49 elin1d 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) -> n e. r )
51 fveq2 
 |-  ( t = o -> ( F ` t ) = ( F ` o ) )
52 51 breq1d 
 |-  ( t = o -> ( ( F ` t ) R ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) <-> ( F ` o ) R ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) )
53 52 notbid 
 |-  ( t = o -> ( -. ( F ` t ) R ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) <-> -. ( F ` o ) R ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) )
54 24 ad2antrr 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> ( ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) e. ( F " r ) /\ A. t e. r -. ( F ` t ) R ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) /\ A. t e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) )
55 54 simp2d 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> A. t e. r -. ( F ` t ) R ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) )
56 simpr 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> o e. r )
57 53 55 56 rspcdva 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> -. ( F ` o ) R ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) )
58 fveqeq2 
 |-  ( t = n -> ( ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) <-> ( F ` n ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) )
59 54 simp3d 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> A. t e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) ( F ` t ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) )
60 simplrl 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) )
61 58 59 60 rspcdva 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> ( F ` n ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) )
62 61 breq2d 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> ( ( F ` o ) R ( F ` n ) <-> ( F ` o ) R ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) ) )
63 57 62 mtbird 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> -. ( F ` o ) R ( F ` n ) )
64 breq1 
 |-  ( m = o -> ( m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n <-> o [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) )
65 64 notbid 
 |-  ( m = o -> ( -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n <-> -. o [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) )
66 simprr 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) -> A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n )
67 66 ad2antrr 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n )
68 simplr 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> o e. r )
69 id 
 |-  ( t = o -> t = o )
70 51 csbeq1d 
 |-  ( t = o -> [_ ( F ` t ) / x ]_ B = [_ ( F ` o ) / x ]_ B )
71 69 70 eleq12d 
 |-  ( t = o -> ( t e. [_ ( F ` t ) / x ]_ B <-> o e. [_ ( F ` o ) / x ]_ B ) )
72 39 ad3antrrr 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> A. t e. U_ x e. A B t e. [_ ( F ` t ) / x ]_ B )
73 22 ad2antrr 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> r C_ U_ x e. A B )
74 73 56 sseldd 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> o e. U_ x e. A B )
75 74 adantr 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> o e. U_ x e. A B )
76 71 72 75 rspcdva 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> o e. [_ ( F ` o ) / x ]_ B )
77 simpr 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> ( F ` o ) = ( F ` n ) )
78 61 adantr 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> ( F ` n ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) )
79 77 78 eqtrd 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> ( F ` o ) = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) )
80 79 csbeq1d 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> [_ ( F ` o ) / x ]_ B = [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B )
81 76 80 eleqtrd 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> o e. [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B )
82 68 81 elind 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> o e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) )
83 65 67 82 rspcdva 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> -. o [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n )
84 79 csbeq1d 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> [_ ( F ` o ) / x ]_ S = [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S )
85 84 breqd 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> ( o [_ ( F ` o ) / x ]_ S n <-> o [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) )
86 83 85 mtbird 
 |-  ( ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) /\ ( F ` o ) = ( F ` n ) ) -> -. o [_ ( F ` o ) / x ]_ S n )
87 86 ex 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> ( ( F ` o ) = ( F ` n ) -> -. o [_ ( F ` o ) / x ]_ S n ) )
88 imnan 
 |-  ( ( ( F ` o ) = ( F ` n ) -> -. o [_ ( F ` o ) / x ]_ S n ) <-> -. ( ( F ` o ) = ( F ` n ) /\ o [_ ( F ` o ) / x ]_ S n ) )
89 87 88 sylib 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> -. ( ( F ` o ) = ( F ` n ) /\ o [_ ( F ` o ) / x ]_ S n ) )
90 pm4.56 
 |-  ( ( -. ( F ` o ) R ( F ` n ) /\ -. ( ( F ` o ) = ( F ` n ) /\ o [_ ( F ` o ) / x ]_ S n ) ) <-> -. ( ( F ` o ) R ( F ` n ) \/ ( ( F ` o ) = ( F ` n ) /\ o [_ ( F ` o ) / x ]_ S n ) ) )
91 90 biimpi 
 |-  ( ( -. ( F ` o ) R ( F ` n ) /\ -. ( ( F ` o ) = ( F ` n ) /\ o [_ ( F ` o ) / x ]_ S n ) ) -> -. ( ( F ` o ) R ( F ` n ) \/ ( ( F ` o ) = ( F ` n ) /\ o [_ ( F ` o ) / x ]_ S n ) ) )
92 63 89 91 syl2anc 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> -. ( ( F ` o ) R ( F ` n ) \/ ( ( F ` o ) = ( F ` n ) /\ o [_ ( F ` o ) / x ]_ S n ) ) )
93 92 intnand 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> -. ( ( o e. U_ x e. A B /\ n e. U_ x e. A B ) /\ ( ( F ` o ) R ( F ` n ) \/ ( ( F ` o ) = ( F ` n ) /\ o [_ ( F ` o ) / x ]_ S n ) ) ) )
94 1 2 weiunlem1 
 |-  ( o T n <-> ( ( o e. U_ x e. A B /\ n e. U_ x e. A B ) /\ ( ( F ` o ) R ( F ` n ) \/ ( ( F ` o ) = ( F ` n ) /\ o [_ ( F ` o ) / x ]_ S n ) ) ) )
95 93 94 sylnibr 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) /\ o e. r ) -> -. o T n )
96 95 ralrimiva 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) /\ ( n e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) /\ A. m e. ( r i^i [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ B ) -. m [_ ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) / x ]_ S n ) ) -> A. o e. r -. o T n )
97 48 50 96 reximssdv 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> E. n e. r A. o e. r -. o T n )
98 97 ex 
 |-  ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) -> ( ( r C_ U_ x e. A B /\ r =/= (/) ) -> E. n e. r A. o e. r -. o T n ) )
99 98 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. n e. r A. o e. r -. o T n ) )
100 df-fr 
 |-  ( T Fr U_ x e. A B <-> A. r ( ( r C_ U_ x e. A B /\ r =/= (/) ) -> E. n e. r A. o e. r -. o T n ) )
101 99 100 sylibr 
 |-  ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) -> T Fr U_ x e. A B )