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 ∖ B x ⊆ y
16 13 15 syl6 ⊢ Ord ⁡ A ∧ B ∈ A ∧ x ∈ A → x ∈ B → ∃ y ∈ A ∖ B x ⊆ 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 ∖ B x ⊆ y
24 21 23 syl6 ⊢ x ∈ A → ¬ x ∈ B → ∃ y ∈ A ∖ B x ⊆ y
25 24 adantl ⊢ Ord ⁡ A ∧ B ∈ A ∧ x ∈ A → ¬ x ∈ B → ∃ y ∈ A ∖ B x ⊆ y
26 16 25 pm2.61d ⊢ Ord ⁡ A ∧ B ∈ A ∧ x ∈ A → ∃ y ∈ A ∖ B x ⊆ y
27 26 ralrimiva ⊢ Ord ⁡ A ∧ B ∈ A → ∀ x ∈ A ∃ y ∈ A ∖ B x ⊆ y
28 unidif ⊢ ∀ x ∈ A ∃ y ∈ A ∖ B x ⊆ y → ⋃ A ∖ B = ⋃ A
29 27 28 syl ⊢ Ord ⁡ A ∧ B ∈ A → ⋃ A ∖ B = ⋃ A