This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oawordex

Description: Existence theorem for weak ordering of ordinal sum. Proposition 8.8 of TakeutiZaring p. 59 and its converse. See oawordeu for uniqueness. (Contributed by NM, 12-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 oawordeu ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ B → ∃! x ∈ On A + 𝑜 x = B
2 1 ex ⊢ A ∈ On ∧ B ∈ On → A ⊆ B → ∃! x ∈ On A + 𝑜 x = B
3 reurex ⊢ ∃! x ∈ On A + 𝑜 x = B → ∃ x ∈ On A + 𝑜 x = B
4 2 3 syl6 ⊢ A ∈ On ∧ B ∈ On → A ⊆ B → ∃ x ∈ On A + 𝑜 x = B
5 oawordexr ⊢ A ∈ On ∧ ∃ x ∈ On A + 𝑜 x = B → A ⊆ B
6 5 ex ⊢ A ∈ On → ∃ x ∈ On A + 𝑜 x = B → A ⊆ B
7 6 adantr ⊢ A ∈ On ∧ B ∈ On → ∃ x ∈ On A + 𝑜 x = B → A ⊆ B
8 4 7 impbid ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ ∃ x ∈ On A + 𝑜 x = B