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 e. On /\ B e. On ) -> ( A e. B <-> E. x e. On ( (/) e. x /\ ( A +o x ) = B ) ) )

Proof

Step Hyp Ref Expression
1 onelss 
 |-  ( B e. On -> ( A e. B -> A C_ B ) )
2 1 adantl 
 |-  ( ( A e. On /\ B e. On ) -> ( A e. B -> A C_ B ) )
3 oawordex 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B <-> E. x e. On ( A +o x ) = B ) )
4 2 3 sylibd 
 |-  ( ( A e. On /\ B e. On ) -> ( A e. B -> E. x e. On ( A +o x ) = B ) )
5 oaord1 
 |-  ( ( A e. On /\ x e. On ) -> ( (/) e. x <-> A e. ( A +o x ) ) )
6 eleq2 
 |-  ( ( A +o x ) = B -> ( A e. ( A +o x ) <-> A e. B ) )
7 5 6 sylan9bb 
 |-  ( ( ( A e. On /\ x e. On ) /\ ( A +o x ) = B ) -> ( (/) e. x <-> A e. B ) )
8 7 biimprcd 
 |-  ( A e. B -> ( ( ( A e. On /\ x e. On ) /\ ( A +o x ) = B ) -> (/) e. x ) )
9 8 exp4c 
 |-  ( A e. B -> ( A e. On -> ( x e. On -> ( ( A +o x ) = B -> (/) e. x ) ) ) )
10 9 com12 
 |-  ( A e. On -> ( A e. B -> ( x e. On -> ( ( A +o x ) = B -> (/) e. x ) ) ) )
11 10 imp4b 
 |-  ( ( A e. On /\ A e. B ) -> ( ( x e. On /\ ( A +o x ) = B ) -> (/) e. x ) )
12 simpr 
 |-  ( ( x e. On /\ ( A +o x ) = B ) -> ( A +o x ) = B )
13 11 12 jca2 
 |-  ( ( A e. On /\ A e. B ) -> ( ( x e. On /\ ( A +o x ) = B ) -> ( (/) e. x /\ ( A +o x ) = B ) ) )
14 13 expd 
 |-  ( ( A e. On /\ A e. B ) -> ( x e. On -> ( ( A +o x ) = B -> ( (/) e. x /\ ( A +o x ) = B ) ) ) )
15 14 reximdvai 
 |-  ( ( A e. On /\ A e. B ) -> ( E. x e. On ( A +o x ) = B -> E. x e. On ( (/) e. x /\ ( A +o x ) = B ) ) )
16 15 ex 
 |-  ( A e. On -> ( A e. B -> ( E. x e. On ( A +o x ) = B -> E. x e. On ( (/) e. x /\ ( A +o x ) = B ) ) ) )
17 16 adantr 
 |-  ( ( A e. On /\ B e. On ) -> ( A e. B -> ( E. x e. On ( A +o x ) = B -> E. x e. On ( (/) e. x /\ ( A +o x ) = B ) ) ) )
18 4 17 mpdd 
 |-  ( ( A e. On /\ B e. On ) -> ( A e. B -> E. x e. On ( (/) e. x /\ ( A +o x ) = B ) ) )
19 7 biimpd 
 |-  ( ( ( A e. On /\ x e. On ) /\ ( A +o x ) = B ) -> ( (/) e. x -> A e. B ) )
20 19 exp31 
 |-  ( A e. On -> ( x e. On -> ( ( A +o x ) = B -> ( (/) e. x -> A e. B ) ) ) )
21 20 com34 
 |-  ( A e. On -> ( x e. On -> ( (/) e. x -> ( ( A +o x ) = B -> A e. B ) ) ) )
22 21 imp4a 
 |-  ( A e. On -> ( x e. On -> ( ( (/) e. x /\ ( A +o x ) = B ) -> A e. B ) ) )
23 22 rexlimdv 
 |-  ( A e. On -> ( E. x e. On ( (/) e. x /\ ( A +o x ) = B ) -> A e. B ) )
24 23 adantr 
 |-  ( ( A e. On /\ B e. On ) -> ( E. x e. On ( (/) e. x /\ ( A +o x ) = B ) -> A e. B ) )
25 18 24 impbid 
 |-  ( ( A e. On /\ B e. On ) -> ( A e. B <-> E. x e. On ( (/) e. x /\ ( A +o x ) = B ) ) )