This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )