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 ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ∈ ( 𝐴 +o 𝐵 ) ) ) → ∃ 𝑥 ∈ 𝐵 ( 𝐴 +o 𝑥 ) = 𝐶 )

Proof

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