Metamath Proof Explorer

Theorem elfzp1

Description: Append an element to a finite set of sequential integers. (Contributed by NM, 19-Sep-2005) (Proof shortened by Mario Carneiro, 28-Apr-2015)

		Ref	Expression
	Assertion	elfzp1	$⊢ N \in ℤ_{\geq M} \to (K \in (M \dots N + 1) \leftrightarrow (K \in (M \dots N) \lor K = N + 1))$

Proof

Step	Hyp	Ref	Expression
1		fzsuc	$⊢ N \in ℤ_{\geq M} \to (M \dots N + 1) = (M \dots N) \cup \{N + 1\}$
2	1	eleq2d	$⊢ N \in ℤ_{\geq M} \to (K \in (M \dots N + 1) \leftrightarrow K \in ((M \dots N) \cup \{N + 1\}))$
3		elun	$⊢ K \in ((M \dots N) \cup \{N + 1\}) \leftrightarrow (K \in (M \dots N) \lor K \in \{N + 1\})$
4		ovex	$⊢ N + 1 \in V$
5	4	elsn2	$⊢ K \in \{N + 1\} \leftrightarrow K = N + 1$
6	5	orbi2i	$⊢ (K \in (M \dots N) \lor K \in \{N + 1\}) \leftrightarrow (K \in (M \dots N) \lor K = N + 1)$
7	3 6	bitri	$⊢ K \in ((M \dots N) \cup \{N + 1\}) \leftrightarrow (K \in (M \dots N) \lor K = N + 1)$
8	2 7	bitrdi	$⊢ N \in ℤ_{\geq M} \to (K \in (M \dots N + 1) \leftrightarrow (K \in (M \dots N) \lor K = N + 1))$