Theorem oadif1

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

	Ref	Expression
Assertion	oadif1	|- ( ( A e. On /\ B e. On ) -> ( ( A +o B ) \ A ) = { x | E. b e. B x = ( A +o b ) } )

Proof

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