zextlet - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem zextlet 6191

Description: An extensionality-like property for integer ordering.

**Assertion**
Ref	Expression
zextlet	⊢ ((M ∈ ℤ ⋀ N ∈ ℤ ⋀ ∀k ∈ ℤ (k ≤ M ↔ k ≤ N)) → M = N)

Distinct variable groups: k,M k,N

**Proof of Theorem zextlet**
Step	Hyp	Ref	Expression
1		zret 6141	. . . . . . . . 9 ⊢ (M ∈ ℤ → M ∈ ℝ)
2		leidt 5543	. . . . . . . . 9 ⊢ (M ∈ ℝ → M ≤ M)
3	1, 2	syl 10	. . . . . . . 8 ⊢ (M ∈ ℤ → M ≤ M)
4	3	adantr 391	. . . . . . 7 ⊢ ((M ∈ ℤ ⋀ ∀k ∈ ℤ (k ≤ M ↔ k ≤ N)) → M ≤ M)
5		breq1 2627	. . . . . . . . 9 ⊢ (k = M → (k ≤ M ↔ M ≤ M))
6		breq1 2627	. . . . . . . . 9 ⊢ (k = M → (k ≤ N ↔ M ≤ N))
7	5, 6	bibi12d 631	. . . . . . . 8 ⊢ (k = M → ((k ≤ M ↔ k ≤ N) ↔ (M ≤ M ↔ M ≤ N)))
8	7	rcla4va 1878	. . . . . . 7 ⊢ ((M ∈ ℤ ⋀ ∀k ∈ ℤ (k ≤ M ↔ k ≤ N)) → (M ≤ M ↔ M ≤ N))
9	4, 8	mpbid 195	. . . . . 6 ⊢ ((M ∈ ℤ ⋀ ∀k ∈ ℤ (k ≤ M ↔ k ≤ N)) → M ≤ N)
10	9	adantlr 395	. . . . 5 ⊢ (((M ∈ ℤ ⋀ N ∈ ℤ) ⋀ ∀k ∈ ℤ (k ≤ M ↔ k ≤ N)) → M ≤ N)
11		zret 6141	. . . . . . . . 9 ⊢ (N ∈ ℤ → N ∈ ℝ)
12		leidt 5543	. . . . . . . . 9 ⊢ (N ∈ ℝ → N ≤ N)
13	11, 12	syl 10	. . . . . . . 8 ⊢ (N ∈ ℤ → N ≤ N)
14	13	adantr 391	. . . . . . 7 ⊢ ((N ∈ ℤ ⋀ ∀k ∈ ℤ (k ≤ M ↔ k ≤ N)) → N ≤ N)
15		breq1 2627	. . . . . . . . 9 ⊢ (k = N → (k ≤ M ↔ N ≤ M))
16		breq1 2627	. . . . . . . . 9 ⊢ (k = N → (k ≤ N ↔ N ≤ N))
17	15, 16	bibi12d 631	. . . . . . . 8 ⊢ (k = N → ((k ≤ M ↔ k ≤ N) ↔ (N ≤ M ↔ N ≤ N)))
18	17	rcla4va 1878	. . . . . . 7 ⊢ ((N ∈ ℤ ⋀ ∀k ∈ ℤ (k ≤ M ↔ k ≤ N)) → (N ≤ M ↔ N ≤ N))
19	14, 18	mpbird 196	. . . . . 6 ⊢ ((N ∈ ℤ ⋀ ∀k ∈ ℤ (k ≤ M ↔ k ≤ N)) → N ≤ M)
20	19	adantll 394	. . . . 5 ⊢ (((M ∈ ℤ ⋀ N ∈ ℤ) ⋀ ∀k ∈ ℤ (k ≤ M ↔ k ≤ N)) → N ≤ M)
21	10, 20	jca 288	. . . 4 ⊢ (((M ∈ ℤ ⋀ N ∈ ℤ) ⋀ ∀k ∈ ℤ (k ≤ M ↔ k ≤ N)) → (M ≤ N ⋀ N ≤ M))
22	21	ex 373	. . 3 ⊢ ((M ∈ ℤ ⋀ N ∈ ℤ) → (∀k ∈ ℤ (k ≤ M ↔ k ≤ N) → (M ≤ N ⋀ N ≤ M)))
23		letri3t 5529	. . . 4 ⊢ ((M ∈ ℝ ⋀ N ∈ ℝ) → (M = N ↔ (M ≤ N ⋀ N ≤ M)))
24	23, 1, 11	syl2an 456	. . 3 ⊢ ((M ∈ ℤ ⋀ N ∈ ℤ) → (M = N ↔ (M ≤ N ⋀ N ≤ M)))
25	22, 24	sylibrd 204	. 2 ⊢ ((M ∈ ℤ ⋀ N ∈ ℤ) → (∀k ∈ ℤ (k ≤ M ↔ k ≤ N) → M = N))
26	25	3impia 832	1 ⊢ ((M ∈ ℤ ⋀ N ∈ ℤ ⋀ ∀k ∈ ℤ (k ≤ M ↔ k ≤ N)) → M = N)

