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 ∈ B A ⊕ ˙ 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 ∈ B x = 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 ∈ B A ⊕ ˙ 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 ∈ B A ⊕ ˙ b = y
15 eqcom ⊢ A ⊕ ˙ b = y ↔ y = A ⊕ ˙ b
16 15 rexbii ⊢ ∃ b ∈ B A ⊕ ˙ b = y ↔ ∃ b ∈ B y = A ⊕ ˙ b
17 14 16 sylib ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ A ⊕ ˙ B ∧ ¬ y ∈ A → ∃ b ∈ B y = A ⊕ ˙ b
18 17 ex ⊢ A ∈ On ∧ B ∈ On → y ∈ A ⊕ ˙ B ∧ ¬ y ∈ A → ∃ b ∈ B y = 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 ∈ B y = A ⊕ ˙ b → y ∈ A ⊕ ˙ B ∧ ¬ y ∈ A
35 18 34 impbid ⊢ A ∈ On ∧ B ∈ On → y ∈ A ⊕ ˙ B ∧ ¬ y ∈ A ↔ ∃ b ∈ B y = 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 ∈ B x = A ⊕ ˙ b ↔ ∃ b ∈ B y = A ⊕ ˙ b
40 37 39 elab ⊢ y ∈ x | ∃ b ∈ B x = A ⊕ ˙ b ↔ ∃ b ∈ B y = A ⊕ ˙ b
41 35 36 40 3bitr4g ⊢ A ∈ On ∧ B ∈ On → y ∈ A ⊕ ˙ B ∖ A ↔ y ∈ x | ∃ b ∈ B x = A ⊕ ˙ b
42 41 eqrdv ⊢ A ∈ On ∧ B ∈ On → A ⊕ ˙ B ∖ A = x | ∃ b ∈ B x = A ⊕ ˙ b