Theorem nmembers1lem3 6271

Description: Lemma for nmembers1 6272. If the interval from one to a natural is in a given natural, extending it by one puts it in the next natural. (Contributed by Scott Fenton, 3-Aug-2019.)

Assertion

Ref	Expression
nmembers1lem3	|- ((A e. Nn /\ B e. Nn ) -> ({m e. Nn | (1c <_c m /\ m <_c A)} e. B -> {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} e. (B +o 1c)))

Distinct variable groups:   A,m   B,m

Proof of Theorem nmembers1lem3

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnltp1c 6263	. . . . . . . . . . . 12 |- (A e. Nn -> A <c (A +o 1c))
2		nnnc 6147	. . . . . . . . . . . . 13 |- (A e. Nn -> A e. NC )
3		peano2 4404	. . . . . . . . . . . . . 14 |- (A e. Nn -> (A +o 1c) e. Nn )
4		nnnc 6147	. . . . . . . . . . . . . 14 |- ((A +o 1c) e. Nn -> (A +o 1c) e. NC )
5	3, 4	syl 15	. . . . . . . . . . . . 13 |- (A e. Nn -> (A +o 1c) e. NC )
6		ltlenlec 6208	. . . . . . . . . . . . 13 |- ((A e. NC /\ (A +o 1c) e. NC ) -> (A <c (A +o 1c) <-> (A <_c (A +o 1c) /\ -. (A +o 1c) <_c A)))
7	2, 5, 6	syl2anc 642	. . . . . . . . . . . 12 |- (A e. Nn -> (A <c (A +o 1c) <-> (A <_c (A +o 1c) /\ -. (A +o 1c) <_c A)))
8	1, 7	mpbid 201	. . . . . . . . . . 11 |- (A e. Nn -> (A <_c (A +o 1c) /\ -. (A +o 1c) <_c A))
9	8	simprd 449	. . . . . . . . . 10 |- (A e. Nn -> -. (A +o 1c) <_c A)
10	9	adantr 451	. . . . . . . . 9 |- ((A e. Nn /\ B e. Nn ) -> -. (A +o 1c) <_c A)
11	10	intnand 882	. . . . . . . 8 |- ((A e. Nn /\ B e. Nn ) -> -. (1c <_c (A +o 1c) /\ (A +o 1c) <_c A))
12	11	a1d 22	. . . . . . 7 |- ((A e. Nn /\ B e. Nn ) -> ((A +o 1c) e. Nn -> -. (1c <_c (A +o 1c) /\ (A +o 1c) <_c A)))
13		breq2 4644	. . . . . . . . . . 11 |- (m = (A +o 1c) -> (1c <_c m <-> 1c <_c (A +o 1c)))
14		breq1 4643	. . . . . . . . . . 11 |- (m = (A +o 1c) -> (m <_c A <-> (A +o 1c) <_c A))
15	13, 14	anbi12d 691	. . . . . . . . . 10 |- (m = (A +o 1c) -> ((1c <_c m /\ m <_c A) <-> (1c <_c (A +o 1c) /\ (A +o 1c) <_c A)))
16	15	elrab 2995	. . . . . . . . 9 |- ((A +o 1c) e. {m e. Nn | (1c <_c m /\ m <_c A)} <-> ((A +o 1c) e. Nn /\ (1c <_c (A +o 1c) /\ (A +o 1c) <_c A)))
17	16	notbii 287	. . . . . . . 8 |- (-. (A +o 1c) e. {m e. Nn | (1c <_c m /\ m <_c A)} <-> -. ((A +o 1c) e. Nn /\ (1c <_c (A +o 1c) /\ (A +o 1c) <_c A)))
18		imnan 411	. . . . . . . 8 |- (((A +o 1c) e. Nn -> -. (1c <_c (A +o 1c) /\ (A +o 1c) <_c A)) <-> -. ((A +o 1c) e. Nn /\ (1c <_c (A +o 1c) /\ (A +o 1c) <_c A)))
19	17, 18	bitr4i 243	. . . . . . 7 |- (-. (A +o 1c) e. {m e. Nn | (1c <_c m /\ m <_c A)} <-> ((A +o 1c) e. Nn -> -. (1c <_c (A +o 1c) /\ (A +o 1c) <_c A)))
20	12, 19	sylibr 203	. . . . . 6 |- ((A e. Nn /\ B e. Nn ) -> -. (A +o 1c) e. {m e. Nn | (1c <_c m /\ m <_c A)})
21	3	adantr 451	. . . . . . 7 |- ((A e. Nn /\ B e. Nn ) -> (A +o 1c) e. Nn )
22		elcomplg 3219	. . . . . . 7 |- ((A +o 1c) e. Nn -> ((A +o 1c) e. ∼ {m e. Nn | (1c <_c m /\ m <_c A)} <-> -. (A +o 1c) e. {m e. Nn | (1c <_c m /\ m <_c A)}))
23	21, 22	syl 15	. . . . . 6 |- ((A e. Nn /\ B e. Nn ) -> ((A +o 1c) e. ∼ {m e. Nn | (1c <_c m /\ m <_c A)} <-> -. (A +o 1c) e. {m e. Nn | (1c <_c m /\ m <_c A)}))
24	20, 23	mpbird 223	. . . . 5 |- ((A e. Nn /\ B e. Nn ) -> (A +o 1c) e. ∼ {m e. Nn | (1c <_c m /\ m <_c A)})
25		nnnc 6147	. . . . . . . . . . . . . 14 |- (x e. Nn -> x e. NC )
26		ncslesuc 6268	. . . . . . . . . . . . . 14 |- ((x e. NC /\ A e. NC ) -> (x <_c (A +o 1c) <-> (x <_c A \/ x = (A +o 1c))))
27	25, 2, 26	syl2an 463	. . . . . . . . . . . . 13 |- ((x e. Nn /\ A e. Nn ) -> (x <_c (A +o 1c) <-> (x <_c A \/ x = (A +o 1c))))
28	27	expcom 424	. . . . . . . . . . . 12 |- (A e. Nn -> (x e. Nn -> (x <_c (A +o 1c) <-> (x <_c A \/ x = (A +o 1c)))))
29	28	adantrd 454	. . . . . . . . . . 11 |- (A e. Nn -> ((x e. Nn /\ 1c <_c x) -> (x <_c (A +o 1c) <-> (x <_c A \/ x = (A +o 1c)))))
30	29	adantr 451	. . . . . . . . . 10 |- ((A e. Nn /\ B e. Nn ) -> ((x e. Nn /\ 1c <_c x) -> (x <_c (A +o 1c) <-> (x <_c A \/ x = (A +o 1c)))))
31	30	pm5.32d 620	. . . . . . . . 9 |- ((A e. Nn /\ B e. Nn ) -> (((x e. Nn /\ 1c <_c x) /\ x <_c (A +o 1c)) <-> ((x e. Nn /\ 1c <_c x) /\ (x <_c A \/ x = (A +o 1c)))))
32		anass 630	. . . . . . . . 9 |- (((x e. Nn /\ 1c <_c x) /\ x <_c (A +o 1c)) <-> (x e. Nn /\ (1c <_c x /\ x <_c (A +o 1c))))
33		andi 837	. . . . . . . . . 10 |- (((x e. Nn /\ 1c <_c x) /\ (x <_c A \/ x = (A +o 1c))) <-> (((x e. Nn /\ 1c <_c x) /\ x <_c A) \/ ((x e. Nn /\ 1c <_c x) /\ x = (A +o 1c))))
34		anass 630	. . . . . . . . . . 11 |- (((x e. Nn /\ 1c <_c x) /\ x <_c A) <-> (x e. Nn /\ (1c <_c x /\ x <_c A)))
35	34	orbi1i 506	. . . . . . . . . 10 |- ((((x e. Nn /\ 1c <_c x) /\ x <_c A) \/ ((x e. Nn /\ 1c <_c x) /\ x = (A +o 1c))) <-> ((x e. Nn /\ (1c <_c x /\ x <_c A)) \/ ((x e. Nn /\ 1c <_c x) /\ x = (A +o 1c))))
36	33, 35	bitri 240	. . . . . . . . 9 |- (((x e. Nn /\ 1c <_c x) /\ (x <_c A \/ x = (A +o 1c))) <-> ((x e. Nn /\ (1c <_c x /\ x <_c A)) \/ ((x e. Nn /\ 1c <_c x) /\ x = (A +o 1c))))
37	31, 32, 36	3bitr3g 278	. . . . . . . 8 |- ((A e. Nn /\ B e. Nn ) -> ((x e. Nn /\ (1c <_c x /\ x <_c (A +o 1c))) <-> ((x e. Nn /\ (1c <_c x /\ x <_c A)) \/ ((x e. Nn /\ 1c <_c x) /\ x = (A +o 1c)))))
38		1cnc 6140	. . . . . . . . . . . . . . . 16 |- 1c e. NC
39		addlecncs 6210	. . . . . . . . . . . . . . . 16 |- ((1c e. NC /\ A e. NC ) -> 1c <_c (1c +o A))
40	38, 2, 39	sylancr 644	. . . . . . . . . . . . . . 15 |- (A e. Nn -> 1c <_c (1c +o A))
41		addccom 4407	. . . . . . . . . . . . . . 15 |- (A +o 1c) = (1c +o A)
42	40, 41	syl6breqr 4680	. . . . . . . . . . . . . 14 |- (A e. Nn -> 1c <_c (A +o 1c))
43	3, 42	jca 518	. . . . . . . . . . . . 13 |- (A e. Nn -> ((A +o 1c) e. Nn /\ 1c <_c (A +o 1c)))
44		eleq1 2413	. . . . . . . . . . . . . 14 |- (x = (A +o 1c) -> (x e. Nn <-> (A +o 1c) e. Nn ))
45		breq2 4644	. . . . . . . . . . . . . 14 |- (x = (A +o 1c) -> (1c <_c x <-> 1c <_c (A +o 1c)))
46	44, 45	anbi12d 691	. . . . . . . . . . . . 13 |- (x = (A +o 1c) -> ((x e. Nn /\ 1c <_c x) <-> ((A +o 1c) e. Nn /\ 1c <_c (A +o 1c))))
47	43, 46	syl5ibrcom 213	. . . . . . . . . . . 12 |- (A e. Nn -> (x = (A +o 1c) -> (x e. Nn /\ 1c <_c x)))
48	47	adantr 451	. . . . . . . . . . 11 |- ((A e. Nn /\ B e. Nn ) -> (x = (A +o 1c) -> (x e. Nn /\ 1c <_c x)))
49	48	pm4.71rd 616	. . . . . . . . . 10 |- ((A e. Nn /\ B e. Nn ) -> (x = (A +o 1c) <-> ((x e. Nn /\ 1c <_c x) /\ x = (A +o 1c))))
50	49	bicomd 192	. . . . . . . . 9 |- ((A e. Nn /\ B e. Nn ) -> (((x e. Nn /\ 1c <_c x) /\ x = (A +o 1c)) <-> x = (A +o 1c)))
51	50	orbi2d 682	. . . . . . . 8 |- ((A e. Nn /\ B e. Nn ) -> (((x e. Nn /\ (1c <_c x /\ x <_c A)) \/ ((x e. Nn /\ 1c <_c x) /\ x = (A +o 1c))) <-> ((x e. Nn /\ (1c <_c x /\ x <_c A)) \/ x = (A +o 1c))))
52	37, 51	bitrd 244	. . . . . . 7 |- ((A e. Nn /\ B e. Nn ) -> ((x e. Nn /\ (1c <_c x /\ x <_c (A +o 1c))) <-> ((x e. Nn /\ (1c <_c x /\ x <_c A)) \/ x = (A +o 1c))))
53		breq2 4644	. . . . . . . . 9 |- (m = x -> (1c <_c m <-> 1c <_c x))
54		breq1 4643	. . . . . . . . 9 |- (m = x -> (m <_c (A +o 1c) <-> x <_c (A +o 1c)))
55	53, 54	anbi12d 691	. . . . . . . 8 |- (m = x -> ((1c <_c m /\ m <_c (A +o 1c)) <-> (1c <_c x /\ x <_c (A +o 1c))))
56	55	elrab 2995	. . . . . . 7 |- (x e. {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} <-> (x e. Nn /\ (1c <_c x /\ x <_c (A +o 1c))))
57		elun 3221	. . . . . . . 8 |- (x e. ({m e. Nn | (1c <_c m /\ m <_c A)} u. {(A +o 1c)}) <-> (x e. {m e. Nn | (1c <_c m /\ m <_c A)} \/ x e. {(A +o 1c)}))
58		breq1 4643	. . . . . . . . . . 11 |- (m = x -> (m <_c A <-> x <_c A))
59	53, 58	anbi12d 691	. . . . . . . . . 10 |- (m = x -> ((1c <_c m /\ m <_c A) <-> (1c <_c x /\ x <_c A)))
60	59	elrab 2995	. . . . . . . . 9 |- (x e. {m e. Nn | (1c <_c m /\ m <_c A)} <-> (x e. Nn /\ (1c <_c x /\ x <_c A)))
61		elsn 3749	. . . . . . . . 9 |- (x e. {(A +o 1c)} <-> x = (A +o 1c))
62	60, 61	orbi12i 507	. . . . . . . 8 |- ((x e. {m e. Nn | (1c <_c m /\ m <_c A)} \/ x e. {(A +o 1c)}) <-> ((x e. Nn /\ (1c <_c x /\ x <_c A)) \/ x = (A +o 1c)))
63	57, 62	bitri 240	. . . . . . 7 |- (x e. ({m e. Nn | (1c <_c m /\ m <_c A)} u. {(A +o 1c)}) <-> ((x e. Nn /\ (1c <_c x /\ x <_c A)) \/ x = (A +o 1c)))
64	52, 56, 63	3bitr4g 279	. . . . . 6 |- ((A e. Nn /\ B e. Nn ) -> (x e. {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} <-> x e. ({m e. Nn | (1c <_c m /\ m <_c A)} u. {(A +o 1c)})))
65	64	eqrdv 2351	. . . . 5 |- ((A e. Nn /\ B e. Nn ) -> {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {(A +o 1c)}))
66		sneq 3745	. . . . . . . 8 |- (y = (A +o 1c) -> {y} = {(A +o 1c)})
67	66	uneq2d 3419	. . . . . . 7 |- (y = (A +o 1c) -> ({m e. Nn | (1c <_c m /\ m <_c A)} u. {y}) = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {(A +o 1c)}))
68	67	eqeq2d 2364	. . . . . 6 |- (y = (A +o 1c) -> ({m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {y}) <-> {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {(A +o 1c)})))
69	68	rspcev 2956	. . . . 5 |- (((A +o 1c) e. ∼ {m e. Nn | (1c <_c m /\ m <_c A)} /\ {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {(A +o 1c)})) -> E.y e. ∼ {m e. Nn | (1c <_c m /\ m <_c A)} {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {y}))
70	24, 65, 69	syl2anc 642	. . . 4 |- ((A e. Nn /\ B e. Nn ) -> E.y e. ∼ {m e. Nn | (1c <_c m /\ m <_c A)} {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {y}))
71		compleq 3244	. . . . . 6 |- (x = {m e. Nn | (1c <_c m /\ m <_c A)} -> ∼ x = ∼ {m e. Nn | (1c <_c m /\ m <_c A)})
72		uneq1 3412	. . . . . . 7 |- (x = {m e. Nn | (1c <_c m /\ m <_c A)} -> (x u. {y}) = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {y}))
73	72	eqeq2d 2364	. . . . . 6 |- (x = {m e. Nn | (1c <_c m /\ m <_c A)} -> ({m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = (x u. {y}) <-> {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {y})))
74	71, 73	rexeqbidv 2821	. . . . 5 |- (x = {m e. Nn | (1c <_c m /\ m <_c A)} -> (E.y e. ∼ x{m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = (x u. {y}) <-> E.y e. ∼ {m e. Nn | (1c <_c m /\ m <_c A)} {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {y})))
75	74	rspcev 2956	. . . 4 |- (({m e. Nn | (1c <_c m /\ m <_c A)} e. B /\ E.y e. ∼ {m e. Nn | (1c <_c m /\ m <_c A)} {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {y})) -> E.x e. B E.y e. ∼ x{m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = (x u. {y}))
76	70, 75	sylan2 460	. . 3 |- (({m e. Nn | (1c <_c m /\ m <_c A)} e. B /\ (A e. Nn /\ B e. Nn )) -> E.x e. B E.y e. ∼ x{m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = (x u. {y}))
77		elsuc 4414	. . 3 |- ({m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} e. (B +o 1c) <-> E.x e. B E.y e. ∼ x{m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = (x u. {y}))
78	76, 77	sylibr 203	. 2 |- (({m e. Nn | (1c <_c m /\ m <_c A)} e. B /\ (A e. Nn /\ B e. Nn )) -> {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} e. (B +o 1c))
79	78	expcom 424	1 |- ((A e. Nn /\ B e. Nn ) -> ({m e. Nn | (1c <_c m /\ m <_c A)} e. B -> {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} e. (B +o 1c)))

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   \/ wo 357   /\ wa 358   = wceq 1642   e. wcel 1710  E.wrex 2616  {crab 2619   ∼ ccompl 3206   u. cun 3208  {csn 3738  1_cc1c 4135   Nn cnnc 4374   +o cplc 4376   class class class wbr 4640   NC cncs 6089   <__c clec 6090   <_c cltc 6091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-reu 2622  df-rmo 2623  df-rab 2624  df-v 2862  df-sbc 3048  df-csb 3138  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-pss 3262  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-iun 3972  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-iota 4340  df-0c 4378  df-addc 4379  df-nnc 4380  df-fin 4381  df-lefin 4441  df-ltfin 4442  df-ncfin 4443  df-tfin 4444  df-evenfin 4445  df-oddfin 4446  df-sfin 4447  df-spfin 4448  df-phi 4566  df-op 4567  df-proj1 4568  df-proj2 4569  df-opab 4624  df-br 4641  df-1st 4724  df-swap 4725  df-sset 4726  df-co 4727  df-ima 4728  df-si 4729  df-id 4768  df-xp 4785  df-cnv 4786  df-rn 4787  df-dm 4788  df-res 4789  df-fun 4790  df-fn 4791  df-f 4792  df-f1 4793  df-fo 4794  df-f1o 4795  df-fv 4796  df-2nd 4798  df-ov 5527  df-oprab 5529  df-mpt 5653  df-mpt2 5655  df-txp 5737  df-fix 5741  df-cup 5743  df-disj 5745  df-addcfn 5747  df-ins2 5751  df-ins3 5753  df-image 5755  df-ins4 5757  df-si3 5759  df-funs 5761  df-fns 5763  df-clos1 5874  df-trans 5900  df-sym 5909  df-er 5910  df-ec 5948  df-qs 5952  df-en 6030  df-ncs 6099  df-lec 6100  df-ltc 6101  df-nc 6102

This theorem is referenced by:  nmembers1  6272