Metamath Proof Explorer

Theorem weiunfr

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

Ref Expression
Hypotheses weiunfr.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 ) )
weiunfr.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 weiunfr.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 weiunfr.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 breq2 
 |-  ( u = m -> ( v R u <-> v R m ) )
4 3 notbid 
 |-  ( u = m -> ( -. v R u <-> -. v R m ) )
5 4 ralbidv 
 |-  ( u = m -> ( A. v e. { x e. A | w e. B } -. v R u <-> A. v e. { x e. A | w e. B } -. v R m ) )
6 5 cbvriotavw 
 |-  ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) = ( iota_ m e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R m )
7 nfcv 
 |-  F/_ x A
8 nfcv 
 |-  F/_ l A
9 nfv 
 |-  F/ l w e. B
10 nfcsb1v 
 |-  F/_ x [_ l / x ]_ B
11 10 nfcri 
 |-  F/ x w e. [_ l / x ]_ B
12 csbeq1a 
 |-  ( x = l -> B = [_ l / x ]_ B )
13 12 eleq2d 
 |-  ( x = l -> ( w e. B <-> w e. [_ l / x ]_ B ) )
14 7 8 9 11 13 cbvrabw 
 |-  { x e. A | w e. B } = { l e. A | w e. [_ l / x ]_ B }
15 eleq1w 
 |-  ( w = k -> ( w e. [_ l / x ]_ B <-> k e. [_ l / x ]_ B ) )
16 15 rabbidv 
 |-  ( w = k -> { l e. A | w e. [_ l / x ]_ B } = { l e. A | k e. [_ l / x ]_ B } )
17 14 16 eqtrid 
 |-  ( w = k -> { x e. A | w e. B } = { l e. A | k e. [_ l / x ]_ B } )
18 breq1 
 |-  ( v = n -> ( v R m <-> n R m ) )
19 18 notbid 
 |-  ( v = n -> ( -. v R m <-> -. n R m ) )
20 19 adantl 
 |-  ( ( w = k /\ v = n ) -> ( -. v R m <-> -. n R m ) )
21 17 adantr 
 |-  ( ( w = k /\ v = n ) -> { x e. A | w e. B } = { l e. A | k e. [_ l / x ]_ B } )
22 20 21 cbvraldva2 
 |-  ( w = k -> ( A. v e. { x e. A | w e. B } -. v R m <-> A. n e. { l e. A | k e. [_ l / x ]_ B } -. n R m ) )
23 17 22 riotaeqbidv 
 |-  ( w = k -> ( iota_ m e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R m ) = ( iota_ m e. { l e. A | k e. [_ l / x ]_ B } A. n e. { l e. A | k e. [_ l / x ]_ B } -. n R m ) )
24 6 23 eqtrid 
 |-  ( w = k -> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) = ( iota_ m e. { l e. A | k e. [_ l / x ]_ B } A. n e. { l e. A | k e. [_ l / x ]_ B } -. n R m ) )
25 24 cbvmptv 
 |-  ( 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 ) ) = ( k e. U_ x e. A B |-> ( iota_ m e. { l e. A | k e. [_ l / x ]_ B } A. n e. { l e. A | k e. [_ l / x ]_ B } -. n R m ) )
26 nfcv 
 |-  F/_ l B
27 26 10 12 cbviun 
 |-  U_ x e. A B = U_ l e. A [_ l / x ]_ B
28 27 mpteq1i 
 |-  ( k e. U_ x e. A B |-> ( iota_ m e. { l e. A | k e. [_ l / x ]_ B } A. n e. { l e. A | k e. [_ l / x ]_ B } -. n R m ) ) = ( k e. U_ l e. A [_ l / x ]_ B |-> ( iota_ m e. { l e. A | k e. [_ l / x ]_ B } A. n e. { l e. A | k e. [_ l / x ]_ B } -. n R m ) )
29 1 25 28 3eqtri 
 |-  F = ( k e. U_ l e. A [_ l / x ]_ B |-> ( iota_ m e. { l e. A | k e. [_ l / x ]_ B } A. n e. { l e. A | k e. [_ l / x ]_ B } -. n R m ) )
30 simpl 
 |-  ( ( y = o /\ z = p ) -> y = o )
31 27 a1i 
 |-  ( ( y = o /\ z = p ) -> U_ x e. A B = U_ l e. A [_ l / x ]_ B )
32 30 31 eleq12d 
 |-  ( ( y = o /\ z = p ) -> ( y e. U_ x e. A B <-> o e. U_ l e. A [_ l / x ]_ B ) )
33 simpr 
 |-  ( ( y = o /\ z = p ) -> z = p )
34 33 31 eleq12d 
 |-  ( ( y = o /\ z = p ) -> ( z e. U_ x e. A B <-> p e. U_ l e. A [_ l / x ]_ B ) )
35 32 34 anbi12d 
 |-  ( ( y = o /\ z = p ) -> ( ( y e. U_ x e. A B /\ z e. U_ x e. A B ) <-> ( o e. U_ l e. A [_ l / x ]_ B /\ p e. U_ l e. A [_ l / x ]_ B ) ) )
36 30 fveq2d 
 |-  ( ( y = o /\ z = p ) -> ( F ` y ) = ( F ` o ) )
37 33 fveq2d 
 |-  ( ( y = o /\ z = p ) -> ( F ` z ) = ( F ` p ) )
38 36 37 breq12d 
 |-  ( ( y = o /\ z = p ) -> ( ( F ` y ) R ( F ` z ) <-> ( F ` o ) R ( F ` p ) ) )
39 36 37 eqeq12d 
 |-  ( ( y = o /\ z = p ) -> ( ( F ` y ) = ( F ` z ) <-> ( F ` o ) = ( F ` p ) ) )
