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∈A→⋃A∖B=⋃A

Proof

Step Hyp Ref Expression
1 ordelon ⊢Ord⁡A∧B∈A→B∈On
2 onelss ⊢B∈On→x∈B→x⊆B
3 1 2 syl ⊢Ord⁡A∧B∈A→x∈B→x⊆B
4 eloni ⊢B∈On→Ord⁡B
5 ordirr ⊢Ord⁡B→¬B∈B
6 4 5 syl ⊢B∈On→¬B∈B
7 eldif ⊢B∈A∖B↔B∈A∧¬B∈B
8 7 simplbi2 ⊢B∈A→¬B∈B→B∈A∖B
9 6 8 syl5 ⊢B∈A→B∈On→B∈A∖B
10 9 adantl ⊢Ord⁡A∧B∈A→B∈On→B∈A∖B
11 1 10 mpd ⊢Ord⁡A∧B∈A→B∈A∖B
12 3 11 jctild ⊢Ord⁡A∧B∈A→x∈B→B∈A∖B∧x⊆B
13 12 adantr ⊢Ord⁡A∧B∈A∧x∈A→x∈B→B∈A∖B∧x⊆B
14 sseq2 ⊢y=B→x⊆y↔x⊆B
15 14 rspcev ⊢B∈A∖B∧x⊆B→∃y∈A∖Bx⊆y
16 13 15 syl6 ⊢Ord⁡A∧B∈A∧x∈A→x∈B→∃y∈A∖Bx⊆y
17 eldif ⊢x∈A∖B↔x∈A∧¬x∈B
18 17 biimpri ⊢x∈A∧¬x∈B→x∈A∖B
19 ssid ⊢x⊆x
20 18 19 jctir ⊢x∈A∧¬x∈B→x∈A∖B∧x⊆x
21 20 ex ⊢x∈A→¬x∈B→x∈A∖B∧x⊆x
22 sseq2 ⊢y=x→x⊆y↔x⊆x
23 22 rspcev ⊢x∈A∖B∧x⊆x→∃y∈A∖Bx⊆y
24 21 23 syl6 ⊢x∈A→¬x∈B→∃y∈A∖Bx⊆y
25 24 adantl ⊢Ord⁡A∧B∈A∧x∈A→¬x∈B→∃y∈A∖Bx⊆y
26 16 25 pm2.61d ⊢Ord⁡A∧B∈A∧x∈A→∃y∈A∖Bx⊆y
27 26 ralrimiva ⊢Ord⁡A∧B∈A→∀x∈A∃y∈A∖Bx⊆y
28 unidif ⊢∀x∈A∃y∈A∖Bx⊆y→⋃A∖B=⋃A
29 27 28 syl ⊢Ord⁡A∧B∈A→⋃A∖B=⋃A