Description: Any collection of singletons is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | sndisj | ⊢ Disj 𝑥 ∈ 𝐴 { 𝑥 } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfdisj2 | ⊢ ( Disj 𝑥 ∈ 𝐴 { 𝑥 } ↔ ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ { 𝑥 } ) ) | |
2 | moeq | ⊢ ∃* 𝑥 𝑥 = 𝑦 | |
3 | simpr | ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ { 𝑥 } ) → 𝑦 ∈ { 𝑥 } ) | |
4 | velsn | ⊢ ( 𝑦 ∈ { 𝑥 } ↔ 𝑦 = 𝑥 ) | |
5 | 3 4 | sylib | ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ { 𝑥 } ) → 𝑦 = 𝑥 ) |
6 | 5 | equcomd | ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ { 𝑥 } ) → 𝑥 = 𝑦 ) |
7 | 6 | moimi | ⊢ ( ∃* 𝑥 𝑥 = 𝑦 → ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ { 𝑥 } ) ) |
8 | 2 7 | ax-mp | ⊢ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ { 𝑥 } ) |
9 | 1 8 | mpgbir | ⊢ Disj 𝑥 ∈ 𝐴 { 𝑥 } |