Metamath Proof Explorer

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 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) = { 𝑥 ∣ ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝐴 +o 𝑏 ) } )

Proof

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