Metamath Proof Explorer

Theorem oawordex2

Description: If C is between A (inclusive) and ( A +o B ) (exclusive), there is an ordinal which equals C when summed to A . This is a slightly different statement than oawordex or oawordeu . (Contributed by RP, 7-Jan-2025)

Ref Expression
Assertion oawordex2 ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ C ∧ C ∈ A + 𝑜 B → ∃ x ∈ B A + 𝑜 x = C

Proof

Step Hyp Ref Expression
1 simprl ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ C ∧ C ∈ A + 𝑜 B → A ⊆ C
2 simpll ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ C ∧ C ∈ A + 𝑜 B → A ∈ On
3 oacl ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B ∈ On
4 simpr ⊢ A ⊆ C ∧ C ∈ A + 𝑜 B → C ∈ A + 𝑜 B
5 onelon ⊢ A + 𝑜 B ∈ On ∧ C ∈ A + 𝑜 B → C ∈ On
6 3 4 5 syl2an ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ C ∧ C ∈ A + 𝑜 B → C ∈ On
7 oawordex ⊢ A ∈ On ∧ C ∈ On → A ⊆ C ↔ ∃ x ∈ On A + 𝑜 x = C
8 2 6 7 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ C ∧ C ∈ A + 𝑜 B → A ⊆ C ↔ ∃ x ∈ On A + 𝑜 x = C
9 1 8 mpbid ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ C ∧ C ∈ A + 𝑜 B → ∃ x ∈ On A + 𝑜 x = C
10 simprr ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ C ∧ C ∈ A + 𝑜 B ∧ x ∈ On ∧ A + 𝑜 x = C → A + 𝑜 x = C
11 simprr ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ C ∧ C ∈ A + 𝑜 B → C ∈ A + 𝑜 B
12 11 adantr ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ C ∧ C ∈ A + 𝑜 B ∧ x ∈ On ∧ A + 𝑜 x = C → C ∈ A + 𝑜 B
13 10 12 eqeltrd ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ C ∧ C ∈ A + 𝑜 B ∧ x ∈ On ∧ A + 𝑜 x = C → A + 𝑜 x ∈ A + 𝑜 B
14 simprl ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ C ∧ C ∈ A + 𝑜 B ∧ x ∈ On ∧ A + 𝑜 x = C → x ∈ On
15 simpllr ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ C ∧ C ∈ A + 𝑜 B ∧ x ∈ On ∧ A + 𝑜 x = C → B ∈ On
16 2 adantr ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ C ∧ C ∈ A + 𝑜 B ∧ x ∈ On ∧ A + 𝑜 x = C → A ∈ On
17 oaord ⊢ x ∈ On ∧ B ∈ On ∧ A ∈ On → x ∈ B ↔ A + 𝑜 x ∈ A + 𝑜 B
18 14 15 16 17 syl3anc ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ C ∧ C ∈ A + 𝑜 B ∧ x ∈ On ∧ A + 𝑜 x = C → x ∈ B ↔ A + 𝑜 x ∈ A + 𝑜 B
19 13 18 mpbird ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ C ∧ C ∈ A + 𝑜 B ∧ x ∈ On ∧ A + 𝑜 x = C → x ∈ B
20 9 19 10 reximssdv ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ C ∧ C ∈ A + 𝑜 B → ∃ x ∈ B A + 𝑜 x = C