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

Proof

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