Metamath Proof Explorer

Theorem oadif1lem

Description: Express the set difference of a continuous sum and its left addend as a class of sums. (Contributed by RP, 13-Feb-2025)

Ref Expression
Hypotheses oadif1lem.cl1 
|- ( ( A e. On /\ B e. On ) -> ( A .(+) B ) e. On )
oadif1lem.cl2 
|- ( ( A e. On /\ b e. On ) -> ( A .(+) b ) e. On )
oadif1lem.sub 
|- ( ( ( A e. On /\ B e. On ) /\ ( A C_ y /\ y e. ( A .(+) B ) ) ) -> E. b e. B ( A .(+) b ) = y )
oadif1lem.ord 
|- ( ( A e. On /\ B e. On ) -> ( b e. B -> ( A .(+) b ) e. ( A .(+) B ) ) )
oadif1lem.word 
|- ( ( A e. On /\ b e. On ) -> A C_ ( A .(+) b ) )
Assertion oadif1lem 
|- ( ( A e. On /\ B e. On ) -> ( ( A .(+) B ) \ A ) = { x | E. b e. B x = ( A .(+) b ) } )

Proof

Step Hyp Ref Expression
1 oadif1lem.cl1 
 |-  ( ( A e. On /\ B e. On ) -> ( A .(+) B ) e. On )
2 oadif1lem.cl2 
 |-  ( ( A e. On /\ b e. On ) -> ( A .(+) b ) e. On )
3 oadif1lem.sub 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( A C_ y /\ y e. ( A .(+) B ) ) ) -> E. b e. B ( A .(+) b ) = y )
4 oadif1lem.ord 
 |-  ( ( A e. On /\ B e. On ) -> ( b e. B -> ( A .(+) b ) e. ( A .(+) B ) ) )
5 oadif1lem.word 
 |-  ( ( A e. On /\ b e. On ) -> A C_ ( A .(+) b ) )
6 simpl 
 |-  ( ( A e. On /\ B e. On ) -> A e. On )
7 onelon 
 |-  ( ( ( A .(+) B ) e. On /\ y e. ( A .(+) B ) ) -> y e. On )
8 1 7 sylan 
 |-  ( ( ( A e. On /\ B e. On ) /\ y e. ( A .(+) B ) ) -> y e. On )
9 ontri1 
 |-  ( ( A e. On /\ y e. On ) -> ( A C_ y <-> -. y e. A ) )
10 6 8 9 syl2an2r 
 |-  ( ( ( A e. On /\ B e. On ) /\ y e. ( A .(+) B ) ) -> ( A C_ y <-> -. y e. A ) )
11 10 pm5.32da 
 |-  ( ( A e. On /\ B e. On ) -> ( ( y e. ( A .(+) B ) /\ A C_ y ) <-> ( y e. ( A .(+) B ) /\ -. y e. A ) ) )
12 ancom 
 |-  ( ( y e. ( A .(+) B ) /\ A C_ y ) <-> ( A C_ y /\ y e. ( A .(+) B ) ) )
13 11 12 bitr3di 
 |-  ( ( A e. On /\ B e. On ) -> ( ( y e. ( A .(+) B ) /\ -. y e. A ) <-> ( A C_ y /\ y e. ( A .(+) B ) ) ) )
14 13 3 sylbida 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( y e. ( A .(+) B ) /\ -. y e. A ) ) -> E. b e. B ( A .(+) b ) = y )
15 eqcom 
 |-  ( ( A .(+) b ) = y <-> y = ( A .(+) b ) )
16 15 rexbii 
 |-  ( E. b e. B ( A .(+) b ) = y <-> E. b e. B y = ( A .(+) b ) )
17 14 16 sylib 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( y e. ( A .(+) B ) /\ -. y e. A ) ) -> E. b e. B y = ( A .(+) b ) )
18 17 ex 
 |-  ( ( A e. On /\ B e. On ) -> ( ( y e. ( A .(+) B ) /\ -. y e. A ) -> E. b e. B y = ( A .(+) b ) ) )
19 simpr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ b e. B ) /\ y = ( A .(+) b ) ) -> y = ( A .(+) b ) )
20 4 imp 
 |-  ( ( ( A e. On /\ B e. On ) /\ b e. B ) -> ( A .(+) b ) e. ( A .(+) B ) )
21 20 adantr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ b e. B ) /\ y = ( A .(+) b ) ) -> ( A .(+) b ) e. ( A .(+) B ) )
22 19 21 eqeltrd 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ b e. B ) /\ y = ( A .(+) b ) ) -> y e. ( A .(+) B ) )
23 simpr 
 |-  ( ( A e. On /\ B e. On ) -> B e. On )
24 onelon 
 |-  ( ( B e. On /\ b e. B ) -> b e. On )
25 23 24 sylan 
 |-  ( ( ( A e. On /\ B e. On ) /\ b e. B ) -> b e. On )
26 6 25 5 syl2an2r 
 |-  ( ( ( A e. On /\ B e. On ) /\ b e. B ) -> A C_ ( A .(+) b ) )
27 6 25 2 syl2an2r 
 |-  ( ( ( A e. On /\ B e. On ) /\ b e. B ) -> ( A .(+) b ) e. On )
28 ontri1 
 |-  ( ( A e. On /\ ( A .(+) b ) e. On ) -> ( A C_ ( A .(+) b ) <-> -. ( A .(+) b ) e. A ) )
29 6 27 28 syl2an2r 
 |-  ( ( ( A e. On /\ B e. On ) /\ b e. B ) -> ( A C_ ( A .(+) b ) <-> -. ( A .(+) b ) e. A ) )
30 26 29 mpbid 
 |-  ( ( ( A e. On /\ B e. On ) /\ b e. B ) -> -. ( A .(+) b ) e. A )
31 30 adantr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ b e. B ) /\ y = ( A .(+) b ) ) -> -. ( A .(+) b ) e. A )
32 19 31 eqneltrd 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ b e. B ) /\ y = ( A .(+) b ) ) -> -. y e. A )
33 22 32 jca 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ b e. B ) /\ y = ( A .(+) b ) ) -> ( y e. ( A .(+) B ) /\ -. y e. A ) )
34 33 rexlimdva2 
 |-  ( ( A e. On /\ B e. On ) -> ( E. b e. B y = ( A .(+) b ) -> ( y e. ( A .(+) B ) /\ -. y e. A ) ) )
35 18 34 impbid 
 |-  ( ( A e. On /\ B e. On ) -> ( ( y e. ( A .(+) B ) /\ -. y e. A ) <-> E. b e. B y = ( A .(+) b ) ) )
36 eldif 
 |-  ( y e. ( ( A .(+) B ) \ A ) <-> ( y e. ( A .(+) B ) /\ -. y e. A ) )
37 vex 
 |-  y e. _V
38 eqeq1 
 |-  ( x = y -> ( x = ( A .(+) b ) <-> y = ( A .(+) b ) ) )
39 38 rexbidv 
 |-  ( x = y -> ( E. b e. B x = ( A .(+) b ) <-> E. b e. B y = ( A .(+) b ) ) )
40 37 39 elab 
 |-  ( y e. { x | E. b e. B x = ( A .(+) b ) } <-> E. b e. B y = ( A .(+) b ) )
41 35 36 40 3bitr4g 
 |-  ( ( A e. On /\ B e. On ) -> ( y e. ( ( A .(+) B ) \ A ) <-> y e. { x | E. b e. B x = ( A .(+) b ) } ) )
42 41 eqrdv 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A .(+) B ) \ A ) = { x | E. b e. B x = ( A .(+) b ) } )