40 36 csbeq1d 
 |-  ( ( y = o /\ z = p ) -> [_ ( F ` y ) / x ]_ S = [_ ( F ` o ) / x ]_ S )
41 csbcow 
 |-  [_ ( F ` o ) / l ]_ [_ l / x ]_ S = [_ ( F ` o ) / x ]_ S
42 40 41 eqtr4di 
 |-  ( ( y = o /\ z = p ) -> [_ ( F ` y ) / x ]_ S = [_ ( F ` o ) / l ]_ [_ l / x ]_ S )
43 30 42 33 breq123d 
 |-  ( ( y = o /\ z = p ) -> ( y [_ ( F ` y ) / x ]_ S z <-> o [_ ( F ` o ) / l ]_ [_ l / x ]_ S p ) )
44 39 43 anbi12d 
 |-  ( ( y = o /\ z = p ) -> ( ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) <-> ( ( F ` o ) = ( F ` p ) /\ o [_ ( F ` o ) / l ]_ [_ l / x ]_ S p ) ) )
45 38 44 orbi12d 
 |-  ( ( y = o /\ z = p ) -> ( ( ( F ` y ) R ( F ` z ) \/ ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) <-> ( ( F ` o ) R ( F ` p ) \/ ( ( F ` o ) = ( F ` p ) /\ o [_ ( F ` o ) / l ]_ [_ l / x ]_ S p ) ) ) )
46 35 45 anbi12d 
 |-  ( ( y = o /\ z = p ) -> ( ( ( 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 ) ) ) <-> ( ( o e. U_ l e. A [_ l / x ]_ B /\ p e. U_ l e. A [_ l / x ]_ B ) /\ ( ( F ` o ) R ( F ` p ) \/ ( ( F ` o ) = ( F ` p ) /\ o [_ ( F ` o ) / l ]_ [_ l / x ]_ S p ) ) ) ) )
47 46 cbvopabv 
 |-  { <. 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 ) ) ) } = { <. o , p >. | ( ( o e. U_ l e. A [_ l / x ]_ B /\ p e. U_ l e. A [_ l / x ]_ B ) /\ ( ( F ` o ) R ( F ` p ) \/ ( ( F ` o ) = ( F ` p ) /\ o [_ ( F ` o ) / l ]_ [_ l / x ]_ S p ) ) ) }
48 2 47 eqtri 
 |-  T = { <. o , p >. | ( ( o e. U_ l e. A [_ l / x ]_ B /\ p e. U_ l e. A [_ l / x ]_ B ) /\ ( ( F ` o ) R ( F ` p ) \/ ( ( F ` o ) = ( F ` p ) /\ o [_ ( F ` o ) / l ]_ [_ l / x ]_ S p ) ) ) }
49 breq1 
 |-  ( q = t -> ( q R s <-> t R s ) )
50 49 notbid 
 |-  ( q = t -> ( -. q R s <-> -. t R s ) )
51 50 cbvralvw 
 |-  ( A. q e. ( F " r ) -. q R s <-> A. t e. ( F " r ) -. t R s )
52 51 a1i 
 |-  ( s e. ( F " r ) -> ( A. q e. ( F " r ) -. q R s <-> A. t e. ( F " r ) -. t R s ) )
53 52 riotabiia 
 |-  ( iota_ s e. ( F " r ) A. q e. ( F " r ) -. q R s ) = ( iota_ s e. ( F " r ) A. t e. ( F " r ) -. t R s )
54 29 48 53 weiunfrlem2 
 |-  ( ( R We A /\ R Se A /\ A. l e. A [_ l / x ]_ S Fr [_ l / x ]_ B ) -> T Fr U_ l e. A [_ l / x ]_ B )
55 nfv 
 |-  F/ l S Fr B
56 nfcsb1v 
 |-  F/_ x [_ l / x ]_ S
57 56 10 nffr 
 |-  F/ x [_ l / x ]_ S Fr [_ l / x ]_ B
58 csbeq1a 
 |-  ( x = l -> S = [_ l / x ]_ S )
59 freq1 
 |-  ( S = [_ l / x ]_ S -> ( S Fr B <-> [_ l / x ]_ S Fr B ) )
60 58 59 syl 
 |-  ( x = l -> ( S Fr B <-> [_ l / x ]_ S Fr B ) )
61 freq2 
 |-  ( B = [_ l / x ]_ B -> ( [_ l / x ]_ S Fr B <-> [_ l / x ]_ S Fr [_ l / x ]_ B ) )
62 12 61 syl 
 |-  ( x = l -> ( [_ l / x ]_ S Fr B <-> [_ l / x ]_ S Fr [_ l / x ]_ B ) )
63 60 62 bitrd 
 |-  ( x = l -> ( S Fr B <-> [_ l / x ]_ S Fr [_ l / x ]_ B ) )
64 55 57 63 cbvralw 
 |-  ( A. x e. A S Fr B <-> A. l e. A [_ l / x ]_ S Fr [_ l / x ]_ B )
65 64 3anbi3i 
 |-  ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) <-> ( R We A /\ R Se A /\ A. l e. A [_ l / x ]_ S Fr [_ l / x ]_ B ) )
66 freq2 
 |-  ( U_ x e. A B = U_ l e. A [_ l / x ]_ B -> ( T Fr U_ x e. A B <-> T Fr U_ l e. A [_ l / x ]_ B ) )
67 27 66 ax-mp 
 |-  ( T Fr U_ x e. A B <-> T Fr U_ l e. A [_ l / x ]_ B )
68 54 65 67 3imtr4i 
 |-  ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) -> T Fr U_ x e. A B )