uzind4

Description: Induction on the upper set of integers that starts at an integer M . The first four hypotheses give us the substitution instances we need, and the last two are the basis and the induction step. (Contributed by NM, 7-Sep-2005)

	Ref	Expression
Hypotheses	uzind4.1	$⊢ j = M \to (φ \leftrightarrow ψ)$
	uzind4.2	$⊢ j = k \to (φ \leftrightarrow χ)$
	uzind4.3	$⊢ j = k + 1 \to (φ \leftrightarrow θ)$
	uzind4.4	$⊢ j = N \to (φ \leftrightarrow τ)$
	uzind4.5	$⊢ M \in ℤ \to ψ$
	uzind4.6	$⊢ k \in ℤ_{\geq M} \to (χ \to θ)$
Assertion	uzind4	$⊢ N \in ℤ_{\geq M} \to τ$

Proof

Step	Hyp	Ref	Expression
1		uzind4.1	$⊢ j = M \to (φ \leftrightarrow ψ)$
2		uzind4.2	$⊢ j = k \to (φ \leftrightarrow χ)$
3		uzind4.3	$⊢ j = k + 1 \to (φ \leftrightarrow θ)$
4		uzind4.4	$⊢ j = N \to (φ \leftrightarrow τ)$
5		uzind4.5	$⊢ M \in ℤ \to ψ$
6		uzind4.6	$⊢ k \in ℤ_{\geq M} \to (χ \to θ)$
7		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
8		breq2	$⊢ m = N \to (M \leq m \leftrightarrow M \leq N)$
9		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
10		eluzle	$⊢ N \in ℤ_{\geq M} \to M \leq N$
11	8 9 10	elrabd	$⊢ N \in ℤ_{\geq M} \to N \in \{m \in ℤ \| M \leq m\}$
12		breq2	$⊢ m = k \to (M \leq m \leftrightarrow M \leq k)$
13	12	elrab	$⊢ k \in \{m \in ℤ \| M \leq m\} \leftrightarrow (k \in ℤ \land M \leq k)$
14		eluz2	$⊢ k \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land k \in ℤ \land M \leq k)$
15	14	biimpri	$⊢ (M \in ℤ \land k \in ℤ \land M \leq k) \to k \in ℤ_{\geq M}$
16	15	3expb	$⊢ (M \in ℤ \land (k \in ℤ \land M \leq k)) \to k \in ℤ_{\geq M}$
17	13 16	sylan2b	$⊢ (M \in ℤ \land k \in \{m \in ℤ \| M \leq m\}) \to k \in ℤ_{\geq M}$
18	17 6	syl	$⊢ (M \in ℤ \land k \in \{m \in ℤ \| M \leq m\}) \to (χ \to θ)$
19	1 2 3 4 5 18	uzind3	$⊢ (M \in ℤ \land N \in \{m \in ℤ \| M \leq m\}) \to τ$
20	7 11 19	syl2anc	$⊢ N \in ℤ_{\geq M} \to τ$

Metamath Proof Explorer

Theorem uzind4

Proof