Metamath Proof Explorer

Theorem onunel

Description: The union of two ordinals is in a third iff both of the first two are. (Contributed by Scott Fenton, 10-Sep-2024)

Ref Expression
Assertion onunel 
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A u. B ) e. C <-> ( A e. C /\ B e. C ) ) )

Proof

Step Hyp Ref Expression
1 ssequn1 
 |-  ( A C_ B <-> ( A u. B ) = B )
2 1 biimpi 
 |-  ( A C_ B -> ( A u. B ) = B )
3 2 eleq1d 
 |-  ( A C_ B -> ( ( A u. B ) e. C <-> B e. C ) )
4 3 adantl 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( ( A u. B ) e. C <-> B e. C ) )
5 ontr2 
 |-  ( ( A e. On /\ C e. On ) -> ( ( A C_ B /\ B e. C ) -> A e. C ) )
6 5 3adant2 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A C_ B /\ B e. C ) -> A e. C ) )
7 6 expdimp 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( B e. C -> A e. C ) )
8 7 pm4.71rd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( B e. C <-> ( A e. C /\ B e. C ) ) )
9 4 8 bitrd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ A C_ B ) -> ( ( A u. B ) e. C <-> ( A e. C /\ B e. C ) ) )
10 ssequn2 
 |-  ( B C_ A <-> ( A u. B ) = A )
11 10 biimpi 
 |-  ( B C_ A -> ( A u. B ) = A )
12 11 eleq1d 
 |-  ( B C_ A -> ( ( A u. B ) e. C <-> A e. C ) )
13 12 adantl 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ B C_ A ) -> ( ( A u. B ) e. C <-> A e. C ) )
14 ontr2 
 |-  ( ( B e. On /\ C e. On ) -> ( ( B C_ A /\ A e. C ) -> B e. C ) )
15 14 3adant1 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( B C_ A /\ A e. C ) -> B e. C ) )
16 15 expdimp 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ B C_ A ) -> ( A e. C -> B e. C ) )
17 16 pm4.71d 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ B C_ A ) -> ( A e. C <-> ( A e. C /\ B e. C ) ) )
18 13 17 bitrd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ B C_ A ) -> ( ( A u. B ) e. C <-> ( A e. C /\ B e. C ) ) )
19 eloni 
 |-  ( A e. On -> Ord A )
20 eloni 
 |-  ( B e. On -> Ord B )
21 ordtri2or2 
 |-  ( ( Ord A /\ Ord B ) -> ( A C_ B \/ B C_ A ) )
22 19 20 21 syl2an 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B \/ B C_ A ) )
23 22 3adant3 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B \/ B C_ A ) )
24 9 18 23 mpjaodan 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A u. B ) e. C <-> ( A e. C /\ B e. C ) ) )