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 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊕ 𝐵 ) ∈ On )
oadif1lem.cl2 ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ) → ( 𝐴 ⊕ 𝑏 ) ∈ On )
oadif1lem.sub ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐴 ⊆ 𝑦 ∧ 𝑦 ∈ ( 𝐴 ⊕ 𝐵 ) ) ) → ∃ 𝑏 ∈ 𝐵 ( 𝐴 ⊕ 𝑏 ) = 𝑦 )
oadif1lem.ord ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝑏 ∈ 𝐵 → ( 𝐴 ⊕ 𝑏 ) ∈ ( 𝐴 ⊕ 𝐵 ) ) )
oadif1lem.word ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ) → 𝐴 ⊆ ( 𝐴 ⊕ 𝑏 ) )
Assertion oadif1lem ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ⊕ 𝐵 ) ∖ 𝐴 ) = { 𝑥 ∣ ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝐴 ⊕ 𝑏 ) } )

Proof

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