Colors of variables: wff set class

Syntax hints: → wi 3 ↔ wb 146 ⋀ wa 223 ⋀ w3a 777 = wceq 958 ∈ wcel 960 ∀wral 1648 class class class wbr 2624 ℝcr 5245 ≤ cle 5307 ℤcz 5310

This theorem is referenced by: zextltt 6192

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 964 ax-gen 965 ax-8 966 ax-9 967 ax-10 968 ax-11 969 ax-12 970 ax-13 971 ax-14 972 ax-17 973 ax-4 975 ax-5o 977 ax-6o 980 ax-9o 1125 ax-10o 1142 ax-16 1212 ax-11o 1220 ax-ext 1462 ax-rep 2698 ax-sep 2708 ax-nul 2715 ax-pow 2748 ax-pr 2785 ax-un 2872 ax-inf2 4634

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 778 df-3an 779 df-ex 983 df-sb 1174 df-eu 1384 df-mo 1385 df-clab 1467 df-cleq 1472 df-clel 1475 df-ne 1590 df-nel 1591 df-ral 1652 df-rex 1653 df-reu 1654 df-rab 1655 df-v 1815 df-sbc 1945 df-csb 2005 df-dif 2052 df-un 2053 df-in 2054 df-ss 2056 df-pss 2058 df-nul 2284 df-if 2366 df-pw 2406 df-sn 2416 df-pr 2417 df-tp 2419 df-op 2420 df-uni 2508 df-int 2538 df-iun 2572 df-br 2625 df-opab 2672 df-tr 2686 df-eprel 2838 df-id 2841 df-po 2846 df-so 2856 df-fr 2923 df-we 2940 df-ord 2957 df-on 2958 df-lim 2959 df-suc 2960 df-om 3138 df-xp 3190 df-rel 3191 df-cnv 3192 df-co 3193 df-dm 3194 df-rn 3195 df-res 3196 df-ima 3197 df-fun 3198 df-fn 3199 df-f 3200 df-f1 3201 df-fo 3202 df-f1o 3203 df-fv 3204 df-rdg 3938 df-opr 3971 df-oprab 3972 df-1st 4085 df-2nd 4086 df-1o 4139 df-oadd 4141 df-omul 4142 df-er 4267 df-ec 4269 df-qs 4272 df-en 4374 df-dom 4375 df-sdom 4376 df-ni 5012 df-pli 5013 df-mi 5014 df-lti 5015 df-plpq 5047 df-mpq 5048 df-enq 5049 df-nq 5050 df-plq 5051 df-mq 5052 df-rq 5053 df-ltq 5054 df-1q 5055 df-np 5098 df-1p 5099 df-plp 5100 df-ltp 5102 df-enr 5178 df-nr 5179 df-ltr 5182 df-0r 5183 df-c 5252 df-r 5256 df-lt 5259 df-neg 5370 df-pnf 5499 df-mnf 5500 df-xr 5501 df-ltxr 5502 df-le 5503 df-z 6138