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 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ∪ ( 𝐴 ∖ 𝐵 ) = ∪ 𝐴 )

Proof

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

Metamath Proof Explorer

Theorem ordunidif

Proof