uzindd

Description: Induction on the upper integers that start at M . The first four hypotheses give us the substitution instances we need; the following two are the basis and the induction step, a deduction version. (Contributed by metakunt, 8-Jun-2024)

	Ref	Expression
Hypotheses	uzindd.1	$⊢ j = M \to (ψ \leftrightarrow χ)$
	uzindd.2	$⊢ j = k \to (ψ \leftrightarrow θ)$
	uzindd.3	$⊢ j = k + 1 \to (ψ \leftrightarrow τ)$
	uzindd.4	$⊢ j = N \to (ψ \leftrightarrow η)$
	uzindd.5	$⊢ φ \to χ$
	uzindd.6	$⊢ (φ \land θ \land (k \in ℤ \land M \leq k)) \to τ$
	uzindd.7	$⊢ φ \to M \in ℤ$
	uzindd.8	$⊢ φ \to N \in ℤ$
	uzindd.9	$⊢ φ \to M \leq N$
Assertion	uzindd	$⊢ φ \to η$

Proof

Step	Hyp	Ref	Expression
1		uzindd.1	$⊢ j = M \to (ψ \leftrightarrow χ)$
2		uzindd.2	$⊢ j = k \to (ψ \leftrightarrow θ)$
3		uzindd.3	$⊢ j = k + 1 \to (ψ \leftrightarrow τ)$
4		uzindd.4	$⊢ j = N \to (ψ \leftrightarrow η)$
5		uzindd.5	$⊢ φ \to χ$
6		uzindd.6	$⊢ (φ \land θ \land (k \in ℤ \land M \leq k)) \to τ$
7		uzindd.7	$⊢ φ \to M \in ℤ$
8		uzindd.8	$⊢ φ \to N \in ℤ$
9		uzindd.9	$⊢ φ \to M \leq N$
10	7 8 9	3jca	$⊢ φ \to (M \in ℤ \land N \in ℤ \land M \leq N)$
11	1	imbi2d	$⊢ j = M \to ((φ \to ψ) \leftrightarrow (φ \to χ))$
12	2	imbi2d	$⊢ j = k \to ((φ \to ψ) \leftrightarrow (φ \to θ))$
13	3	imbi2d	$⊢ j = k + 1 \to ((φ \to ψ) \leftrightarrow (φ \to τ))$
14	4	imbi2d	$⊢ j = N \to ((φ \to ψ) \leftrightarrow (φ \to η))$
15	5	adantr	$⊢ (φ \land M \in ℤ) \to χ$
16	15	expcom	$⊢ M \in ℤ \to (φ \to χ)$
17		3anass	$⊢ (M \in ℤ \land k \in ℤ \land M \leq k) \leftrightarrow (M \in ℤ \land (k \in ℤ \land M \leq k))$
18		ancom	$⊢ (M \in ℤ \land (k \in ℤ \land M \leq k)) \leftrightarrow ((k \in ℤ \land M \leq k) \land M \in ℤ)$
19	17 18	bitri	$⊢ (M \in ℤ \land k \in ℤ \land M \leq k) \leftrightarrow ((k \in ℤ \land M \leq k) \land M \in ℤ)$
20	6	ad4ant123	$⊢ (((φ \land θ) \land (k \in ℤ \land M \leq k)) \land M \in ℤ) \to τ$
21	20	anasss	$⊢ ((φ \land θ) \land ((k \in ℤ \land M \leq k) \land M \in ℤ)) \to τ$
22	19 21	sylan2b	$⊢ ((φ \land θ) \land (M \in ℤ \land k \in ℤ \land M \leq k)) \to τ$
23	22	3impa	$⊢ (φ \land θ \land (M \in ℤ \land k \in ℤ \land M \leq k)) \to τ$
24	23	3com23	$⊢ (φ \land (M \in ℤ \land k \in ℤ \land M \leq k) \land θ) \to τ$
25	24	3expia	$⊢ (φ \land (M \in ℤ \land k \in ℤ \land M \leq k)) \to (θ \to τ)$
26	25	expcom	$⊢ (M \in ℤ \land k \in ℤ \land M \leq k) \to (φ \to (θ \to τ))$
27	26	a2d	$⊢ (M \in ℤ \land k \in ℤ \land M \leq k) \to ((φ \to θ) \to (φ \to τ))$
28	11 12 13 14 16 27	uzind	$⊢ (M \in ℤ \land N \in ℤ \land M \leq N) \to (φ \to η)$
29	10 28	mpcom	$⊢ φ \to η$

Metamath Proof Explorer

Theorem uzindd

Proof