Metamath Proof Explorer

Theorem weiunlem1

Description: Lemma for weiunpo , weiunso , weiunfr , and weiunse . (Contributed by Matthew House, 8-Sep-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 weiunlem1 
|- ( C T D <-> ( ( C e. U_ x e. A B /\ D e. U_ x e. A B ) /\ ( ( F ` C ) R ( F ` D ) \/ ( ( F ` C ) = ( F ` D ) /\ C [_ ( F ` C ) / x ]_ S D ) ) ) )

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 simpl 
 |-  ( ( y = C /\ z = D ) -> y = C )
4 3 fveq2d 
 |-  ( ( y = C /\ z = D ) -> ( F ` y ) = ( F ` C ) )
5 simpr 
 |-  ( ( y = C /\ z = D ) -> z = D )
6 5 fveq2d 
 |-  ( ( y = C /\ z = D ) -> ( F ` z ) = ( F ` D ) )
7 4 6 breq12d 
 |-  ( ( y = C /\ z = D ) -> ( ( F ` y ) R ( F ` z ) <-> ( F ` C ) R ( F ` D ) ) )
8 4 6 eqeq12d 
 |-  ( ( y = C /\ z = D ) -> ( ( F ` y ) = ( F ` z ) <-> ( F ` C ) = ( F ` D ) ) )
9 4 csbeq1d 
 |-  ( ( y = C /\ z = D ) -> [_ ( F ` y ) / x ]_ S = [_ ( F ` C ) / x ]_ S )
10 3 9 5 breq123d 
 |-  ( ( y = C /\ z = D ) -> ( y [_ ( F ` y ) / x ]_ S z <-> C [_ ( F ` C ) / x ]_ S D ) )
11 8 10 anbi12d 
 |-  ( ( y = C /\ z = D ) -> ( ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) <-> ( ( F ` C ) = ( F ` D ) /\ C [_ ( F ` C ) / x ]_ S D ) ) )
12 7 11 orbi12d 
 |-  ( ( y = C /\ z = D ) -> ( ( ( F ` y ) R ( F ` z ) \/ ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) <-> ( ( F ` C ) R ( F ` D ) \/ ( ( F ` C ) = ( F ` D ) /\ C [_ ( F ` C ) / x ]_ S D ) ) ) )
13 12 2 brab2a 
 |-  ( C T D <-> ( ( C e. U_ x e. A B /\ D e. U_ x e. A B ) /\ ( ( F ` C ) R ( F ` D ) \/ ( ( F ` C ) = ( F ` D ) /\ C [_ ( F ` C ) / x ]_ S D ) ) ) )