ssfzo12

Description: Subset relationship for half-open integer ranges. (Contributed by Alexander van der Vekens, 16-Mar-2018)

		Ref	Expression
	Assertion	ssfzo12	$⊢ (K \in ℤ \land L \in ℤ \land K < L) \to ((K ..^L) \subseteq (M ..^N) \to (M \leq K \land L \leq N))$

Proof

Step	Hyp	Ref	Expression
1		fzolb2	$⊢ (K \in ℤ \land L \in ℤ) \to (K \in (K ..^L) \leftrightarrow K < L)$
2	1	biimp3ar	$⊢ (K \in ℤ \land L \in ℤ \land K < L) \to K \in (K ..^L)$
3		fzoend	$⊢ K \in (K ..^L) \to L - 1 \in (K ..^L)$
4		ssel2	$⊢ ((K ..^L) \subseteq (M ..^N) \land K \in (K ..^L)) \to K \in (M ..^N)$
5		ssel2	$⊢ ((K ..^L) \subseteq (M ..^N) \land L - 1 \in (K ..^L)) \to L - 1 \in (M ..^N)$
6		elfzolt2	$⊢ L - 1 \in (M ..^N) \to L - 1 < N$
7		simp2	$⊢ (K \in ℤ \land L \in ℤ \land K < L) \to L \in ℤ$
8		elfzoel2	$⊢ K \in (M ..^N) \to N \in ℤ$
9		zlem1lt	$⊢ (L \in ℤ \land N \in ℤ) \to (L \leq N \leftrightarrow L - 1 < N)$
10	7 8 9	syl2anr	$⊢ (K \in (M ..^N) \land (K \in ℤ \land L \in ℤ \land K < L)) \to (L \leq N \leftrightarrow L - 1 < N)$
11		elfzole1	$⊢ K \in (M ..^N) \to M \leq K$
12		pm3.2	$⊢ M \leq K \to (L \leq N \to (M \leq K \land L \leq N))$
13	11 12	syl	$⊢ K \in (M ..^N) \to (L \leq N \to (M \leq K \land L \leq N))$
14	13	adantr	$⊢ (K \in (M ..^N) \land (K \in ℤ \land L \in ℤ \land K < L)) \to (L \leq N \to (M \leq K \land L \leq N))$
15	10 14	sylbird	$⊢ (K \in (M ..^N) \land (K \in ℤ \land L \in ℤ \land K < L)) \to (L - 1 < N \to (M \leq K \land L \leq N))$
16	15	ex	$⊢ K \in (M ..^N) \to ((K \in ℤ \land L \in ℤ \land K < L) \to (L - 1 < N \to (M \leq K \land L \leq N)))$
17	16	com13	$⊢ L - 1 < N \to ((K \in ℤ \land L \in ℤ \land K < L) \to (K \in (M ..^N) \to (M \leq K \land L \leq N)))$
18	5 6 17	3syl	$⊢ ((K ..^L) \subseteq (M ..^N) \land L - 1 \in (K ..^L)) \to ((K \in ℤ \land L \in ℤ \land K < L) \to (K \in (M ..^N) \to (M \leq K \land L \leq N)))$
19	18	ex	$⊢ (K ..^L) \subseteq (M ..^N) \to (L - 1 \in (K ..^L) \to ((K \in ℤ \land L \in ℤ \land K < L) \to (K \in (M ..^N) \to (M \leq K \land L \leq N))))$
20	19	com24	$⊢ (K ..^L) \subseteq (M ..^N) \to (K \in (M ..^N) \to ((K \in ℤ \land L \in ℤ \land K < L) \to (L - 1 \in (K ..^L) \to (M \leq K \land L \leq N))))$
21	4 20	syl5com	$⊢ ((K ..^L) \subseteq (M ..^N) \land K \in (K ..^L)) \to ((K ..^L) \subseteq (M ..^N) \to ((K \in ℤ \land L \in ℤ \land K < L) \to (L - 1 \in (K ..^L) \to (M \leq K \land L \leq N))))$
22	21	ex	$⊢ (K ..^L) \subseteq (M ..^N) \to (K \in (K ..^L) \to ((K ..^L) \subseteq (M ..^N) \to ((K \in ℤ \land L \in ℤ \land K < L) \to (L - 1 \in (K ..^L) \to (M \leq K \land L \leq N)))))$
23	22	pm2.43a	$⊢ (K ..^L) \subseteq (M ..^N) \to (K \in (K ..^L) \to ((K \in ℤ \land L \in ℤ \land K < L) \to (L - 1 \in (K ..^L) \to (M \leq K \land L \leq N))))$
24	23	com14	$⊢ L - 1 \in (K ..^L) \to (K \in (K ..^L) \to ((K \in ℤ \land L \in ℤ \land K < L) \to ((K ..^L) \subseteq (M ..^N) \to (M \leq K \land L \leq N))))$
25	3 24	mpcom	$⊢ K \in (K ..^L) \to ((K \in ℤ \land L \in ℤ \land K < L) \to ((K ..^L) \subseteq (M ..^N) \to (M \leq K \land L \leq N)))$
26	2 25	mpcom	$⊢ (K \in ℤ \land L \in ℤ \land K < L) \to ((K ..^L) \subseteq (M ..^N) \to (M \leq K \land L \leq N))$

Metamath Proof Explorer

Theorem ssfzo12

Proof