Theorem oawordexr

Description: Existence theorem for weak ordering of ordinal sum. (Contributed by NM, 12-Dec-2004)

	Ref	Expression
Assertion	oawordexr	⊢ ( ( 𝐴 ∈ On ∧ ∃ 𝑥 ∈ On ( 𝐴 +o 𝑥 ) = 𝐵 ) → 𝐴 ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		oaword1	⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → 𝐴 ⊆ ( 𝐴 +o 𝑥 ) )
2		sseq2	⊢ ( ( 𝐴 +o 𝑥 ) = 𝐵 → ( 𝐴 ⊆ ( 𝐴 +o 𝑥 ) ↔ 𝐴 ⊆ 𝐵 ) )
3	1 2	syl5ibcom	⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( ( 𝐴 +o 𝑥 ) = 𝐵 → 𝐴 ⊆ 𝐵 ) )
4	3	rexlimdva	⊢ ( 𝐴 ∈ On → ( ∃ 𝑥 ∈ On ( 𝐴 +o 𝑥 ) = 𝐵 → 𝐴 ⊆ 𝐵 ) )
5	4	imp	⊢ ( ( 𝐴 ∈ On ∧ ∃ 𝑥 ∈ On ( 𝐴 +o 𝑥 ) = 𝐵 ) → 𝐴 ⊆ 𝐵 )