Metamath Proof Explorer


Theorem ordunidif

Description: The union of an ordinal stays the same if a subset equal to one of its elements is removed. (Contributed by NM, 10-Dec-2004)

Ref Expression
Assertion ordunidif
|- ( ( Ord A /\ B e. A ) -> U. ( A \ B ) = U. A )

Proof

Step Hyp Ref Expression
1 ordelon
 |-  ( ( Ord A /\ B e. A ) -> B e. On )
2 onelss
 |-  ( B e. On -> ( x e. B -> x C_ B ) )
3 1 2 syl
 |-  ( ( Ord A /\ B e. A ) -> ( x e. B -> x C_ B ) )
4 eloni
 |-  ( B e. On -> Ord B )
5 ordirr
 |-  ( Ord B -> -. B e. B )
6 4 5 syl
 |-  ( B e. On -> -. B e. B )
7 eldif
 |-  ( B e. ( A \ B ) <-> ( B e. A /\ -. B e. B ) )
8 7 simplbi2
 |-  ( B e. A -> ( -. B e. B -> B e. ( A \ B ) ) )
9 6 8 syl5
 |-  ( B e. A -> ( B e. On -> B e. ( A \ B ) ) )
10 9 adantl
 |-  ( ( Ord A /\ B e. A ) -> ( B e. On -> B e. ( A \ B ) ) )
11 1 10 mpd
 |-  ( ( Ord A /\ B e. A ) -> B e. ( A \ B ) )
12 3 11 jctild
 |-  ( ( Ord A /\ B e. A ) -> ( x e. B -> ( B e. ( A \ B ) /\ x C_ B ) ) )
13 12 adantr
 |-  ( ( ( Ord A /\ B e. A ) /\ x e. A ) -> ( x e. B -> ( B e. ( A \ B ) /\ x C_ B ) ) )
14 sseq2
 |-  ( y = B -> ( x C_ y <-> x C_ B ) )
15 14 rspcev
 |-  ( ( B e. ( A \ B ) /\ x C_ B ) -> E. y e. ( A \ B ) x C_ y )
16 13 15 syl6
 |-  ( ( ( Ord A /\ B e. A ) /\ x e. A ) -> ( x e. B -> E. y e. ( A \ B ) x C_ y ) )
17 eldif
 |-  ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
18 17 biimpri
 |-  ( ( x e. A /\ -. x e. B ) -> x e. ( A \ B ) )
19 ssid
 |-  x C_ x
20 18 19 jctir
 |-  ( ( x e. A /\ -. x e. B ) -> ( x e. ( A \ B ) /\ x C_ x ) )
21 20 ex
 |-  ( x e. A -> ( -. x e. B -> ( x e. ( A \ B ) /\ x C_ x ) ) )
22 sseq2
 |-  ( y = x -> ( x C_ y <-> x C_ x ) )
23 22 rspcev
 |-  ( ( x e. ( A \ B ) /\ x C_ x ) -> E. y e. ( A \ B ) x C_ y )
24 21 23 syl6
 |-  ( x e. A -> ( -. x e. B -> E. y e. ( A \ B ) x C_ y ) )
25 24 adantl
 |-  ( ( ( Ord A /\ B e. A ) /\ x e. A ) -> ( -. x e. B -> E. y e. ( A \ B ) x C_ y ) )
26 16 25 pm2.61d
 |-  ( ( ( Ord A /\ B e. A ) /\ x e. A ) -> E. y e. ( A \ B ) x C_ y )
27 26 ralrimiva
 |-  ( ( Ord A /\ B e. A ) -> A. x e. A E. y e. ( A \ B ) x C_ y )
28 unidif
 |-  ( A. x e. A E. y e. ( A \ B ) x C_ y -> U. ( A \ B ) = U. A )
29 27 28 syl
 |-  ( ( Ord A /\ B e. A ) -> U. ( A \ B ) = U. A )