Metamath Proof Explorer

Theorem oaordex

Description: Existence theorem for ordering of ordinal sum. Similar to Proposition 4.34(f) of Mendelson p. 266 and its converse. (Contributed by NM, 12-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 onelss ⊢ B ∈ On → A ∈ B → A ⊆ B
2 1 adantl ⊢ A ∈ On ∧ B ∈ On → A ∈ B → A ⊆ B
3 oawordex ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ ∃ x ∈ On A + 𝑜 x = B
4 2 3 sylibd ⊢ A ∈ On ∧ B ∈ On → A ∈ B → ∃ x ∈ On A + 𝑜 x = B
5 oaord1 ⊢ A ∈ On ∧ x ∈ On → ∅ ∈ x ↔ A ∈ A + 𝑜 x
6 eleq2 ⊢ A + 𝑜 x = B → A ∈ A + 𝑜 x ↔ A ∈ B
7 5 6 sylan9bb ⊢ A ∈ On ∧ x ∈ On ∧ A + 𝑜 x = B → ∅ ∈ x ↔ A ∈ B
8 7 biimprcd ⊢ A ∈ B → A ∈ On ∧ x ∈ On ∧ A + 𝑜 x = B → ∅ ∈ x
9 8 exp4c ⊢ A ∈ B → A ∈ On → x ∈ On → A + 𝑜 x = B → ∅ ∈ x
10 9 com12 ⊢ A ∈ On → A ∈ B → x ∈ On → A + 𝑜 x = B → ∅ ∈ x
11 10 imp4b ⊢ A ∈ On ∧ A ∈ B → x ∈ On ∧ A + 𝑜 x = B → ∅ ∈ x
12 simpr ⊢ x ∈ On ∧ A + 𝑜 x = B → A + 𝑜 x = B
13 11 12 jca2 ⊢ A ∈ On ∧ A ∈ B → x ∈ On ∧ A + 𝑜 x = B → ∅ ∈ x ∧ A + 𝑜 x = B
14 13 expd ⊢ A ∈ On ∧ A ∈ B → x ∈ On → A + 𝑜 x = B → ∅ ∈ x ∧ A + 𝑜 x = B
15 14 reximdvai ⊢ A ∈ On ∧ A ∈ B → ∃ x ∈ On A + 𝑜 x = B → ∃ x ∈ On ∅ ∈ x ∧ A + 𝑜 x = B
16 15 ex ⊢ A ∈ On → A ∈ B → ∃ x ∈ On A + 𝑜 x = B → ∃ x ∈ On ∅ ∈ x ∧ A + 𝑜 x = B
17 16 adantr ⊢ A ∈ On ∧ B ∈ On → A ∈ B → ∃ x ∈ On A + 𝑜 x = B → ∃ x ∈ On ∅ ∈ x ∧ A + 𝑜 x = B
18 4 17 mpdd ⊢ A ∈ On ∧ B ∈ On → A ∈ B → ∃ x ∈ On ∅ ∈ x ∧ A + 𝑜 x = B
19 7 biimpd ⊢ A ∈ On ∧ x ∈ On ∧ A + 𝑜 x = B → ∅ ∈ x → A ∈ B
20 19 exp31 ⊢ A ∈ On → x ∈ On → A + 𝑜 x = B → ∅ ∈ x → A ∈ B
21 20 com34 ⊢ A ∈ On → x ∈ On → ∅ ∈ x → A + 𝑜 x = B → A ∈ B
22 21 imp4a ⊢ A ∈ On → x ∈ On → ∅ ∈ x ∧ A + 𝑜 x = B → A ∈ B
23 22 rexlimdv ⊢ A ∈ On → ∃ x ∈ On ∅ ∈ x ∧ A + 𝑜 x = B → A ∈ B
24 23 adantr ⊢ A ∈ On ∧ B ∈ On → ∃ x ∈ On ∅ ∈ x ∧ A + 𝑜 x = B → A ∈ B
25 18 24 impbid ⊢ A ∈ On ∧ B ∈ On → A ∈ B ↔ ∃ x ∈ On ∅ ∈ x ∧ A + 𝑜 x = B