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∈On∧B∈On→A⊕˙B∈On
oadif1lem.cl2 ⊢A∈On∧b∈On→A⊕˙b∈On
oadif1lem.sub ⊢A∈On∧B∈On∧A⊆y∧y∈A⊕˙B→∃b∈BA⊕˙b=y
oadif1lem.ord ⊢A∈On∧B∈On→b∈B→A⊕˙b∈A⊕˙B
oadif1lem.word ⊢A∈On∧b∈On→A⊆A⊕˙b
Assertion oadif1lem ⊢A∈On∧B∈On→A⊕˙B∖A=x|∃b∈Bx=A⊕˙b

Proof

Step Hyp Ref Expression
1 oadif1lem.cl1 ⊢A∈On∧B∈On→A⊕˙B∈On
2 oadif1lem.cl2 ⊢A∈On∧b∈On→A⊕˙b∈On
3 oadif1lem.sub ⊢A∈On∧B∈On∧A⊆y∧y∈A⊕˙B→∃b∈BA⊕˙b=y
4 oadif1lem.ord ⊢A∈On∧B∈On→b∈B→A⊕˙b∈A⊕˙B
5 oadif1lem.word ⊢A∈On∧b∈On→A⊆A⊕˙b
6 simpl ⊢A∈On∧B∈On→A∈On
7 onelon ⊢A⊕˙B∈On∧y∈A⊕˙B→y∈On
8 1 7 sylan ⊢A∈On∧B∈On∧y∈A⊕˙B→y∈On
9 ontri1 ⊢A∈On∧y∈On→A⊆y↔¬y∈A
10 6 8 9 syl2an2r ⊢A∈On∧B∈On∧y∈A⊕˙B→A⊆y↔¬y∈A
11 10 pm5.32da ⊢A∈On∧B∈On→y∈A⊕˙B∧A⊆y↔y∈A⊕˙B∧¬y∈A
12 ancom ⊢y∈A⊕˙B∧A⊆y↔A⊆y∧y∈A⊕˙B
13 11 12 bitr3di ⊢A∈On∧B∈On→y∈A⊕˙B∧¬y∈A↔A⊆y∧y∈A⊕˙B
14 13 3 sylbida ⊢A∈On∧B∈On∧y∈A⊕˙B∧¬y∈A→∃b∈BA⊕˙b=y
15 eqcom ⊢A⊕˙b=y↔y=A⊕˙b
16 15 rexbii ⊢∃b∈BA⊕˙b=y↔∃b∈By=A⊕˙b
17 14 16 sylib ⊢A∈On∧B∈On∧y∈A⊕˙B∧¬y∈A→∃b∈By=A⊕˙b
18 17 ex ⊢A∈On∧B∈On→y∈A⊕˙B∧¬y∈A→∃b∈By=A⊕˙b
19 simpr ⊢A∈On∧B∈On∧b∈B∧y=A⊕˙b→y=A⊕˙b
20 4 imp ⊢A∈On∧B∈On∧b∈B→A⊕˙b∈A⊕˙B
21 20 adantr ⊢A∈On∧B∈On∧b∈B∧y=A⊕˙b→A⊕˙b∈A⊕˙B
22 19 21 eqeltrd ⊢A∈On∧B∈On∧b∈B∧y=A⊕˙b→y∈A⊕˙B
23 simpr ⊢A∈On∧B∈On→B∈On
24 onelon ⊢B∈On∧b∈B→b∈On
25 23 24 sylan ⊢A∈On∧B∈On∧b∈B→b∈On
26 6 25 5 syl2an2r ⊢A∈On∧B∈On∧b∈B→A⊆A⊕˙b
27 6 25 2 syl2an2r ⊢A∈On∧B∈On∧b∈B→A⊕˙b∈On
28 ontri1 ⊢A∈On∧A⊕˙b∈On→A⊆A⊕˙b↔¬A⊕˙b∈A
29 6 27 28 syl2an2r ⊢A∈On∧B∈On∧b∈B→A⊆A⊕˙b↔¬A⊕˙b∈A
30 26 29 mpbid ⊢A∈On∧B∈On∧b∈B→¬A⊕˙b∈A
31 30 adantr ⊢A∈On∧B∈On∧b∈B∧y=A⊕˙b→¬A⊕˙b∈A
32 19 31 eqneltrd ⊢A∈On∧B∈On∧b∈B∧y=A⊕˙b→¬y∈A
33 22 32 jca ⊢A∈On∧B∈On∧b∈B∧y=A⊕˙b→y∈A⊕˙B∧¬y∈A
34 33 rexlimdva2 ⊢A∈On∧B∈On→∃b∈By=A⊕˙b→y∈A⊕˙B∧¬y∈A
35 18 34 impbid ⊢A∈On∧B∈On→y∈A⊕˙B∧¬y∈A↔∃b∈By=A⊕˙b
36 eldif ⊢y∈A⊕˙B∖A↔y∈A⊕˙B∧¬y∈A
37 vex ⊢y∈V
38 eqeq1 ⊢x=y→x=A⊕˙b↔y=A⊕˙b
39 38 rexbidv ⊢x=y→∃b∈Bx=A⊕˙b↔∃b∈By=A⊕˙b
40 37 39 elab ⊢y∈x|∃b∈Bx=A⊕˙b↔∃b∈By=A⊕˙b
41 35 36 40 3bitr4g ⊢A∈On∧B∈On→y∈A⊕˙B∖A↔y∈x|∃b∈Bx=A⊕˙b
42 41 eqrdv ⊢A∈On∧B∈On→A⊕˙B∖A=x|∃b∈Bx=A⊕˙b